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 syl5ibr y ω 𝑜 y = 𝑜 suc y =
21 2 4 6 8 11 20 finds A ω 𝑜 A =