This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fprodeq0g

Description: Any finite product containing a zero term is itself zero. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses fprodeq0g.kph ⊢ Ⅎ k φ
fprodeq0g.a ⊢ φ → A ∈ Fin
fprodeq0g.b ⊢ φ ∧ k ∈ A → B ∈ ℂ
fprodeq0g.c ⊢ φ → C ∈ A
fprodeq0g.b0 ⊢ φ ∧ k = C → B = 0
Assertion fprodeq0g ⊢ φ → ∏ k ∈ A B = 0

Proof

Step Hyp Ref Expression
1 fprodeq0g.kph ⊢ Ⅎ k φ
2 fprodeq0g.a ⊢ φ → A ∈ Fin
3 fprodeq0g.b ⊢ φ ∧ k ∈ A → B ∈ ℂ
4 fprodeq0g.c ⊢ φ → C ∈ A
5 fprodeq0g.b0 ⊢ φ ∧ k = C → B = 0
6 nfcvd ⊢ φ → Ⅎ _ k 0
7 1 6 2 3 4 5 fprodsplit1f ⊢ φ → ∏ k ∈ A B = 0 ⋅ ∏ k ∈ A ∖ C B
8 diffi ⊢ A ∈ Fin → A ∖ C ∈ Fin
9 2 8 syl ⊢ φ → A ∖ C ∈ Fin
10 eldifi ⊢ k ∈ A ∖ C → k ∈ A
11 10 3 sylan2 ⊢ φ ∧ k ∈ A ∖ C → B ∈ ℂ
12 1 9 11 fprodclf ⊢ φ → ∏ k ∈ A ∖ C B ∈ ℂ
13 12 mul02d ⊢ φ → 0 ⋅ ∏ k ∈ A ∖ C B = 0
14 7 13 eqtrd ⊢ φ → ∏ k ∈ A B = 0