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