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

Metamath Proof Explorer

Theorem nnmul1com

Description: Multiplication with 1 is commutative for natural numbers, without ax-mulcom . Since ( A x. 1 ) is A by ax-1rid , this is equivalent to remullid for natural numbers, but using fewer axioms (avoiding ax-resscn , ax-addass , ax-mulass , ax-rnegex , ax-pre-lttri , ax-pre-lttrn , ax-pre-ltadd ). (Contributed by SN, 5-Feb-2024)

Ref Expression
Assertion nnmul1com ( 𝐴 ∈ ℕ → ( 1 · 𝐴 ) = ( 𝐴 · 1 ) )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑥 = 1 → ( 1 · 𝑥 ) = ( 1 · 1 ) )
2 id ⊢ ( 𝑥 = 1 → 𝑥 = 1 )
3 1 2 eqeq12d ⊢ ( 𝑥 = 1 → ( ( 1 · 𝑥 ) = 𝑥 ↔ ( 1 · 1 ) = 1 ) )
4 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 1 · 𝑥 ) = ( 1 · 𝑦 ) )
5 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
6 4 5 eqeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 1 · 𝑥 ) = 𝑥 ↔ ( 1 · 𝑦 ) = 𝑦 ) )
7 oveq2 ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( 1 · 𝑥 ) = ( 1 · ( 𝑦 + 1 ) ) )
8 id ⊢ ( 𝑥 = ( 𝑦 + 1 ) → 𝑥 = ( 𝑦 + 1 ) )
9 7 8 eqeq12d ⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 1 · 𝑥 ) = 𝑥 ↔ ( 1 · ( 𝑦 + 1 ) ) = ( 𝑦 + 1 ) ) )
10 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 1 · 𝑥 ) = ( 1 · 𝐴 ) )
11 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
12 10 11 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 1 · 𝑥 ) = 𝑥 ↔ ( 1 · 𝐴 ) = 𝐴 ) )
13 1t1e1ALT ⊢ ( 1 · 1 ) = 1
14 1cnd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 1 · 𝑦 ) = 𝑦 ) → 1 ∈ ℂ )
15 simpl ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 1 · 𝑦 ) = 𝑦 ) → 𝑦 ∈ ℕ )
16 15 nncnd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 1 · 𝑦 ) = 𝑦 ) → 𝑦 ∈ ℂ )
17 14 16 14 adddid ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 1 · 𝑦 ) = 𝑦 ) → ( 1 · ( 𝑦 + 1 ) ) = ( ( 1 · 𝑦 ) + ( 1 · 1 ) ) )
18 simpr ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 1 · 𝑦 ) = 𝑦 ) → ( 1 · 𝑦 ) = 𝑦 )
19 13 a1i ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 1 · 𝑦 ) = 𝑦 ) → ( 1 · 1 ) = 1 )
20 18 19 oveq12d ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 1 · 𝑦 ) = 𝑦 ) → ( ( 1 · 𝑦 ) + ( 1 · 1 ) ) = ( 𝑦 + 1 ) )
21 17 20 eqtrd ⊢ ( ( 𝑦 ∈ ℕ ∧ ( 1 · 𝑦 ) = 𝑦 ) → ( 1 · ( 𝑦 + 1 ) ) = ( 𝑦 + 1 ) )
22 21 ex ⊢ ( 𝑦 ∈ ℕ → ( ( 1 · 𝑦 ) = 𝑦 → ( 1 · ( 𝑦 + 1 ) ) = ( 𝑦 + 1 ) ) )
23 3 6 9 12 13 22 nnind ⊢ ( 𝐴 ∈ ℕ → ( 1 · 𝐴 ) = 𝐴 )
24 nnre ⊢ ( 𝐴 ∈ ℕ → 𝐴 ∈ ℝ )
25 ax-1rid ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )
26 24 25 syl ⊢ ( 𝐴 ∈ ℕ → ( 𝐴 · 1 ) = 𝐴 )
27 23 26 eqtr4d ⊢ ( 𝐴 ∈ ℕ → ( 1 · 𝐴 ) = ( 𝐴 · 1 ) )