Metamath Proof Explorer

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 ⊢ A ∈ ω → A ⋅ 𝑜 2 𝑜 = A + 𝑜 A

Proof

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