Theorem nnm2

Description: Multiply an element of _om by 2o . (Contributed by Scott Fenton, 18-Apr-2012) (Revised by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Assertion	nnm2	$$⊢A\in \mathrm{\omega }\to A{\cdot }_{𝑜}{2}_{𝑜}=A{+}_{𝑜}A$$

Proof

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