Metamath Proof Explorer

Theorem nnaddcom

Description: Addition is commutative for natural numbers. Uses fewer axioms than addcom . (Contributed by Steven Nguyen, 9-Dec-2022)

Ref Expression
Assertion nnaddcom 
|- ( ( A e. NN /\ B e. NN ) -> ( A + B ) = ( B + A ) )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( x = 1 -> ( x + B ) = ( 1 + B ) )
2 oveq2 
 |-  ( x = 1 -> ( B + x ) = ( B + 1 ) )
3 1 2 eqeq12d 
 |-  ( x = 1 -> ( ( x + B ) = ( B + x ) <-> ( 1 + B ) = ( B + 1 ) ) )
4 3 imbi2d 
 |-  ( x = 1 -> ( ( B e. NN -> ( x + B ) = ( B + x ) ) <-> ( B e. NN -> ( 1 + B ) = ( B + 1 ) ) ) )
5 oveq1 
 |-  ( x = y -> ( x + B ) = ( y + B ) )
6 oveq2 
 |-  ( x = y -> ( B + x ) = ( B + y ) )
7 5 6 eqeq12d 
 |-  ( x = y -> ( ( x + B ) = ( B + x ) <-> ( y + B ) = ( B + y ) ) )
8 7 imbi2d 
 |-  ( x = y -> ( ( B e. NN -> ( x + B ) = ( B + x ) ) <-> ( B e. NN -> ( y + B ) = ( B + y ) ) ) )
9 oveq1 
 |-  ( x = ( y + 1 ) -> ( x + B ) = ( ( y + 1 ) + B ) )
10 oveq2 
 |-  ( x = ( y + 1 ) -> ( B + x ) = ( B + ( y + 1 ) ) )
11 9 10 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( x + B ) = ( B + x ) <-> ( ( y + 1 ) + B ) = ( B + ( y + 1 ) ) ) )
12 11 imbi2d 
 |-  ( x = ( y + 1 ) -> ( ( B e. NN -> ( x + B ) = ( B + x ) ) <-> ( B e. NN -> ( ( y + 1 ) + B ) = ( B + ( y + 1 ) ) ) ) )
13 oveq1 
 |-  ( x = A -> ( x + B ) = ( A + B ) )
14 oveq2 
 |-  ( x = A -> ( B + x ) = ( B + A ) )
15 13 14 eqeq12d 
 |-  ( x = A -> ( ( x + B ) = ( B + x ) <-> ( A + B ) = ( B + A ) ) )
16 15 imbi2d 
 |-  ( x = A -> ( ( B e. NN -> ( x + B ) = ( B + x ) ) <-> ( B e. NN -> ( A + B ) = ( B + A ) ) ) )
17 nnadd1com 
 |-  ( B e. NN -> ( B + 1 ) = ( 1 + B ) )
18 17 eqcomd 
 |-  ( B e. NN -> ( 1 + B ) = ( B + 1 ) )
19 oveq1 
 |-  ( ( y + B ) = ( B + y ) -> ( ( y + B ) + 1 ) = ( ( B + y ) + 1 ) )
20 17 oveq2d 
 |-  ( B e. NN -> ( y + ( B + 1 ) ) = ( y + ( 1 + B ) ) )
21 20 adantl 
 |-  ( ( y e. NN /\ B e. NN ) -> ( y + ( B + 1 ) ) = ( y + ( 1 + B ) ) )
22 nncn 
 |-  ( y e. NN -> y e. CC )
23 22 adantr 
 |-  ( ( y e. NN /\ B e. NN ) -> y e. CC )
24 nncn 
 |-  ( B e. NN -> B e. CC )
25 24 adantl 
 |-  ( ( y e. NN /\ B e. NN ) -> B e. CC )
26 1cnd 
 |-  ( ( y e. NN /\ B e. NN ) -> 1 e. CC )
27 23 25 26 addassd 
 |-  ( ( y e. NN /\ B e. NN ) -> ( ( y + B ) + 1 ) = ( y + ( B + 1 ) ) )
28 23 26 25 addassd 
 |-  ( ( y e. NN /\ B e. NN ) -> ( ( y + 1 ) + B ) = ( y + ( 1 + B ) ) )
29 21 27 28 3eqtr4d 
 |-  ( ( y e. NN /\ B e. NN ) -> ( ( y + B ) + 1 ) = ( ( y + 1 ) + B ) )
30 25 23 26 addassd 
 |-  ( ( y e. NN /\ B e. NN ) -> ( ( B + y ) + 1 ) = ( B + ( y + 1 ) ) )
31 29 30 eqeq12d 
 |-  ( ( y e. NN /\ B e. NN ) -> ( ( ( y + B ) + 1 ) = ( ( B + y ) + 1 ) <-> ( ( y + 1 ) + B ) = ( B + ( y + 1 ) ) ) )
32 19 31 imbitrid 
 |-  ( ( y e. NN /\ B e. NN ) -> ( ( y + B ) = ( B + y ) -> ( ( y + 1 ) + B ) = ( B + ( y + 1 ) ) ) )
33 32 ex 
 |-  ( y e. NN -> ( B e. NN -> ( ( y + B ) = ( B + y ) -> ( ( y + 1 ) + B ) = ( B + ( y + 1 ) ) ) ) )
34 33 a2d 
 |-  ( y e. NN -> ( ( B e. NN -> ( y + B ) = ( B + y ) ) -> ( B e. NN -> ( ( y + 1 ) + B ) = ( B + ( y + 1 ) ) ) ) )
35 4 8 12 16 18 34 nnind 
 |-  ( A e. NN -> ( B e. NN -> ( A + B ) = ( B + A ) ) )
36 35 imp 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A + B ) = ( B + A ) )