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	imbitrrid	⊢ ( 𝑦 ∈ ω → ( ( ∅ ·o 𝑦 ) = ∅ → ( ∅ ·o suc 𝑦 ) = ∅ ) )
21	2 4 6 8 11 20	finds	⊢ ( 𝐴 ∈ ω → ( ∅ ·o 𝐴 ) = ∅ )