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=∅