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 
|- ( ( A e. _om /\ B e. _om ) -> ( A +o B ) = ( B +o A ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = A -> ( x +o B ) = ( A +o B ) )
2 oveq2 
 |-  ( x = A -> ( B +o x ) = ( B +o A ) )
3 1 2 eqeq12d 
 |-  ( x = A -> ( ( x +o B ) = ( B +o x ) <-> ( A +o B ) = ( B +o A ) ) )
4 3 imbi2d 
 |-  ( x = A -> ( ( B e. _om -> ( x +o B ) = ( B +o x ) ) <-> ( B e. _om -> ( A +o B ) = ( B +o A ) ) ) )
5 oveq1 
 |-  ( x = (/) -> ( x +o B ) = ( (/) +o B ) )
6 oveq2 
 |-  ( x = (/) -> ( B +o x ) = ( B +o (/) ) )
7 5 6 eqeq12d 
 |-  ( x = (/) -> ( ( x +o B ) = ( B +o x ) <-> ( (/) +o B ) = ( B +o (/) ) ) )
8 oveq1 
 |-  ( x = y -> ( x +o B ) = ( y +o B ) )
9 oveq2 
 |-  ( x = y -> ( B +o x ) = ( B +o y ) )
10 8 9 eqeq12d 
 |-  ( x = y -> ( ( x +o B ) = ( B +o x ) <-> ( y +o B ) = ( B +o y ) ) )
11 oveq1 
 |-  ( x = suc y -> ( x +o B ) = ( suc y +o B ) )
12 oveq2 
 |-  ( x = suc y -> ( B +o x ) = ( B +o suc y ) )
13 11 12 eqeq12d 
 |-  ( x = suc y -> ( ( x +o B ) = ( B +o x ) <-> ( suc y +o B ) = ( B +o suc y ) ) )
14 nna0r 
 |-  ( B e. _om -> ( (/) +o B ) = B )
15 nna0 
 |-  ( B e. _om -> ( B +o (/) ) = B )
16 14 15 eqtr4d 
 |-  ( B e. _om -> ( (/) +o B ) = ( B +o (/) ) )
17 suceq 
 |-  ( ( y +o B ) = ( B +o y ) -> suc ( y +o B ) = suc ( B +o y ) )
18 oveq2 
 |-  ( x = B -> ( suc y +o x ) = ( suc y +o B ) )
19 oveq2 
 |-  ( x = B -> ( y +o x ) = ( y +o B ) )
20 suceq 
 |-  ( ( y +o x ) = ( y +o B ) -> suc ( y +o x ) = suc ( y +o B ) )
21 19 20 syl 
 |-  ( x = B -> suc ( y +o x ) = suc ( y +o B ) )
22 18 21 eqeq12d 
 |-  ( x = B -> ( ( suc y +o x ) = suc ( y +o x ) <-> ( suc y +o B ) = suc ( y +o B ) ) )
23 22 imbi2d 
 |-  ( x = B -> ( ( y e. _om -> ( suc y +o x ) = suc ( y +o x ) ) <-> ( y e. _om -> ( suc y +o B ) = suc ( y +o B ) ) ) )
24 oveq2 
 |-  ( x = (/) -> ( suc y +o x ) = ( suc y +o (/) ) )
25 oveq2 
 |-  ( x = (/) -> ( y +o x ) = ( y +o (/) ) )
26 suceq 
 |-  ( ( y +o x ) = ( y +o (/) ) -> suc ( y +o x ) = suc ( y +o (/) ) )
27 25 26 syl 
 |-  ( x = (/) -> suc ( y +o x ) = suc ( y +o (/) ) )
28 24 27 eqeq12d 
 |-  ( x = (/) -> ( ( suc y +o x ) = suc ( y +o x ) <-> ( suc y +o (/) ) = suc ( y +o (/) ) ) )
29 oveq2 
 |-  ( x = z -> ( suc y +o x ) = ( suc y +o z ) )
30 oveq2 
 |-  ( x = z -> ( y +o x ) = ( y +o z ) )
31 suceq 
 |-  ( ( y +o x ) = ( y +o z ) -> suc ( y +o x ) = suc ( y +o z ) )
32 30 31 syl 
 |-  ( x = z -> suc ( y +o x ) = suc ( y +o z ) )
33 29 32 eqeq12d 
 |-  ( x = z -> ( ( suc y +o x ) = suc ( y +o x ) <-> ( suc y +o z ) = suc ( y +o z ) ) )
34 oveq2 
 |-  ( x = suc z -> ( suc y +o x ) = ( suc y +o suc z ) )
35 oveq2 
 |-  ( x = suc z -> ( y +o x ) = ( y +o suc z ) )
36 suceq 
 |-  ( ( y +o x ) = ( y +o suc z ) -> suc ( y +o x ) = suc ( y +o suc z ) )
37 35 36 syl 
 |-  ( x = suc z -> suc ( y +o x ) = suc ( y +o suc z ) )
38 34 37 eqeq12d 
 |-  ( x = suc z -> ( ( suc y +o x ) = suc ( y +o x ) <-> ( suc y +o suc z ) = suc ( y +o suc z ) ) )
39 peano2 
 |-  ( y e. _om -> suc y e. _om )
40 nna0 
 |-  ( suc y e. _om -> ( suc y +o (/) ) = suc y )
41 39 40 syl 
 |-  ( y e. _om -> ( suc y +o (/) ) = suc y )
42 nna0 
 |-  ( y e. _om -> ( y +o (/) ) = y )
43 suceq 
 |-  ( ( y +o (/) ) = y -> suc ( y +o (/) ) = suc y )
44 42 43 syl 
 |-  ( y e. _om -> suc ( y +o (/) ) = suc y )
45 41 44 eqtr4d 
 |-  ( y e. _om -> ( suc y +o (/) ) = suc ( y +o (/) ) )
46 suceq 
 |-  ( ( suc y +o z ) = suc ( y +o z ) -> suc ( suc y +o z ) = suc suc ( y +o z ) )
47 nnasuc 
 |-  ( ( suc y e. _om /\ z e. _om ) -> ( suc y +o suc z ) = suc ( suc y +o z ) )
48 39 47 sylan 
 |-  ( ( y e. _om /\ z e. _om ) -> ( suc y +o suc z ) = suc ( suc y +o z ) )
49 nnasuc 
 |-  ( ( y e. _om /\ z e. _om ) -> ( y +o suc z ) = suc ( y +o z ) )
50 suceq 
 |-  ( ( y +o suc z ) = suc ( y +o z ) -> suc ( y +o suc z ) = suc suc ( y +o z ) )
51 49 50 syl 
 |-  ( ( y e. _om /\ z e. _om ) -> suc ( y +o suc z ) = suc suc ( y +o z ) )
52 48 51 eqeq12d 
 |-  ( ( y e. _om /\ z e. _om ) -> ( ( suc y +o suc z ) = suc ( y +o suc z ) <-> suc ( suc y +o z ) = suc suc ( y +o z ) ) )
53 46 52 imbitrrid 
 |-  ( ( y e. _om /\ z e. _om ) -> ( ( suc y +o z ) = suc ( y +o z ) -> ( suc y +o suc z ) = suc ( y +o suc z ) ) )
54 53 expcom 
 |-  ( z e. _om -> ( y e. _om -> ( ( suc y +o z ) = suc ( y +o z ) -> ( suc y +o suc z ) = suc ( y +o suc z ) ) ) )
55 28 33 38 45 54 finds2 
 |-  ( x e. _om -> ( y e. _om -> ( suc y +o x ) = suc ( y +o x ) ) )
56 23 55 vtoclga 
 |-  ( B e. _om -> ( y e. _om -> ( suc y +o B ) = suc ( y +o B ) ) )
57 56 imp 
 |-  ( ( B e. _om /\ y e. _om ) -> ( suc y +o B ) = suc ( y +o B ) )
58 nnasuc 
 |-  ( ( B e. _om /\ y e. _om ) -> ( B +o suc y ) = suc ( B +o y ) )
59 57 58 eqeq12d 
 |-  ( ( B e. _om /\ y e. _om ) -> ( ( suc y +o B ) = ( B +o suc y ) <-> suc ( y +o B ) = suc ( B +o y ) ) )
60 17 59 imbitrrid 
 |-  ( ( B e. _om /\ y e. _om ) -> ( ( y +o B ) = ( B +o y ) -> ( suc y +o B ) = ( B +o suc y ) ) )
61 60 expcom 
 |-  ( y e. _om -> ( B e. _om -> ( ( y +o B ) = ( B +o y ) -> ( suc y +o B ) = ( B +o suc y ) ) ) )
62 7 10 13 16 61 finds2 
 |-  ( x e. _om -> ( B e. _om -> ( x +o B ) = ( B +o x ) ) )
63 4 62 vtoclga 
 |-  ( A e. _om -> ( B e. _om -> ( A +o B ) = ( B +o A ) ) )
64 63 imp 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A +o B ) = ( B +o A ) )