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

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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
fprodeq0.2 ⊢ ( 𝜑 → 𝑁 ∈ 𝑍 )
fprodeq0.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
fprodeq0.4 ⊢ ( ( 𝜑 ∧ 𝑘 = 𝑁 ) → 𝐴 = 0 )
Assertion fprodeq0 ( ( 𝜑 ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ∏ 𝑘 ∈ ( 𝑀 ... 𝐾 ) 𝐴 = 0 )

Proof

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