Theorem nnm1

Description: Multiply an element of _om by 1o . (Contributed by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Assertion	nnm1	$$⊢A\in \mathrm{\omega }\to A{\cdot }_{𝑜}{1}_{𝑜}=A$$

Proof

Step	Hyp	Ref	Expression
1		df-1o	$$⊢1_{𝑜}=\mathrm{suc}\varnothing$$
2	1	oveq2i	$$⊢A{\cdot }_{𝑜}{1}_{𝑜}=A{\cdot }_{𝑜}\mathrm{suc}\varnothing$$
3		peano1	$$⊢\varnothing \in \mathrm{\omega }$$
4		nnmsuc	$$⊢\left(A\in \mathrm{\omega }\wedge \varnothing \in \mathrm{\omega }\right)\to A{\cdot }_{𝑜}\mathrm{suc}\varnothing =\left(A{\cdot }_{𝑜}\varnothing \right){+}_{𝑜}A$$
5	3 4	mpan2	$$⊢A\in \mathrm{\omega }\to A{\cdot }_{𝑜}\mathrm{suc}\varnothing =\left(A{\cdot }_{𝑜}\varnothing \right){+}_{𝑜}A$$
6		nnm0	$$⊢A\in \mathrm{\omega }\to A{\cdot }_{𝑜}\varnothing =\varnothing$$
7	6	oveq1d	$$⊢A\in \mathrm{\omega }\to \left(A{\cdot }_{𝑜}\varnothing \right){+}_{𝑜}A=\varnothing {+}_{𝑜}A$$
8		nna0r	$$⊢A\in \mathrm{\omega }\to \varnothing {+}_{𝑜}A=A$$
9	5 7 8	3eqtrd	$$⊢A\in \mathrm{\omega }\to A{\cdot }_{𝑜}\mathrm{suc}\varnothing =A$$
10	2 9	eqtrid	$$⊢A\in \mathrm{\omega }\to A{\cdot }_{𝑜}{1}_{𝑜}=A$$