Metamath Proof Explorer

Theorem nn2m

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

Ref Expression
Assertion nn2m ⊢ A ∈ ω → 2 𝑜 ⋅ 𝑜 A = A + 𝑜 A

Proof

Step Hyp Ref Expression
1 2onn ⊢ 2 𝑜 ∈ ω
2 nnmcom ⊢ 2 𝑜 ∈ ω ∧ A ∈ ω → 2 𝑜 ⋅ 𝑜 A = A ⋅ 𝑜 2 𝑜
3 1 2 mpan ⊢ A ∈ ω → 2 𝑜 ⋅ 𝑜 A = A ⋅ 𝑜 2 𝑜
4 nnm2 ⊢ A ∈ ω → A ⋅ 𝑜 2 𝑜 = A + 𝑜 A
5 3 4 eqtrd ⊢ A ∈ ω → 2 𝑜 ⋅ 𝑜 A = A + 𝑜 A