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 ( 𝐴 ∈ ω → ( ∅ ·o 𝐴 ) = ∅ )

Proof

Step Hyp Ref Expression
1 oveq2 ( 𝑥 = ∅ → ( ∅ ·o 𝑥 ) = ( ∅ ·o ∅ ) )
2 1 eqeq1d ( 𝑥 = ∅ → ( ( ∅ ·o 𝑥 ) = ∅ ↔ ( ∅ ·o ∅ ) = ∅ ) )
3 oveq2 ( 𝑥 = 𝑦 → ( ∅ ·o 𝑥 ) = ( ∅ ·o 𝑦 ) )
4 3 eqeq1d ( 𝑥 = 𝑦 → ( ( ∅ ·o 𝑥 ) = ∅ ↔ ( ∅ ·o 𝑦 ) = ∅ ) )
5 oveq2 ( 𝑥 = suc 𝑦 → ( ∅ ·o 𝑥 ) = ( ∅ ·o suc 𝑦 ) )
6 5 eqeq1d ( 𝑥 = suc 𝑦 → ( ( ∅ ·o 𝑥 ) = ∅ ↔ ( ∅ ·o suc 𝑦 ) = ∅ ) )
7 oveq2 ( 𝑥 = 𝐴 → ( ∅ ·o 𝑥 ) = ( ∅ ·o 𝐴 ) )
8 7 eqeq1d ( 𝑥 = 𝐴 → ( ( ∅ ·o 𝑥 ) = ∅ ↔ ( ∅ ·o 𝐴 ) = ∅ ) )
9 0elon ∅ ∈ On
10 om0 ( ∅ ∈ On → ( ∅ ·o ∅ ) = ∅ )
11 9 10 ax-mp ( ∅ ·o ∅ ) = ∅
12 oveq1 ( ( ∅ ·o 𝑦 ) = ∅ → ( ( ∅ ·o 𝑦 ) +o ∅ ) = ( ∅ +o ∅ ) )
13 oa0 ( ∅ ∈ On → ( ∅ +o ∅ ) = ∅ )
14 9 13 ax-mp ( ∅ +o ∅ ) = ∅
15 12 14 eqtrdi ( ( ∅ ·o 𝑦 ) = ∅ → ( ( ∅ ·o 𝑦 ) +o ∅ ) = ∅ )
16 peano1 ∅ ∈ ω
17 nnmsuc ( ( ∅ ∈ ω ∧ 𝑦 ∈ ω ) → ( ∅ ·o suc 𝑦 ) = ( ( ∅ ·o 𝑦 ) +o ∅ ) )
18 16 17 mpan ( 𝑦 ∈ ω → ( ∅ ·o suc 𝑦 ) = ( ( ∅ ·o 𝑦 ) +o ∅ ) )
19 18 eqeq1d ( 𝑦 ∈ ω → ( ( ∅ ·o suc 𝑦 ) = ∅ ↔ ( ( ∅ ·o 𝑦 ) +o ∅ ) = ∅ ) )
20 15 19 syl5ibr ( 𝑦 ∈ ω → ( ( ∅ ·o 𝑦 ) = ∅ → ( ∅ ·o suc 𝑦 ) = ∅ ) )
21 2 4 6 8 11 20 finds ( 𝐴 ∈ ω → ( ∅ ·o 𝐴 ) = ∅ )