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 B 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 x + B = B + x B 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 x + B = B + x B 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 x + B = B + x B 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 x + B = B + x B A + B = B + A
17 nnadd1com B B + 1 = 1 + B
18 17 eqcomd B 1 + B = B + 1
19 oveq1 y + B = B + y y + B + 1 = B + y + 1
20 17 oveq2d B y + B + 1 = y + 1 + B
21 20 adantl y B y + B + 1 = y + 1 + B
22 nncn y y
23 22 adantr y B y
24 nncn B B
25 24 adantl y B B
26 1cnd y B 1
27 23 25 26 addassd y B y + B + 1 = y + B + 1
28 23 26 25 addassd y B y + 1 + B = y + 1 + B
29 21 27 28 3eqtr4d y B y + B + 1 = y + 1 + B
30 25 23 26 addassd y B B + y + 1 = B + y + 1
31 29 30 eqeq12d y B y + B + 1 = B + y + 1 y + 1 + B = B + y + 1
32 19 31 syl5ib y B y + B = B + y y + 1 + B = B + y + 1
33 32 ex y B y + B = B + y y + 1 + B = B + y + 1
34 33 a2d y B y + B = B + y B y + 1 + B = B + y + 1
35 4 8 12 16 18 34 nnind A B A + B = B + A
36 35 imp A B A + B = B + A