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 imbitrid ⊢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