Theorem nnm1

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

	Ref	Expression
Assertion	nnm1	⊢ ( 𝐴 ∈ ω → ( 𝐴 ·o 1o ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-1o	⊢ 1o = suc ∅
2	1	oveq2i	⊢ ( 𝐴 ·o 1o ) = ( 𝐴 ·o suc ∅ )
3		peano1	⊢ ∅ ∈ ω
4		nnmsuc	⊢ ( ( 𝐴 ∈ ω ∧ ∅ ∈ ω ) → ( 𝐴 ·o suc ∅ ) = ( ( 𝐴 ·o ∅ ) +o 𝐴 ) )
5	3 4	mpan2	⊢ ( 𝐴 ∈ ω → ( 𝐴 ·o suc ∅ ) = ( ( 𝐴 ·o ∅ ) +o 𝐴 ) )
6		nnm0	⊢ ( 𝐴 ∈ ω → ( 𝐴 ·o ∅ ) = ∅ )
7	6	oveq1d	⊢ ( 𝐴 ∈ ω → ( ( 𝐴 ·o ∅ ) +o 𝐴 ) = ( ∅ +o 𝐴 ) )
8		nna0r	⊢ ( 𝐴 ∈ ω → ( ∅ +o 𝐴 ) = 𝐴 )
9	5 7 8	3eqtrd	⊢ ( 𝐴 ∈ ω → ( 𝐴 ·o suc ∅ ) = 𝐴 )
10	2 9	syl5eq	⊢ ( 𝐴 ∈ ω → ( 𝐴 ·o 1o ) = 𝐴 )