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 remulid2 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 ) )