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 
|- Z = ( ZZ>= ` M )
fprodeq0.2 
|- ( ph -> N e. Z )
fprodeq0.3 
|- ( ( ph /\ k e. Z ) -> A e. CC )
fprodeq0.4 
|- ( ( ph /\ k = N ) -> A = 0 )
Assertion fprodeq0 
|- ( ( ph /\ K e. ( ZZ>= ` N ) ) -> prod_ k e. ( M ... K ) A = 0 )

Proof

Step Hyp Ref Expression
1 fprodeq0.1 
 |-  Z = ( ZZ>= ` M )
2 fprodeq0.2 
 |-  ( ph -> N e. Z )
3 fprodeq0.3 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
4 fprodeq0.4 
 |-  ( ( ph /\ k = N ) -> A = 0 )
5 eluzel2 
 |-  ( K e. ( ZZ>= ` N ) -> N e. ZZ )
6 5 adantl 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> N e. ZZ )
7 6 zred 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> N e. RR )
8 7 ltp1d 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> N < ( N + 1 ) )
9 fzdisj 
 |-  ( N < ( N + 1 ) -> ( ( M ... N ) i^i ( ( N + 1 ) ... K ) ) = (/) )
10 8 9 syl 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> ( ( M ... N ) i^i ( ( N + 1 ) ... K ) ) = (/) )
11 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
12 11 1 eleq2s 
 |-  ( N e. Z -> M e. ZZ )
13 2 12 syl 
 |-  ( ph -> M e. ZZ )
14 13 adantr 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> M e. ZZ )
15 eluzelz 
 |-  ( K e. ( ZZ>= ` N ) -> K e. ZZ )
16 15 adantl 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> K e. ZZ )
17 14 16 6 3jca 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> ( M e. ZZ /\ K e. ZZ /\ N e. ZZ ) )
18 eluzle 
 |-  ( N e. ( ZZ>= ` M ) -> M <_ N )
19 18 1 eleq2s 
 |-  ( N e. Z -> M <_ N )
20 2 19 syl 
 |-  ( ph -> M <_ N )
21 eluzle 
 |-  ( K e. ( ZZ>= ` N ) -> N <_ K )
22 20 21 anim12i 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> ( M <_ N /\ N <_ K ) )
23 elfz2 
 |-  ( N e. ( M ... K ) <-> ( ( M e. ZZ /\ K e. ZZ /\ N e. ZZ ) /\ ( M <_ N /\ N <_ K ) ) )
24 17 22 23 sylanbrc 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> N e. ( M ... K ) )
25 fzsplit 
 |-  ( N e. ( M ... K ) -> ( M ... K ) = ( ( M ... N ) u. ( ( N + 1 ) ... K ) ) )
26 24 25 syl 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> ( M ... K ) = ( ( M ... N ) u. ( ( N + 1 ) ... K ) ) )
27 fzfid 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> ( M ... K ) e. Fin )
28 elfzuz 
 |-  ( k e. ( M ... K ) -> k e. ( ZZ>= ` M ) )
29 28 1 eleqtrrdi 
 |-  ( k e. ( M ... K ) -> k e. Z )
30 29 3 sylan2 
 |-  ( ( ph /\ k e. ( M ... K ) ) -> A e. CC )
31 30 adantlr 
 |-  ( ( ( ph /\ K e. ( ZZ>= ` N ) ) /\ k e. ( M ... K ) ) -> A e. CC )
32 10 26 27 31 fprodsplit 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> prod_ k e. ( M ... K ) A = ( prod_ k e. ( M ... N ) A x. prod_ k e. ( ( N + 1 ) ... K ) A ) )
33 2 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
34 elfzuz 
 |-  ( k e. ( M ... N ) -> k e. ( ZZ>= ` M ) )
35 34 1 eleqtrrdi 
 |-  ( k e. ( M ... N ) -> k e. Z )
36 35 3 sylan2 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )
37 33 36 fprodm1s 
 |-  ( ph -> prod_ k e. ( M ... N ) A = ( prod_ k e. ( M ... ( N - 1 ) ) A x. [_ N / k ]_ A ) )
38 2 4 csbied 
 |-  ( ph -> [_ N / k ]_ A = 0 )
39 38 oveq2d 
 |-  ( ph -> ( prod_ k e. ( M ... ( N - 1 ) ) A x. [_ N / k ]_ A ) = ( prod_ k e. ( M ... ( N - 1 ) ) A x. 0 ) )
40 fzfid 
 |-  ( ph -> ( M ... ( N - 1 ) ) e. Fin )
41 elfzuz 
 |-  ( k e. ( M ... ( N - 1 ) ) -> k e. ( ZZ>= ` M ) )
42 41 1 eleqtrrdi 
 |-  ( k e. ( M ... ( N - 1 ) ) -> k e. Z )
43 42 3 sylan2 
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> A e. CC )
44 40 43 fprodcl 
 |-  ( ph -> prod_ k e. ( M ... ( N - 1 ) ) A e. CC )
45 44 mul01d 
 |-  ( ph -> ( prod_ k e. ( M ... ( N - 1 ) ) A x. 0 ) = 0 )
46 37 39 45 3eqtrd 
 |-  ( ph -> prod_ k e. ( M ... N ) A = 0 )
47 46 adantr 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> prod_ k e. ( M ... N ) A = 0 )
48 47 oveq1d 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> ( prod_ k e. ( M ... N ) A x. prod_ k e. ( ( N + 1 ) ... K ) A ) = ( 0 x. prod_ k e. ( ( N + 1 ) ... K ) A ) )
49 fzfid 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> ( ( N + 1 ) ... K ) e. Fin )
50 1 peano2uzs 
 |-  ( N e. Z -> ( N + 1 ) e. Z )
51 2 50 syl 
 |-  ( ph -> ( N + 1 ) e. Z )
52 elfzuz 
 |-  ( k e. ( ( N + 1 ) ... K ) -> k e. ( ZZ>= ` ( N + 1 ) ) )
53 1 uztrn2 
 |-  ( ( ( N + 1 ) e. Z /\ k e. ( ZZ>= ` ( N + 1 ) ) ) -> k e. Z )
54 51 52 53 syl2an 
 |-  ( ( ph /\ k e. ( ( N + 1 ) ... K ) ) -> k e. Z )
55 54 adantrl 
 |-  ( ( ph /\ ( K e. ( ZZ>= ` N ) /\ k e. ( ( N + 1 ) ... K ) ) ) -> k e. Z )
56 55 3 syldan 
 |-  ( ( ph /\ ( K e. ( ZZ>= ` N ) /\ k e. ( ( N + 1 ) ... K ) ) ) -> A e. CC )
57 56 anassrs 
 |-  ( ( ( ph /\ K e. ( ZZ>= ` N ) ) /\ k e. ( ( N + 1 ) ... K ) ) -> A e. CC )
58 49 57 fprodcl 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> prod_ k e. ( ( N + 1 ) ... K ) A e. CC )
59 58 mul02d 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> ( 0 x. prod_ k e. ( ( N + 1 ) ... K ) A ) = 0 )
60 32 48 59 3eqtrd 
 |-  ( ( ph /\ K e. ( ZZ>= ` N ) ) -> prod_ k e. ( M ... K ) A = 0 )