Metamath Proof Explorer

Theorem prodfn0

Description: No term of a nonzero infinite product is zero. (Contributed by Scott Fenton, 14-Jan-2018)

Ref Expression
Hypotheses prodfn0.1 
|- ( ph -> N e. ( ZZ>= ` M ) )
prodfn0.2 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )
prodfn0.3 
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) =/= 0 )
Assertion prodfn0 
|- ( ph -> ( seq M ( x. , F ) ` N ) =/= 0 )

Proof

Step Hyp Ref Expression
1 prodfn0.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 prodfn0.2 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )
3 prodfn0.3 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) =/= 0 )
4 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
5 1 4 syl 
 |-  ( ph -> N e. ( M ... N ) )
6 fveq2 
 |-  ( m = M -> ( seq M ( x. , F ) ` m ) = ( seq M ( x. , F ) ` M ) )
7 6 neeq1d 
 |-  ( m = M -> ( ( seq M ( x. , F ) ` m ) =/= 0 <-> ( seq M ( x. , F ) ` M ) =/= 0 ) )
8 7 imbi2d 
 |-  ( m = M -> ( ( ph -> ( seq M ( x. , F ) ` m ) =/= 0 ) <-> ( ph -> ( seq M ( x. , F ) ` M ) =/= 0 ) ) )
9 fveq2 
 |-  ( m = n -> ( seq M ( x. , F ) ` m ) = ( seq M ( x. , F ) ` n ) )
10 9 neeq1d 
 |-  ( m = n -> ( ( seq M ( x. , F ) ` m ) =/= 0 <-> ( seq M ( x. , F ) ` n ) =/= 0 ) )
11 10 imbi2d 
 |-  ( m = n -> ( ( ph -> ( seq M ( x. , F ) ` m ) =/= 0 ) <-> ( ph -> ( seq M ( x. , F ) ` n ) =/= 0 ) ) )
12 fveq2 
 |-  ( m = ( n + 1 ) -> ( seq M ( x. , F ) ` m ) = ( seq M ( x. , F ) ` ( n + 1 ) ) )
13 12 neeq1d 
 |-  ( m = ( n + 1 ) -> ( ( seq M ( x. , F ) ` m ) =/= 0 <-> ( seq M ( x. , F ) ` ( n + 1 ) ) =/= 0 ) )
14 13 imbi2d 
 |-  ( m = ( n + 1 ) -> ( ( ph -> ( seq M ( x. , F ) ` m ) =/= 0 ) <-> ( ph -> ( seq M ( x. , F ) ` ( n + 1 ) ) =/= 0 ) ) )
15 fveq2 
 |-  ( m = N -> ( seq M ( x. , F ) ` m ) = ( seq M ( x. , F ) ` N ) )
16 15 neeq1d 
 |-  ( m = N -> ( ( seq M ( x. , F ) ` m ) =/= 0 <-> ( seq M ( x. , F ) ` N ) =/= 0 ) )
17 16 imbi2d 
 |-  ( m = N -> ( ( ph -> ( seq M ( x. , F ) ` m ) =/= 0 ) <-> ( ph -> ( seq M ( x. , F ) ` N ) =/= 0 ) ) )
18 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
19 elfzelz 
 |-  ( M e. ( M ... N ) -> M e. ZZ )
20 19 adantl 
 |-  ( ( ph /\ M e. ( M ... N ) ) -> M e. ZZ )
21 seq1 
 |-  ( M e. ZZ -> ( seq M ( x. , F ) ` M ) = ( F ` M ) )
22 20 21 syl 
 |-  ( ( ph /\ M e. ( M ... N ) ) -> ( seq M ( x. , F ) ` M ) = ( F ` M ) )
23 fveq2 
 |-  ( k = M -> ( F ` k ) = ( F ` M ) )
24 23 neeq1d 
 |-  ( k = M -> ( ( F ` k ) =/= 0 <-> ( F ` M ) =/= 0 ) )
25 24 imbi2d 
 |-  ( k = M -> ( ( ph -> ( F ` k ) =/= 0 ) <-> ( ph -> ( F ` M ) =/= 0 ) ) )
26 3 expcom 
 |-  ( k e. ( M ... N ) -> ( ph -> ( F ` k ) =/= 0 ) )
27 25 26 vtoclga 
 |-  ( M e. ( M ... N ) -> ( ph -> ( F ` M ) =/= 0 ) )
28 27 impcom 
 |-  ( ( ph /\ M e. ( M ... N ) ) -> ( F ` M ) =/= 0 )
29 22 28 eqnetrd 
 |-  ( ( ph /\ M e. ( M ... N ) ) -> ( seq M ( x. , F ) ` M ) =/= 0 )
30 29 expcom 
 |-  ( M e. ( M ... N ) -> ( ph -> ( seq M ( x. , F ) ` M ) =/= 0 ) )
31 18 30 syl 
 |-  ( N e. ( ZZ>= ` M ) -> ( ph -> ( seq M ( x. , F ) ` M ) =/= 0 ) )
32 elfzouz 
 |-  ( n e. ( M ..^ N ) -> n e. ( ZZ>= ` M ) )
33 32 3ad2ant2 
 |-  ( ( ph /\ n e. ( M ..^ N ) /\ ( seq M ( x. , F ) ` n ) =/= 0 ) -> n e. ( ZZ>= ` M ) )
34 seqp1 
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( x. , F ) ` ( n + 1 ) ) = ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) )
35 33 34 syl 
 |-  ( ( ph /\ n e. ( M ..^ N ) /\ ( seq M ( x. , F ) ` n ) =/= 0 ) -> ( seq M ( x. , F ) ` ( n + 1 ) ) = ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) )
36 elfzofz 
 |-  ( n e. ( M ..^ N ) -> n e. ( M ... N ) )
37 elfzuz 
 |-  ( n e. ( M ... N ) -> n e. ( ZZ>= ` M ) )
38 37 adantl 
 |-  ( ( ph /\ n e. ( M ... N ) ) -> n e. ( ZZ>= ` M ) )
39 elfzuz3 
 |-  ( n e. ( M ... N ) -> N e. ( ZZ>= ` n ) )
40 fzss2 
 |-  ( N e. ( ZZ>= ` n ) -> ( M ... n ) C_ ( M ... N ) )
41 39 40 syl 
 |-  ( n e. ( M ... N ) -> ( M ... n ) C_ ( M ... N ) )
42 41 sselda 
 |-  ( ( n e. ( M ... N ) /\ k e. ( M ... n ) ) -> k e. ( M ... N ) )
43 42 2 sylan2 
 |-  ( ( ph /\ ( n e. ( M ... N ) /\ k e. ( M ... n ) ) ) -> ( F ` k ) e. CC )
44 43 anassrs 
 |-  ( ( ( ph /\ n e. ( M ... N ) ) /\ k e. ( M ... n ) ) -> ( F ` k ) e. CC )
45 mulcl 
 |-  ( ( k e. CC /\ x e. CC ) -> ( k x. x ) e. CC )
46 45 adantl 
 |-  ( ( ( ph /\ n e. ( M ... N ) ) /\ ( k e. CC /\ x e. CC ) ) -> ( k x. x ) e. CC )
47 38 44 46 seqcl 
 |-  ( ( ph /\ n e. ( M ... N ) ) -> ( seq M ( x. , F ) ` n ) e. CC )
48 36 47 sylan2 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( seq M ( x. , F ) ` n ) e. CC )
49 48 3adant3 
 |-  ( ( ph /\ n e. ( M ..^ N ) /\ ( seq M ( x. , F ) ` n ) =/= 0 ) -> ( seq M ( x. , F ) ` n ) e. CC )
50 fzofzp1 
 |-  ( n e. ( M ..^ N ) -> ( n + 1 ) e. ( M ... N ) )
51 fveq2 
 |-  ( k = ( n + 1 ) -> ( F ` k ) = ( F ` ( n + 1 ) ) )
52 51 eleq1d 
 |-  ( k = ( n + 1 ) -> ( ( F ` k ) e. CC <-> ( F ` ( n + 1 ) ) e. CC ) )
53 52 imbi2d 
 |-  ( k = ( n + 1 ) -> ( ( ph -> ( F ` k ) e. CC ) <-> ( ph -> ( F ` ( n + 1 ) ) e. CC ) ) )
54 2 expcom 
 |-  ( k e. ( M ... N ) -> ( ph -> ( F ` k ) e. CC ) )
55 53 54 vtoclga 
 |-  ( ( n + 1 ) e. ( M ... N ) -> ( ph -> ( F ` ( n + 1 ) ) e. CC ) )
56 50 55 syl 
 |-  ( n e. ( M ..^ N ) -> ( ph -> ( F ` ( n + 1 ) ) e. CC ) )
57 56 impcom 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( F ` ( n + 1 ) ) e. CC )
58 57 3adant3 
 |-  ( ( ph /\ n e. ( M ..^ N ) /\ ( seq M ( x. , F ) ` n ) =/= 0 ) -> ( F ` ( n + 1 ) ) e. CC )
59 simp3 
 |-  ( ( ph /\ n e. ( M ..^ N ) /\ ( seq M ( x. , F ) ` n ) =/= 0 ) -> ( seq M ( x. , F ) ` n ) =/= 0 )
60 51 neeq1d 
 |-  ( k = ( n + 1 ) -> ( ( F ` k ) =/= 0 <-> ( F ` ( n + 1 ) ) =/= 0 ) )
61 60 imbi2d 
 |-  ( k = ( n + 1 ) -> ( ( ph -> ( F ` k ) =/= 0 ) <-> ( ph -> ( F ` ( n + 1 ) ) =/= 0 ) ) )
62 61 26 vtoclga 
 |-  ( ( n + 1 ) e. ( M ... N ) -> ( ph -> ( F ` ( n + 1 ) ) =/= 0 ) )
63 62 impcom 
 |-  ( ( ph /\ ( n + 1 ) e. ( M ... N ) ) -> ( F ` ( n + 1 ) ) =/= 0 )
64 50 63 sylan2 
 |-  ( ( ph /\ n e. ( M ..^ N ) ) -> ( F ` ( n + 1 ) ) =/= 0 )
65 64 3adant3 
 |-  ( ( ph /\ n e. ( M ..^ N ) /\ ( seq M ( x. , F ) ` n ) =/= 0 ) -> ( F ` ( n + 1 ) ) =/= 0 )
66 49 58 59 65 mulne0d 
 |-  ( ( ph /\ n e. ( M ..^ N ) /\ ( seq M ( x. , F ) ` n ) =/= 0 ) -> ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) =/= 0 )
67 35 66 eqnetrd 
 |-  ( ( ph /\ n e. ( M ..^ N ) /\ ( seq M ( x. , F ) ` n ) =/= 0 ) -> ( seq M ( x. , F ) ` ( n + 1 ) ) =/= 0 )
68 67 3exp 
 |-  ( ph -> ( n e. ( M ..^ N ) -> ( ( seq M ( x. , F ) ` n ) =/= 0 -> ( seq M ( x. , F ) ` ( n + 1 ) ) =/= 0 ) ) )
69 68 com12 
 |-  ( n e. ( M ..^ N ) -> ( ph -> ( ( seq M ( x. , F ) ` n ) =/= 0 -> ( seq M ( x. , F ) ` ( n + 1 ) ) =/= 0 ) ) )
70 69 a2d 
 |-  ( n e. ( M ..^ N ) -> ( ( ph -> ( seq M ( x. , F ) ` n ) =/= 0 ) -> ( ph -> ( seq M ( x. , F ) ` ( n + 1 ) ) =/= 0 ) ) )
71 8 11 14 17 31 70 fzind2 
 |-  ( N e. ( M ... N ) -> ( ph -> ( seq M ( x. , F ) ` N ) =/= 0 ) )
72 5 71 mpcom 
 |-  ( ph -> ( seq M ( x. , F ) ` N ) =/= 0 )