This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnmulcom

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

Ref Expression
Assertion nnmulcom ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ ( 𝑥 = 1 → ( 𝑥 · 𝐵 ) = ( 1 · 𝐵 ) )
2 oveq2 ⊢ ( 𝑥 = 1 → ( 𝐵 · 𝑥 ) = ( 𝐵 · 1 ) )
3 1 2 eqeq12d ⊢ ( 𝑥 = 1 → ( ( 𝑥 · 𝐵 ) = ( 𝐵 · 𝑥 ) ↔ ( 1 · 𝐵 ) = ( 𝐵 · 1 ) ) )
4 3 imbi2d ⊢ ( 𝑥 = 1 → ( ( 𝐵 ∈ ℕ → ( 𝑥 · 𝐵 ) = ( 𝐵 · 𝑥 ) ) ↔ ( 𝐵 ∈ ℕ → ( 1 · 𝐵 ) = ( 𝐵 · 1 ) ) ) )
5 oveq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 · 𝐵 ) = ( 𝑦 · 𝐵 ) )
6 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 · 𝑥 ) = ( 𝐵 · 𝑦 ) )
7 5 6 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 · 𝐵 ) = ( 𝐵 · 𝑥 ) ↔ ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) ) )
8 7 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐵 ∈ ℕ → ( 𝑥 · 𝐵 ) = ( 𝐵 · 𝑥 ) ) ↔ ( 𝐵 ∈ ℕ → ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) ) ) )
9 oveq1 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 · 𝐵 ) = ( ( 𝑦 + 1 ) · 𝐵 ) )
10 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 𝐵 · 𝑥 ) = ( 𝐵 · ( 𝑦 + 1 ) ) )
11 9 10 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝑥 · 𝐵 ) = ( 𝐵 · 𝑥 ) ↔ ( ( 𝑦 + 1 ) · 𝐵 ) = ( 𝐵 · ( 𝑦 + 1 ) ) ) )
12 11 imbi2d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝐵 ∈ ℕ → ( 𝑥 · 𝐵 ) = ( 𝐵 · 𝑥 ) ) ↔ ( 𝐵 ∈ ℕ → ( ( 𝑦 + 1 ) · 𝐵 ) = ( 𝐵 · ( 𝑦 + 1 ) ) ) ) )
13 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 · 𝐵 ) = ( 𝐴 · 𝐵 ) )
14 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐵 · 𝑥 ) = ( 𝐵 · 𝐴 ) )
15 13 14 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 · 𝐵 ) = ( 𝐵 · 𝑥 ) ↔ ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) ) )
16 15 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐵 ∈ ℕ → ( 𝑥 · 𝐵 ) = ( 𝐵 · 𝑥 ) ) ↔ ( 𝐵 ∈ ℕ → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) ) ) )
17 nnmul1com ⊢ ( 𝐵 ∈ ℕ → ( 1 · 𝐵 ) = ( 𝐵 · 1 ) )
18 simp3 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) ) → ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) )
19 17 3ad2ant2 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) ) → ( 1 · 𝐵 ) = ( 𝐵 · 1 ) )
20 18 19 oveq12d ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) ) → ( ( 𝑦 · 𝐵 ) + ( 1 · 𝐵 ) ) = ( ( 𝐵 · 𝑦 ) + ( 𝐵 · 1 ) ) )
21 simp1 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) ) → 𝑦 ∈ ℕ )
22 1nn ⊢ 1 ∈ ℕ
23 22 a1i ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) ) → 1 ∈ ℕ )
24 simp2 ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) ) → 𝐵 ∈ ℕ )
25 nnadddir ⊢ ( ( 𝑦 ∈ ℕ ∧ 1 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( ( 𝑦 + 1 ) · 𝐵 ) = ( ( 𝑦 · 𝐵 ) + ( 1 · 𝐵 ) ) )
26 21 23 24 25 syl3anc ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) ) → ( ( 𝑦 + 1 ) · 𝐵 ) = ( ( 𝑦 · 𝐵 ) + ( 1 · 𝐵 ) ) )
27 24 nncnd ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) ) → 𝐵 ∈ ℂ )
28 21 nncnd ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) ) → 𝑦 ∈ ℂ )
29 1cnd ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) ) → 1 ∈ ℂ )
30 27 28 29 adddid ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) ) → ( 𝐵 · ( 𝑦 + 1 ) ) = ( ( 𝐵 · 𝑦 ) + ( 𝐵 · 1 ) ) )
31 20 26 30 3eqtr4d ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) ) → ( ( 𝑦 + 1 ) · 𝐵 ) = ( 𝐵 · ( 𝑦 + 1 ) ) )
32 31 3exp ⊢ ( 𝑦 ∈ ℕ → ( 𝐵 ∈ ℕ → ( ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) → ( ( 𝑦 + 1 ) · 𝐵 ) = ( 𝐵 · ( 𝑦 + 1 ) ) ) ) )
33 32 a2d ⊢ ( 𝑦 ∈ ℕ → ( ( 𝐵 ∈ ℕ → ( 𝑦 · 𝐵 ) = ( 𝐵 · 𝑦 ) ) → ( 𝐵 ∈ ℕ → ( ( 𝑦 + 1 ) · 𝐵 ) = ( 𝐵 · ( 𝑦 + 1 ) ) ) ) )
34 4 8 12 16 17 33 nnind ⊢ ( 𝐴 ∈ ℕ → ( 𝐵 ∈ ℕ → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) ) )
35 34 imp ⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ( 𝐴 · 𝐵 ) = ( 𝐵 · 𝐴 ) )