Metamath Proof Explorer

Theorem nnm1

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

Ref Expression
Assertion nnm1 ⊢ A ∈ ω → A ⋅ 𝑜 1 𝑜 = A

Proof

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