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 ω \to A \cdot_{𝑜} 2_{𝑜} = A +_{𝑜} A$

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

Metamath Proof Explorer