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	$$⊢A\in \mathbb{N}\to 1A=A\cdot 1$$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$$⊢x=1\to 1x=1\cdot 1$$
2		id	$$⊢x=1\to x=1$$
3	1 2	eqeq12d	$$⊢x=1\to \left(1x=x\leftrightarrow 1\cdot 1=1\right)$$
4		oveq2	$$⊢x=y\to 1x=1y$$
5		id	$$⊢x=y\to x=y$$
6	4 5	eqeq12d	$$⊢x=y\to \left(1x=x\leftrightarrow 1y=y\right)$$
7		oveq2	$$⊢x=y+1\to 1x=1\left(y+1\right)$$
8		id	$$⊢x=y+1\to x=y+1$$
9	7 8	eqeq12d	$$⊢x=y+1\to \left(1x=x\leftrightarrow 1\left(y+1\right)=y+1\right)$$
10		oveq2	$$⊢x=A\to 1x=1A$$
11		id	$$⊢x=A\to x=A$$
12	10 11	eqeq12d	$$⊢x=A\to \left(1x=x\leftrightarrow 1A=A\right)$$
13		1t1e1ALT	$$⊢1\cdot 1=1$$
14		1cnd	$$⊢\left(y\in \mathbb{N}\wedge 1y=y\right)\to 1\in ℂ$$
15		simpl	$$⊢\left(y\in \mathbb{N}\wedge 1y=y\right)\to y\in \mathbb{N}$$
16	15	nncnd	$$⊢\left(y\in \mathbb{N}\wedge 1y=y\right)\to y\in ℂ$$
17	14 16 14	adddid	$$⊢\left(y\in \mathbb{N}\wedge 1y=y\right)\to 1\left(y+1\right)=1y+1\cdot 1$$
18		simpr	$$⊢\left(y\in \mathbb{N}\wedge 1y=y\right)\to 1y=y$$
19	13	a1i	$$⊢\left(y\in \mathbb{N}\wedge 1y=y\right)\to 1\cdot 1=1$$
20	18 19	oveq12d	$$⊢\left(y\in \mathbb{N}\wedge 1y=y\right)\to 1y+1\cdot 1=y+1$$
21	17 20	eqtrd	$$⊢\left(y\in \mathbb{N}\wedge 1y=y\right)\to 1\left(y+1\right)=y+1$$
22	21	ex	$$⊢y\in \mathbb{N}\to \left(1y=y\to 1\left(y+1\right)=y+1\right)$$
23	3 6 9 12 13 22	nnind	$$⊢A\in \mathbb{N}\to 1A=A$$
24		nnre	$$⊢A\in \mathbb{N}\to A\in ℝ$$
25		ax-1rid	$$⊢A\in ℝ\to A\cdot 1=A$$
26	24 25	syl	$$⊢A\in \mathbb{N}\to A\cdot 1=A$$
27	23 26	eqtr4d	$$⊢A\in \mathbb{N}\to 1A=A\cdot 1$$