Metamath Proof Explorer

Theorem nnm0r

Description: Multiplication with zero. Exercise 16 of Enderton p. 82. (Contributed by NM, 20-Sep-1995) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnm0r ⊢ A ∈ ω → ∅ ⋅ 𝑜 A = ∅

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ x = ∅ → ∅ ⋅ 𝑜 x = ∅ ⋅ 𝑜 ∅
2 1 eqeq1d ⊢ x = ∅ → ∅ ⋅ 𝑜 x = ∅ ↔ ∅ ⋅ 𝑜 ∅ = ∅
3 oveq2 ⊢ x = y → ∅ ⋅ 𝑜 x = ∅ ⋅ 𝑜 y
4 3 eqeq1d ⊢ x = y → ∅ ⋅ 𝑜 x = ∅ ↔ ∅ ⋅ 𝑜 y = ∅
5 oveq2 ⊢ x = suc ⁡ y → ∅ ⋅ 𝑜 x = ∅ ⋅ 𝑜 suc ⁡ y
6 5 eqeq1d ⊢ x = suc ⁡ y → ∅ ⋅ 𝑜 x = ∅ ↔ ∅ ⋅ 𝑜 suc ⁡ y = ∅
7 oveq2 ⊢ x = A → ∅ ⋅ 𝑜 x = ∅ ⋅ 𝑜 A
8 7 eqeq1d ⊢ x = A → ∅ ⋅ 𝑜 x = ∅ ↔ ∅ ⋅ 𝑜 A = ∅
9 0elon ⊢ ∅ ∈ On
10 om0 ⊢ ∅ ∈ On → ∅ ⋅ 𝑜 ∅ = ∅
11 9 10 ax-mp ⊢ ∅ ⋅ 𝑜 ∅ = ∅
12 oveq1 ⊢ ∅ ⋅ 𝑜 y = ∅ → ∅ ⋅ 𝑜 y + 𝑜 ∅ = ∅ + 𝑜 ∅
13 oa0 ⊢ ∅ ∈ On → ∅ + 𝑜 ∅ = ∅
14 9 13 ax-mp ⊢ ∅ + 𝑜 ∅ = ∅
15 12 14 eqtrdi ⊢ ∅ ⋅ 𝑜 y = ∅ → ∅ ⋅ 𝑜 y + 𝑜 ∅ = ∅
16 peano1 ⊢ ∅ ∈ ω
17 nnmsuc ⊢ ∅ ∈ ω ∧ y ∈ ω → ∅ ⋅ 𝑜 suc ⁡ y = ∅ ⋅ 𝑜 y + 𝑜 ∅
18 16 17 mpan ⊢ y ∈ ω → ∅ ⋅ 𝑜 suc ⁡ y = ∅ ⋅ 𝑜 y + 𝑜 ∅
19 18 eqeq1d ⊢ y ∈ ω → ∅ ⋅ 𝑜 suc ⁡ y = ∅ ↔ ∅ ⋅ 𝑜 y + 𝑜 ∅ = ∅
20 15 19 imbitrrid ⊢ y ∈ ω → ∅ ⋅ 𝑜 y = ∅ → ∅ ⋅ 𝑜 suc ⁡ y = ∅
21 2 4 6 8 11 20 finds ⊢ A ∈ ω → ∅ ⋅ 𝑜 A = ∅