Metamath Proof Explorer

Theorem nnmulcom

Description: Multiplication is commutative for natural numbers. (Contributed by SN, 5-Feb-2024)

Ref Expression
Assertion nnmulcom ⊢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 nnmul1com ⊢B∈ℕ→1⁢B=B⋅1
18 simp3 ⊢y∈ℕ∧B∈ℕ∧y⁢B=B⁢y→y⁢B=B⁢y
19 17 3ad2ant2 ⊢y∈ℕ∧B∈ℕ∧y⁢B=B⁢y→1⁢B=B⋅1
20 18 19 oveq12d ⊢y∈ℕ∧B∈ℕ∧y⁢B=B⁢y→y⁢B+1⁢B=B⁢y+B⋅1
21 simp1 ⊢y∈ℕ∧B∈ℕ∧y⁢B=B⁢y→y∈ℕ
22 1nn ⊢1∈ℕ
23 22 a1i ⊢y∈ℕ∧B∈ℕ∧y⁢B=B⁢y→1∈ℕ
24 simp2 ⊢y∈ℕ∧B∈ℕ∧y⁢B=B⁢y→B∈ℕ
25 nnadddir ⊢y∈ℕ∧1∈ℕ∧B∈ℕ→y+1⁢B=y⁢B+1⁢B
26 21 23 24 25 syl3anc ⊢y∈ℕ∧B∈ℕ∧y⁢B=B⁢y→y+1⁢B=y⁢B+1⁢B
27 24 nncnd ⊢y∈ℕ∧B∈ℕ∧y⁢B=B⁢y→B∈ℂ
28 21 nncnd ⊢y∈ℕ∧B∈ℕ∧y⁢B=B⁢y→y∈ℂ
29 1cnd ⊢y∈ℕ∧B∈ℕ∧y⁢B=B⁢y→1∈ℂ
30 27 28 29 adddid ⊢y∈ℕ∧B∈ℕ∧y⁢B=B⁢y→B⁢y+1=B⁢y+B⋅1
31 20 26 30 3eqtr4d ⊢y∈ℕ∧B∈ℕ∧y⁢B=B⁢y→y+1⁢B=B⁢y+1
32 31 3exp ⊢y∈ℕ→B∈ℕ→y⁢B=B⁢y→y+1⁢B=B⁢y+1
33 32 a2d ⊢y∈ℕ→B∈ℕ→y⁢B=B⁢y→B∈ℕ→y+1⁢B=B⁢y+1
34 4 8 12 16 17 33 nnind ⊢A∈ℕ→B∈ℕ→A⁢B=B⁢A
35 34 imp ⊢A∈ℕ∧B∈ℕ→A⁢B=B⁢A