Metamath Proof Explorer

Theorem nnaass

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)

Ref Expression
Assertion nnaass 
|- ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( A +o B ) +o C ) = ( A +o ( B +o C ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = C -> ( ( A +o B ) +o x ) = ( ( A +o B ) +o C ) )
2 oveq2 
 |-  ( x = C -> ( B +o x ) = ( B +o C ) )
3 2 oveq2d 
 |-  ( x = C -> ( A +o ( B +o x ) ) = ( A +o ( B +o C ) ) )
4 1 3 eqeq12d 
 |-  ( x = C -> ( ( ( A +o B ) +o x ) = ( A +o ( B +o x ) ) <-> ( ( A +o B ) +o C ) = ( A +o ( B +o C ) ) ) )
5 4 imbi2d 
 |-  ( x = C -> ( ( ( A e. _om /\ B e. _om ) -> ( ( A +o B ) +o x ) = ( A +o ( B +o x ) ) ) <-> ( ( A e. _om /\ B e. _om ) -> ( ( A +o B ) +o C ) = ( A +o ( B +o C ) ) ) ) )
6 oveq2 
 |-  ( x = (/) -> ( ( A +o B ) +o x ) = ( ( A +o B ) +o (/) ) )
7 oveq2 
 |-  ( x = (/) -> ( B +o x ) = ( B +o (/) ) )
8 7 oveq2d 
 |-  ( x = (/) -> ( A +o ( B +o x ) ) = ( A +o ( B +o (/) ) ) )
9 6 8 eqeq12d 
 |-  ( x = (/) -> ( ( ( A +o B ) +o x ) = ( A +o ( B +o x ) ) <-> ( ( A +o B ) +o (/) ) = ( A +o ( B +o (/) ) ) ) )
10 oveq2 
 |-  ( x = y -> ( ( A +o B ) +o x ) = ( ( A +o B ) +o y ) )
11 oveq2 
 |-  ( x = y -> ( B +o x ) = ( B +o y ) )
12 11 oveq2d 
 |-  ( x = y -> ( A +o ( B +o x ) ) = ( A +o ( B +o y ) ) )
13 10 12 eqeq12d 
 |-  ( x = y -> ( ( ( A +o B ) +o x ) = ( A +o ( B +o x ) ) <-> ( ( A +o B ) +o y ) = ( A +o ( B +o y ) ) ) )
14 oveq2 
 |-  ( x = suc y -> ( ( A +o B ) +o x ) = ( ( A +o B ) +o suc y ) )
15 oveq2 
 |-  ( x = suc y -> ( B +o x ) = ( B +o suc y ) )
16 15 oveq2d 
 |-  ( x = suc y -> ( A +o ( B +o x ) ) = ( A +o ( B +o suc y ) ) )
17 14 16 eqeq12d 
 |-  ( x = suc y -> ( ( ( A +o B ) +o x ) = ( A +o ( B +o x ) ) <-> ( ( A +o B ) +o suc y ) = ( A +o ( B +o suc y ) ) ) )
18 nnacl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A +o B ) e. _om )
19 nna0 
 |-  ( ( A +o B ) e. _om -> ( ( A +o B ) +o (/) ) = ( A +o B ) )
20 18 19 syl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( A +o B ) +o (/) ) = ( A +o B ) )
21 nna0 
 |-  ( B e. _om -> ( B +o (/) ) = B )
22 21 oveq2d 
 |-  ( B e. _om -> ( A +o ( B +o (/) ) ) = ( A +o B ) )
23 22 adantl 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A +o ( B +o (/) ) ) = ( A +o B ) )
24 20 23 eqtr4d 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( A +o B ) +o (/) ) = ( A +o ( B +o (/) ) ) )
25 suceq 
 |-  ( ( ( A +o B ) +o y ) = ( A +o ( B +o y ) ) -> suc ( ( A +o B ) +o y ) = suc ( A +o ( B +o y ) ) )
26 nnasuc 
 |-  ( ( ( A +o B ) e. _om /\ y e. _om ) -> ( ( A +o B ) +o suc y ) = suc ( ( A +o B ) +o y ) )
27 18 26 sylan 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ y e. _om ) -> ( ( A +o B ) +o suc y ) = suc ( ( A +o B ) +o y ) )
28 nnasuc 
 |-  ( ( B e. _om /\ y e. _om ) -> ( B +o suc y ) = suc ( B +o y ) )
29 28 oveq2d 
 |-  ( ( B e. _om /\ y e. _om ) -> ( A +o ( B +o suc y ) ) = ( A +o suc ( B +o y ) ) )
30 29 adantl 
 |-  ( ( A e. _om /\ ( B e. _om /\ y e. _om ) ) -> ( A +o ( B +o suc y ) ) = ( A +o suc ( B +o y ) ) )
31 nnacl 
 |-  ( ( B e. _om /\ y e. _om ) -> ( B +o y ) e. _om )
32 nnasuc 
 |-  ( ( A e. _om /\ ( B +o y ) e. _om ) -> ( A +o suc ( B +o y ) ) = suc ( A +o ( B +o y ) ) )
33 31 32 sylan2 
 |-  ( ( A e. _om /\ ( B e. _om /\ y e. _om ) ) -> ( A +o suc ( B +o y ) ) = suc ( A +o ( B +o y ) ) )
34 30 33 eqtrd 
 |-  ( ( A e. _om /\ ( B e. _om /\ y e. _om ) ) -> ( A +o ( B +o suc y ) ) = suc ( A +o ( B +o y ) ) )
35 34 anassrs 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ y e. _om ) -> ( A +o ( B +o suc y ) ) = suc ( A +o ( B +o y ) ) )
36 27 35 eqeq12d 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ y e. _om ) -> ( ( ( A +o B ) +o suc y ) = ( A +o ( B +o suc y ) ) <-> suc ( ( A +o B ) +o y ) = suc ( A +o ( B +o y ) ) ) )
37 25 36 imbitrrid 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ y e. _om ) -> ( ( ( A +o B ) +o y ) = ( A +o ( B +o y ) ) -> ( ( A +o B ) +o suc y ) = ( A +o ( B +o suc y ) ) ) )
38 37 expcom 
 |-  ( y e. _om -> ( ( A e. _om /\ B e. _om ) -> ( ( ( A +o B ) +o y ) = ( A +o ( B +o y ) ) -> ( ( A +o B ) +o suc y ) = ( A +o ( B +o suc y ) ) ) ) )
39 9 13 17 24 38 finds2 
 |-  ( x e. _om -> ( ( A e. _om /\ B e. _om ) -> ( ( A +o B ) +o x ) = ( A +o ( B +o x ) ) ) )
40 5 39 vtoclga 
 |-  ( C e. _om -> ( ( A e. _om /\ B e. _om ) -> ( ( A +o B ) +o C ) = ( A +o ( B +o C ) ) ) )
41 40 com12 
 |-  ( ( A e. _om /\ B e. _om ) -> ( C e. _om -> ( ( A +o B ) +o C ) = ( A +o ( B +o C ) ) ) )
42 41 3impia 
 |-  ( ( A e. _om /\ B e. _om /\ C e. _om ) -> ( ( A +o B ) +o C ) = ( A +o ( B +o C ) ) )