Metamath Proof Explorer

Theorem nnacom

Description: Addition of natural numbers is commutative. Theorem 4K(2) of Enderton p. 81. (Contributed by NM, 6-May-1995) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnacom ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 +o 𝐵 ) = ( 𝐵 +o 𝐴 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 +o 𝐵 ) = ( 𝐴 +o 𝐵 ) )
2 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o 𝐴 ) )
3 1 2 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 +o 𝐵 ) = ( 𝐵 +o 𝑥 ) ↔ ( 𝐴 +o 𝐵 ) = ( 𝐵 +o 𝐴 ) ) )
4 3 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐵 ∈ ω → ( 𝑥 +o 𝐵 ) = ( 𝐵 +o 𝑥 ) ) ↔ ( 𝐵 ∈ ω → ( 𝐴 +o 𝐵 ) = ( 𝐵 +o 𝐴 ) ) ) )
5 oveq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 +o 𝐵 ) = ( ∅ +o 𝐵 ) )
6 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o ∅ ) )
7 5 6 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( 𝑥 +o 𝐵 ) = ( 𝐵 +o 𝑥 ) ↔ ( ∅ +o 𝐵 ) = ( 𝐵 +o ∅ ) ) )
8 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 +o 𝐵 ) = ( 𝑦 +o 𝐵 ) )
9 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o 𝑦 ) )
10 8 9 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 +o 𝐵 ) = ( 𝐵 +o 𝑥 ) ↔ ( 𝑦 +o 𝐵 ) = ( 𝐵 +o 𝑦 ) ) )
11 oveq1 ⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 +o 𝐵 ) = ( suc 𝑦 +o 𝐵 ) )
12 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐵 +o 𝑥 ) = ( 𝐵 +o suc 𝑦 ) )
13 11 12 eqeq12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑥 +o 𝐵 ) = ( 𝐵 +o 𝑥 ) ↔ ( suc 𝑦 +o 𝐵 ) = ( 𝐵 +o suc 𝑦 ) ) )
14 nna0r ⊢ ( 𝐵 ∈ ω → ( ∅ +o 𝐵 ) = 𝐵 )
15 nna0 ⊢ ( 𝐵 ∈ ω → ( 𝐵 +o ∅ ) = 𝐵 )
16 14 15 eqtr4d ⊢ ( 𝐵 ∈ ω → ( ∅ +o 𝐵 ) = ( 𝐵 +o ∅ ) )
17 suceq ⊢ ( ( 𝑦 +o 𝐵 ) = ( 𝐵 +o 𝑦 ) → suc ( 𝑦 +o 𝐵 ) = suc ( 𝐵 +o 𝑦 ) )
18 oveq2 ⊢ ( 𝑥 = 𝐵 → ( suc 𝑦 +o 𝑥 ) = ( suc 𝑦 +o 𝐵 ) )
19 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝑦 +o 𝑥 ) = ( 𝑦 +o 𝐵 ) )
20 suceq ⊢ ( ( 𝑦 +o 𝑥 ) = ( 𝑦 +o 𝐵 ) → suc ( 𝑦 +o 𝑥 ) = suc ( 𝑦 +o 𝐵 ) )
21 19 20 syl ⊢ ( 𝑥 = 𝐵 → suc ( 𝑦 +o 𝑥 ) = suc ( 𝑦 +o 𝐵 ) )
22 18 21 eqeq12d ⊢ ( 𝑥 = 𝐵 → ( ( suc 𝑦 +o 𝑥 ) = suc ( 𝑦 +o 𝑥 ) ↔ ( suc 𝑦 +o 𝐵 ) = suc ( 𝑦 +o 𝐵 ) ) )
23 22 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝑦 ∈ ω → ( suc 𝑦 +o 𝑥 ) = suc ( 𝑦 +o 𝑥 ) ) ↔ ( 𝑦 ∈ ω → ( suc 𝑦 +o 𝐵 ) = suc ( 𝑦 +o 𝐵 ) ) ) )
24 oveq2 ⊢ ( 𝑥 = ∅ → ( suc 𝑦 +o 𝑥 ) = ( suc 𝑦 +o ∅ ) )
25 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝑦 +o 𝑥 ) = ( 𝑦 +o ∅ ) )
26 suceq ⊢ ( ( 𝑦 +o 𝑥 ) = ( 𝑦 +o ∅ ) → suc ( 𝑦 +o 𝑥 ) = suc ( 𝑦 +o ∅ ) )
27 25 26 syl ⊢ ( 𝑥 = ∅ → suc ( 𝑦 +o 𝑥 ) = suc ( 𝑦 +o ∅ ) )
28 24 27 eqeq12d ⊢ ( 𝑥 = ∅ → ( ( suc 𝑦 +o 𝑥 ) = suc ( 𝑦 +o 𝑥 ) ↔ ( suc 𝑦 +o ∅ ) = suc ( 𝑦 +o ∅ ) ) )
29 oveq2 ⊢ ( 𝑥 = 𝑧 → ( suc 𝑦 +o 𝑥 ) = ( suc 𝑦 +o 𝑧 ) )
30 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝑦 +o 𝑥 ) = ( 𝑦 +o 𝑧 ) )
31 suceq ⊢ ( ( 𝑦 +o 𝑥 ) = ( 𝑦 +o 𝑧 ) → suc ( 𝑦 +o 𝑥 ) = suc ( 𝑦 +o 𝑧 ) )
32 30 31 syl ⊢ ( 𝑥 = 𝑧 → suc ( 𝑦 +o 𝑥 ) = suc ( 𝑦 +o 𝑧 ) )
33 29 32 eqeq12d ⊢ ( 𝑥 = 𝑧 → ( ( suc 𝑦 +o 𝑥 ) = suc ( 𝑦 +o 𝑥 ) ↔ ( suc 𝑦 +o 𝑧 ) = suc ( 𝑦 +o 𝑧 ) ) )
34 oveq2 ⊢ ( 𝑥 = suc 𝑧 → ( suc 𝑦 +o 𝑥 ) = ( suc 𝑦 +o suc 𝑧 ) )
35 oveq2 ⊢ ( 𝑥 = suc 𝑧 → ( 𝑦 +o 𝑥 ) = ( 𝑦 +o suc 𝑧 ) )
36 suceq ⊢ ( ( 𝑦 +o 𝑥 ) = ( 𝑦 +o suc 𝑧 ) → suc ( 𝑦 +o 𝑥 ) = suc ( 𝑦 +o suc 𝑧 ) )
37 35 36 syl ⊢ ( 𝑥 = suc 𝑧 → suc ( 𝑦 +o 𝑥 ) = suc ( 𝑦 +o suc 𝑧 ) )
38 34 37 eqeq12d ⊢ ( 𝑥 = suc 𝑧 → ( ( suc 𝑦 +o 𝑥 ) = suc ( 𝑦 +o 𝑥 ) ↔ ( suc 𝑦 +o suc 𝑧 ) = suc ( 𝑦 +o suc 𝑧 ) ) )
39 peano2 ⊢ ( 𝑦 ∈ ω → suc 𝑦 ∈ ω )
40 nna0 ⊢ ( suc 𝑦 ∈ ω → ( suc 𝑦 +o ∅ ) = suc 𝑦 )
41 39 40 syl ⊢ ( 𝑦 ∈ ω → ( suc 𝑦 +o ∅ ) = suc 𝑦 )
42 nna0 ⊢ ( 𝑦 ∈ ω → ( 𝑦 +o ∅ ) = 𝑦 )
43 suceq ⊢ ( ( 𝑦 +o ∅ ) = 𝑦 → suc ( 𝑦 +o ∅ ) = suc 𝑦 )
44 42 43 syl ⊢ ( 𝑦 ∈ ω → suc ( 𝑦 +o ∅ ) = suc 𝑦 )
45 41 44 eqtr4d ⊢ ( 𝑦 ∈ ω → ( suc 𝑦 +o ∅ ) = suc ( 𝑦 +o ∅ ) )
46 suceq ⊢ ( ( suc 𝑦 +o 𝑧 ) = suc ( 𝑦 +o 𝑧 ) → suc ( suc 𝑦 +o 𝑧 ) = suc suc ( 𝑦 +o 𝑧 ) )
47 nnasuc ⊢ ( ( suc 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( suc 𝑦 +o suc 𝑧 ) = suc ( suc 𝑦 +o 𝑧 ) )
48 39 47 sylan ⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( suc 𝑦 +o suc 𝑧 ) = suc ( suc 𝑦 +o 𝑧 ) )
49 nnasuc ⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( 𝑦 +o suc 𝑧 ) = suc ( 𝑦 +o 𝑧 ) )
50 suceq ⊢ ( ( 𝑦 +o suc 𝑧 ) = suc ( 𝑦 +o 𝑧 ) → suc ( 𝑦 +o suc 𝑧 ) = suc suc ( 𝑦 +o 𝑧 ) )
51 49 50 syl ⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → suc ( 𝑦 +o suc 𝑧 ) = suc suc ( 𝑦 +o 𝑧 ) )
52 48 51 eqeq12d ⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( ( suc 𝑦 +o suc 𝑧 ) = suc ( 𝑦 +o suc 𝑧 ) ↔ suc ( suc 𝑦 +o 𝑧 ) = suc suc ( 𝑦 +o 𝑧 ) ) )
53 46 52 imbitrrid ⊢ ( ( 𝑦 ∈ ω ∧ 𝑧 ∈ ω ) → ( ( suc 𝑦 +o 𝑧 ) = suc ( 𝑦 +o 𝑧 ) → ( suc 𝑦 +o suc 𝑧 ) = suc ( 𝑦 +o suc 𝑧 ) ) )
54 53 expcom ⊢ ( 𝑧 ∈ ω → ( 𝑦 ∈ ω → ( ( suc 𝑦 +o 𝑧 ) = suc ( 𝑦 +o 𝑧 ) → ( suc 𝑦 +o suc 𝑧 ) = suc ( 𝑦 +o suc 𝑧 ) ) ) )
55 28 33 38 45 54 finds2 ⊢ ( 𝑥 ∈ ω → ( 𝑦 ∈ ω → ( suc 𝑦 +o 𝑥 ) = suc ( 𝑦 +o 𝑥 ) ) )
56 23 55 vtoclga ⊢ ( 𝐵 ∈ ω → ( 𝑦 ∈ ω → ( suc 𝑦 +o 𝐵 ) = suc ( 𝑦 +o 𝐵 ) ) )
57 56 imp ⊢ ( ( 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( suc 𝑦 +o 𝐵 ) = suc ( 𝑦 +o 𝐵 ) )
58 nnasuc ⊢ ( ( 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐵 +o suc 𝑦 ) = suc ( 𝐵 +o 𝑦 ) )
59 57 58 eqeq12d ⊢ ( ( 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( suc 𝑦 +o 𝐵 ) = ( 𝐵 +o suc 𝑦 ) ↔ suc ( 𝑦 +o 𝐵 ) = suc ( 𝐵 +o 𝑦 ) ) )
60 17 59 imbitrrid ⊢ ( ( 𝐵 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝑦 +o 𝐵 ) = ( 𝐵 +o 𝑦 ) → ( suc 𝑦 +o 𝐵 ) = ( 𝐵 +o suc 𝑦 ) ) )
61 60 expcom ⊢ ( 𝑦 ∈ ω → ( 𝐵 ∈ ω → ( ( 𝑦 +o 𝐵 ) = ( 𝐵 +o 𝑦 ) → ( suc 𝑦 +o 𝐵 ) = ( 𝐵 +o suc 𝑦 ) ) ) )
62 7 10 13 16 61 finds2 ⊢ ( 𝑥 ∈ ω → ( 𝐵 ∈ ω → ( 𝑥 +o 𝐵 ) = ( 𝐵 +o 𝑥 ) ) )
63 4 62 vtoclga ⊢ ( 𝐴 ∈ ω → ( 𝐵 ∈ ω → ( 𝐴 +o 𝐵 ) = ( 𝐵 +o 𝐴 ) ) )
64 63 imp ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 +o 𝐵 ) = ( 𝐵 +o 𝐴 ) )