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	⊢ ( 𝐴 ∈ ω → ( 𝐴 ·o 2o ) = ( 𝐴 +o 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df-2o	⊢ 2o = suc 1o
2	1	oveq2i	⊢ ( 𝐴 ·o 2o ) = ( 𝐴 ·o suc 1o )
3		1onn	⊢ 1o ∈ ω
4		nnmsuc	⊢ ( ( 𝐴 ∈ ω ∧ 1o ∈ ω ) → ( 𝐴 ·o suc 1o ) = ( ( 𝐴 ·o 1o ) +o 𝐴 ) )
5	3 4	mpan2	⊢ ( 𝐴 ∈ ω → ( 𝐴 ·o suc 1o ) = ( ( 𝐴 ·o 1o ) +o 𝐴 ) )
6		nnm1	⊢ ( 𝐴 ∈ ω → ( 𝐴 ·o 1o ) = 𝐴 )
7	6	oveq1d	⊢ ( 𝐴 ∈ ω → ( ( 𝐴 ·o 1o ) +o 𝐴 ) = ( 𝐴 +o 𝐴 ) )
8	5 7	eqtrd	⊢ ( 𝐴 ∈ ω → ( 𝐴 ·o suc 1o ) = ( 𝐴 +o 𝐴 ) )
9	2 8	eqtrid	⊢ ( 𝐴 ∈ ω → ( 𝐴 ·o 2o ) = ( 𝐴 +o 𝐴 ) )