ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nnaass Structured version   GIF version

Theorem nnaass 5968
Description: Addition of natural numbers is associative. Theorem 4K(1) of [Enderton] p. 81. (Contributed by NM, 20-Sep-1995.) (Revised by Mario Carneiro, 15-Nov-2014.)
Assertion
Ref Expression
nnaass ((A 𝜔 B 𝜔 𝐶 𝜔) → ((A +𝑜 B) +𝑜 𝐶) = (A +𝑜 (B +𝑜 𝐶)))

Proof of Theorem nnaass
Dummy variables x y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 5433 . . . . . 6 (x = 𝐶 → ((A +𝑜 B) +𝑜 x) = ((A +𝑜 B) +𝑜 𝐶))
2 oveq2 5433 . . . . . . 7 (x = 𝐶 → (B +𝑜 x) = (B +𝑜 𝐶))
32oveq2d 5441 . . . . . 6 (x = 𝐶 → (A +𝑜 (B +𝑜 x)) = (A +𝑜 (B +𝑜 𝐶)))
41, 3eqeq12d 2028 . . . . 5 (x = 𝐶 → (((A +𝑜 B) +𝑜 x) = (A +𝑜 (B +𝑜 x)) ↔ ((A +𝑜 B) +𝑜 𝐶) = (A +𝑜 (B +𝑜 𝐶))))
54imbi2d 219 . . . 4 (x = 𝐶 → (((A 𝜔 B 𝜔) → ((A +𝑜 B) +𝑜 x) = (A +𝑜 (B +𝑜 x))) ↔ ((A 𝜔 B 𝜔) → ((A +𝑜 B) +𝑜 𝐶) = (A +𝑜 (B +𝑜 𝐶)))))
6 oveq2 5433 . . . . . 6 (x = ∅ → ((A +𝑜 B) +𝑜 x) = ((A +𝑜 B) +𝑜 ∅))
7 oveq2 5433 . . . . . . 7 (x = ∅ → (B +𝑜 x) = (B +𝑜 ∅))
87oveq2d 5441 . . . . . 6 (x = ∅ → (A +𝑜 (B +𝑜 x)) = (A +𝑜 (B +𝑜 ∅)))
96, 8eqeq12d 2028 . . . . 5 (x = ∅ → (((A +𝑜 B) +𝑜 x) = (A +𝑜 (B +𝑜 x)) ↔ ((A +𝑜 B) +𝑜 ∅) = (A +𝑜 (B +𝑜 ∅))))
10 oveq2 5433 . . . . . 6 (x = y → ((A +𝑜 B) +𝑜 x) = ((A +𝑜 B) +𝑜 y))
11 oveq2 5433 . . . . . . 7 (x = y → (B +𝑜 x) = (B +𝑜 y))
1211oveq2d 5441 . . . . . 6 (x = y → (A +𝑜 (B +𝑜 x)) = (A +𝑜 (B +𝑜 y)))
1310, 12eqeq12d 2028 . . . . 5 (x = y → (((A +𝑜 B) +𝑜 x) = (A +𝑜 (B +𝑜 x)) ↔ ((A +𝑜 B) +𝑜 y) = (A +𝑜 (B +𝑜 y))))
14 oveq2 5433 . . . . . 6 (x = suc y → ((A +𝑜 B) +𝑜 x) = ((A +𝑜 B) +𝑜 suc y))
15 oveq2 5433 . . . . . . 7 (x = suc y → (B +𝑜 x) = (B +𝑜 suc y))
1615oveq2d 5441 . . . . . 6 (x = suc y → (A +𝑜 (B +𝑜 x)) = (A +𝑜 (B +𝑜 suc y)))
1714, 16eqeq12d 2028 . . . . 5 (x = suc y → (((A +𝑜 B) +𝑜 x) = (A +𝑜 (B +𝑜 x)) ↔ ((A +𝑜 B) +𝑜 suc y) = (A +𝑜 (B +𝑜 suc y))))
18 nnacl 5963 . . . . . . 7 ((A 𝜔 B 𝜔) → (A +𝑜 B) 𝜔)
19 nna0 5957 . . . . . . 7 ((A +𝑜 B) 𝜔 → ((A +𝑜 B) +𝑜 ∅) = (A +𝑜 B))
2018, 19syl 14 . . . . . 6 ((A 𝜔 B 𝜔) → ((A +𝑜 B) +𝑜 ∅) = (A +𝑜 B))
21 nna0 5957 . . . . . . . 8 (B 𝜔 → (B +𝑜 ∅) = B)
2221oveq2d 5441 . . . . . . 7 (B 𝜔 → (A +𝑜 (B +𝑜 ∅)) = (A +𝑜 B))
2322adantl 262 . . . . . 6 ((A 𝜔 B 𝜔) → (A +𝑜 (B +𝑜 ∅)) = (A +𝑜 B))
2420, 23eqtr4d 2049 . . . . 5 ((A 𝜔 B 𝜔) → ((A +𝑜 B) +𝑜 ∅) = (A +𝑜 (B +𝑜 ∅)))
25 suceq 4078 . . . . . . 7 (((A +𝑜 B) +𝑜 y) = (A +𝑜 (B +𝑜 y)) → suc ((A +𝑜 B) +𝑜 y) = suc (A +𝑜 (B +𝑜 y)))
26 nnasuc 5959 . . . . . . . . 9 (((A +𝑜 B) 𝜔 y 𝜔) → ((A +𝑜 B) +𝑜 suc y) = suc ((A +𝑜 B) +𝑜 y))
2718, 26sylan 267 . . . . . . . 8 (((A 𝜔 B 𝜔) y 𝜔) → ((A +𝑜 B) +𝑜 suc y) = suc ((A +𝑜 B) +𝑜 y))
28 nnasuc 5959 . . . . . . . . . . . 12 ((B 𝜔 y 𝜔) → (B +𝑜 suc y) = suc (B +𝑜 y))
2928oveq2d 5441 . . . . . . . . . . 11 ((B 𝜔 y 𝜔) → (A +𝑜 (B +𝑜 suc y)) = (A +𝑜 suc (B +𝑜 y)))
3029adantl 262 . . . . . . . . . 10 ((A 𝜔 (B 𝜔 y 𝜔)) → (A +𝑜 (B +𝑜 suc y)) = (A +𝑜 suc (B +𝑜 y)))
31 nnacl 5963 . . . . . . . . . . 11 ((B 𝜔 y 𝜔) → (B +𝑜 y) 𝜔)
32 nnasuc 5959 . . . . . . . . . . 11 ((A 𝜔 (B +𝑜 y) 𝜔) → (A +𝑜 suc (B +𝑜 y)) = suc (A +𝑜 (B +𝑜 y)))
3331, 32sylan2 270 . . . . . . . . . 10 ((A 𝜔 (B 𝜔 y 𝜔)) → (A +𝑜 suc (B +𝑜 y)) = suc (A +𝑜 (B +𝑜 y)))
3430, 33eqtrd 2046 . . . . . . . . 9 ((A 𝜔 (B 𝜔 y 𝜔)) → (A +𝑜 (B +𝑜 suc y)) = suc (A +𝑜 (B +𝑜 y)))
3534anassrs 380 . . . . . . . 8 (((A 𝜔 B 𝜔) y 𝜔) → (A +𝑜 (B +𝑜 suc y)) = suc (A +𝑜 (B +𝑜 y)))
3627, 35eqeq12d 2028 . . . . . . 7 (((A 𝜔 B 𝜔) y 𝜔) → (((A +𝑜 B) +𝑜 suc y) = (A +𝑜 (B +𝑜 suc y)) ↔ suc ((A +𝑜 B) +𝑜 y) = suc (A +𝑜 (B +𝑜 y))))
3725, 36syl5ibr 145 . . . . . 6 (((A 𝜔 B 𝜔) y 𝜔) → (((A +𝑜 B) +𝑜 y) = (A +𝑜 (B +𝑜 y)) → ((A +𝑜 B) +𝑜 suc y) = (A +𝑜 (B +𝑜 suc y))))
3837expcom 109 . . . . 5 (y 𝜔 → ((A 𝜔 B 𝜔) → (((A +𝑜 B) +𝑜 y) = (A +𝑜 (B +𝑜 y)) → ((A +𝑜 B) +𝑜 suc y) = (A +𝑜 (B +𝑜 suc y)))))
399, 13, 17, 24, 38finds2 4240 . . . 4 (x 𝜔 → ((A 𝜔 B 𝜔) → ((A +𝑜 B) +𝑜 x) = (A +𝑜 (B +𝑜 x))))
405, 39vtoclga 2588 . . 3 (𝐶 𝜔 → ((A 𝜔 B 𝜔) → ((A +𝑜 B) +𝑜 𝐶) = (A +𝑜 (B +𝑜 𝐶))))
4140com12 27 . 2 ((A 𝜔 B 𝜔) → (𝐶 𝜔 → ((A +𝑜 B) +𝑜 𝐶) = (A +𝑜 (B +𝑜 𝐶))))
42413impia 1082 1 ((A 𝜔 B 𝜔 𝐶 𝜔) → ((A +𝑜 B) +𝑜 𝐶) = (A +𝑜 (B +𝑜 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   w3a 867   = wceq 1224   wcel 1367  c0 3193  suc csuc 4041  𝜔com 4229  (class class class)co 5425   +𝑜 coa 5902
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 529  ax-in2 530  ax-io 614  ax-5 1310  ax-7 1311  ax-gen 1312  ax-ie1 1356  ax-ie2 1357  ax-8 1369  ax-10 1370  ax-11 1371  ax-i12 1372  ax-bnd 1373  ax-4 1374  ax-13 1378  ax-14 1379  ax-17 1393  ax-i9 1397  ax-ial 1401  ax-i5r 1402  ax-ext 1996  ax-coll 3836  ax-sep 3839  ax-nul 3847  ax-pow 3891  ax-pr 3908  ax-un 4109  ax-setind 4193  ax-iinf 4227
This theorem depends on definitions:  df-bi 110  df-3an 869  df-tru 1227  df-fal 1230  df-nf 1324  df-sb 1620  df-eu 1877  df-mo 1878  df-clab 2001  df-cleq 2007  df-clel 2010  df-nfc 2141  df-ne 2180  df-ral 2281  df-rex 2282  df-reu 2283  df-rab 2285  df-v 2529  df-sbc 2734  df-csb 2822  df-dif 2889  df-un 2891  df-in 2893  df-ss 2900  df-nul 3194  df-pw 3326  df-sn 3346  df-pr 3347  df-op 3349  df-uni 3545  df-int 3580  df-iun 3623  df-br 3729  df-opab 3783  df-mpt 3784  df-tr 3819  df-id 3994  df-iord 4042  df-on 4044  df-suc 4047  df-iom 4230  df-xp 4267  df-rel 4268  df-cnv 4269  df-co 4270  df-dm 4271  df-rn 4272  df-res 4273  df-ima 4274  df-iota 4783  df-fun 4820  df-fn 4821  df-f 4822  df-f1 4823  df-fo 4824  df-f1o 4825  df-fv 4826  df-ov 5428  df-oprab 5429  df-mpt2 5430  df-1st 5679  df-2nd 5680  df-recs 5831  df-irdg 5867  df-oadd 5909
This theorem is referenced by:  nndi  5969  nnmsucr  5971  addasspig  6177  addassnq0  6304  prarloclemlo  6335
  Copyright terms: Public domain W3C validator