nnm1

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

		Ref	Expression
	Assertion	nnm1	$⊢ A \in ω \to A \cdot_{𝑜} 1_{𝑜} = A$

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

Metamath Proof Explorer