# Metamath Proof Explorer

## Theorem fprodeq0

Description: Any finite product containing a zero term is itself zero. (Contributed by Scott Fenton, 27-Dec-2017)

Ref Expression
Hypotheses fprodeq0.1 $⊢ Z = ℤ ≥ M$
fprodeq0.2 $⊢ φ → N ∈ Z$
fprodeq0.3 $⊢ φ ∧ k ∈ Z → A ∈ ℂ$
fprodeq0.4 $⊢ φ ∧ k = N → A = 0$
Assertion fprodeq0 $⊢ φ ∧ K ∈ ℤ ≥ N → ∏ k = M K A = 0$

### Proof

Step Hyp Ref Expression
1 fprodeq0.1 $⊢ Z = ℤ ≥ M$
2 fprodeq0.2 $⊢ φ → N ∈ Z$
3 fprodeq0.3 $⊢ φ ∧ k ∈ Z → A ∈ ℂ$
4 fprodeq0.4 $⊢ φ ∧ k = N → A = 0$
5 eluzel2 $⊢ K ∈ ℤ ≥ N → N ∈ ℤ$
6 5 adantl $⊢ φ ∧ K ∈ ℤ ≥ N → N ∈ ℤ$
7 6 zred $⊢ φ ∧ K ∈ ℤ ≥ N → N ∈ ℝ$
8 7 ltp1d $⊢ φ ∧ K ∈ ℤ ≥ N → N < N + 1$
9 fzdisj $⊢ N < N + 1 → M … N ∩ N + 1 … K = ∅$
10 8 9 syl $⊢ φ ∧ K ∈ ℤ ≥ N → M … N ∩ N + 1 … K = ∅$
11 eluzel2 $⊢ N ∈ ℤ ≥ M → M ∈ ℤ$
12 11 1 eleq2s $⊢ N ∈ Z → M ∈ ℤ$
13 2 12 syl $⊢ φ → M ∈ ℤ$
14 13 adantr $⊢ φ ∧ K ∈ ℤ ≥ N → M ∈ ℤ$
15 eluzelz $⊢ K ∈ ℤ ≥ N → K ∈ ℤ$
16 15 adantl $⊢ φ ∧ K ∈ ℤ ≥ N → K ∈ ℤ$
17 14 16 6 3jca $⊢ φ ∧ K ∈ ℤ ≥ N → M ∈ ℤ ∧ K ∈ ℤ ∧ N ∈ ℤ$
18 eluzle $⊢ N ∈ ℤ ≥ M → M ≤ N$
19 18 1 eleq2s $⊢ N ∈ Z → M ≤ N$
20 2 19 syl $⊢ φ → M ≤ N$
21 eluzle $⊢ K ∈ ℤ ≥ N → N ≤ K$
22 20 21 anim12i $⊢ φ ∧ K ∈ ℤ ≥ N → M ≤ N ∧ N ≤ K$
23 elfz2 $⊢ N ∈ M … K ↔ M ∈ ℤ ∧ K ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ N ∧ N ≤ K$
24 17 22 23 sylanbrc $⊢ φ ∧ K ∈ ℤ ≥ N → N ∈ M … K$
25 fzsplit $⊢ N ∈ M … K → M … K = M … N ∪ N + 1 … K$
26 24 25 syl $⊢ φ ∧ K ∈ ℤ ≥ N → M … K = M … N ∪ N + 1 … K$
27 fzfid $⊢ φ ∧ K ∈ ℤ ≥ N → M … K ∈ Fin$
28 elfzuz $⊢ k ∈ M … K → k ∈ ℤ ≥ M$
29 28 1 eleqtrrdi $⊢ k ∈ M … K → k ∈ Z$
30 29 3 sylan2 $⊢ φ ∧ k ∈ M … K → A ∈ ℂ$
31 30 adantlr $⊢ φ ∧ K ∈ ℤ ≥ N ∧ k ∈ M … K → A ∈ ℂ$
32 10 26 27 31 fprodsplit $⊢ φ ∧ K ∈ ℤ ≥ N → ∏ k = M K A = ∏ k = M N A ⁢ ∏ k = N + 1 K A$
33 2 1 eleqtrdi $⊢ φ → N ∈ ℤ ≥ M$
34 elfzuz $⊢ k ∈ M … N → k ∈ ℤ ≥ M$
35 34 1 eleqtrrdi $⊢ k ∈ M … N → k ∈ Z$
36 35 3 sylan2 $⊢ φ ∧ k ∈ M … N → A ∈ ℂ$
37 33 36 fprodm1s
38 2 4 csbied
39 38 oveq2d
40 fzfid $⊢ φ → M … N − 1 ∈ Fin$
41 elfzuz $⊢ k ∈ M … N − 1 → k ∈ ℤ ≥ M$
42 41 1 eleqtrrdi $⊢ k ∈ M … N − 1 → k ∈ Z$
43 42 3 sylan2 $⊢ φ ∧ k ∈ M … N − 1 → A ∈ ℂ$
44 40 43 fprodcl $⊢ φ → ∏ k = M N − 1 A ∈ ℂ$
45 44 mul01d $⊢ φ → ∏ k = M N − 1 A ⋅ 0 = 0$
46 37 39 45 3eqtrd $⊢ φ → ∏ k = M N A = 0$
47 46 adantr $⊢ φ ∧ K ∈ ℤ ≥ N → ∏ k = M N A = 0$
48 47 oveq1d $⊢ φ ∧ K ∈ ℤ ≥ N → ∏ k = M N A ⁢ ∏ k = N + 1 K A = 0 ⋅ ∏ k = N + 1 K A$
49 fzfid $⊢ φ ∧ K ∈ ℤ ≥ N → N + 1 … K ∈ Fin$
50 1 peano2uzs $⊢ N ∈ Z → N + 1 ∈ Z$
51 2 50 syl $⊢ φ → N + 1 ∈ Z$
52 elfzuz $⊢ k ∈ N + 1 … K → k ∈ ℤ ≥ N + 1$
53 1 uztrn2 $⊢ N + 1 ∈ Z ∧ k ∈ ℤ ≥ N + 1 → k ∈ Z$
54 51 52 53 syl2an $⊢ φ ∧ k ∈ N + 1 … K → k ∈ Z$
55 54 adantrl $⊢ φ ∧ K ∈ ℤ ≥ N ∧ k ∈ N + 1 … K → k ∈ Z$
56 55 3 syldan $⊢ φ ∧ K ∈ ℤ ≥ N ∧ k ∈ N + 1 … K → A ∈ ℂ$
57 56 anassrs $⊢ φ ∧ K ∈ ℤ ≥ N ∧ k ∈ N + 1 … K → A ∈ ℂ$
58 49 57 fprodcl $⊢ φ ∧ K ∈ ℤ ≥ N → ∏ k = N + 1 K A ∈ ℂ$
59 58 mul02d $⊢ φ ∧ K ∈ ℤ ≥ N → 0 ⋅ ∏ k = N + 1 K A = 0$
60 32 48 59 3eqtrd $⊢ φ ∧ K ∈ ℤ ≥ N → ∏ k = M K A = 0$