Metamath Proof Explorer

Theorem ntrivcvgfvn0

Description: Any value of a product sequence that converges to a nonzero value is itself nonzero. (Contributed by Scott Fenton, 20-Dec-2017)

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

Proof

Step Hyp Ref Expression
1 ntrivcvgfvn0.1 
 |-  Z = ( ZZ>= ` M )
2 ntrivcvgfvn0.2 
 |-  ( ph -> N e. Z )
3 ntrivcvgfvn0.3 
 |-  ( ph -> seq M ( x. , F ) ~~> X )
4 ntrivcvgfvn0.4 
 |-  ( ph -> X =/= 0 )
5 ntrivcvgfvn0.5 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
6 fclim 
 |-  ~~> : dom ~~> --> CC
7 ffun 
 |-  ( ~~> : dom ~~> --> CC -> Fun ~~> )
8 6 7 ax-mp 
 |-  Fun ~~>
9 funbrfv 
 |-  ( Fun ~~> -> ( seq M ( x. , F ) ~~> X -> ( ~~> ` seq M ( x. , F ) ) = X ) )
10 8 3 9 mpsyl 
 |-  ( ph -> ( ~~> ` seq M ( x. , F ) ) = X )
11 10 adantr 
 |-  ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> ( ~~> ` seq M ( x. , F ) ) = X )
12 eqid 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
13 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
14 1 13 eqsstri 
 |-  Z C_ ZZ
15 14 2 sselid 
 |-  ( ph -> N e. ZZ )
16 15 adantr 
 |-  ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> N e. ZZ )
17 seqex 
 |-  seq M ( x. , F ) e. _V
18 17 a1i 
 |-  ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> seq M ( x. , F ) e. _V )
19 0cnd 
 |-  ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> 0 e. CC )
20 fveqeq2 
 |-  ( m = N -> ( ( seq M ( x. , F ) ` m ) = 0 <-> ( seq M ( x. , F ) ` N ) = 0 ) )
21 20 imbi2d 
 |-  ( m = N -> ( ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> ( seq M ( x. , F ) ` m ) = 0 ) <-> ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> ( seq M ( x. , F ) ` N ) = 0 ) ) )
22 fveqeq2 
 |-  ( m = n -> ( ( seq M ( x. , F ) ` m ) = 0 <-> ( seq M ( x. , F ) ` n ) = 0 ) )
23 22 imbi2d 
 |-  ( m = n -> ( ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> ( seq M ( x. , F ) ` m ) = 0 ) <-> ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> ( seq M ( x. , F ) ` n ) = 0 ) ) )
24 fveqeq2 
 |-  ( m = ( n + 1 ) -> ( ( seq M ( x. , F ) ` m ) = 0 <-> ( seq M ( x. , F ) ` ( n + 1 ) ) = 0 ) )
25 24 imbi2d 
 |-  ( m = ( n + 1 ) -> ( ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> ( seq M ( x. , F ) ` m ) = 0 ) <-> ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> ( seq M ( x. , F ) ` ( n + 1 ) ) = 0 ) ) )
26 fveqeq2 
 |-  ( m = k -> ( ( seq M ( x. , F ) ` m ) = 0 <-> ( seq M ( x. , F ) ` k ) = 0 ) )
27 26 imbi2d 
 |-  ( m = k -> ( ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> ( seq M ( x. , F ) ` m ) = 0 ) <-> ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> ( seq M ( x. , F ) ` k ) = 0 ) ) )
28 simpr 
 |-  ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> ( seq M ( x. , F ) ` N ) = 0 )
29 2 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
30 uztrn 
 |-  ( ( n e. ( ZZ>= ` N ) /\ N e. ( ZZ>= ` M ) ) -> n e. ( ZZ>= ` M ) )
31 29 30 sylan2 
 |-  ( ( n e. ( ZZ>= ` N ) /\ ph ) -> n e. ( ZZ>= ` M ) )
32 31 3adant3 
 |-  ( ( n e. ( ZZ>= ` N ) /\ ph /\ ( seq M ( x. , F ) ` n ) = 0 ) -> n e. ( ZZ>= ` M ) )
33 seqp1 
 |-  ( n e. ( ZZ>= ` M ) -> ( seq M ( x. , F ) ` ( n + 1 ) ) = ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) )
34 32 33 syl 
 |-  ( ( n e. ( ZZ>= ` N ) /\ ph /\ ( seq M ( x. , F ) ` n ) = 0 ) -> ( seq M ( x. , F ) ` ( n + 1 ) ) = ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) )
35 oveq1 
 |-  ( ( seq M ( x. , F ) ` n ) = 0 -> ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) = ( 0 x. ( F ` ( n + 1 ) ) ) )
36 35 3ad2ant3 
 |-  ( ( n e. ( ZZ>= ` N ) /\ ph /\ ( seq M ( x. , F ) ` n ) = 0 ) -> ( ( seq M ( x. , F ) ` n ) x. ( F ` ( n + 1 ) ) ) = ( 0 x. ( F ` ( n + 1 ) ) ) )
37 peano2uz 
 |-  ( n e. ( ZZ>= ` N ) -> ( n + 1 ) e. ( ZZ>= ` N ) )
38 1 uztrn2 
 |-  ( ( N e. Z /\ ( n + 1 ) e. ( ZZ>= ` N ) ) -> ( n + 1 ) e. Z )
39 2 37 38 syl2an 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( n + 1 ) e. Z )
40 5 ralrimiva 
 |-  ( ph -> A. k e. Z ( F ` k ) e. CC )
41 fveq2 
 |-  ( k = ( n + 1 ) -> ( F ` k ) = ( F ` ( n + 1 ) ) )
42 41 eleq1d 
 |-  ( k = ( n + 1 ) -> ( ( F ` k ) e. CC <-> ( F ` ( n + 1 ) ) e. CC ) )
43 42 rspcv 
 |-  ( ( n + 1 ) e. Z -> ( A. k e. Z ( F ` k ) e. CC -> ( F ` ( n + 1 ) ) e. CC ) )
44 40 43 mpan9 
 |-  ( ( ph /\ ( n + 1 ) e. Z ) -> ( F ` ( n + 1 ) ) e. CC )
45 39 44 syldan 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( F ` ( n + 1 ) ) e. CC )
46 45 ancoms 
 |-  ( ( n e. ( ZZ>= ` N ) /\ ph ) -> ( F ` ( n + 1 ) ) e. CC )
47 46 mul02d 
 |-  ( ( n e. ( ZZ>= ` N ) /\ ph ) -> ( 0 x. ( F ` ( n + 1 ) ) ) = 0 )
48 47 3adant3 
 |-  ( ( n e. ( ZZ>= ` N ) /\ ph /\ ( seq M ( x. , F ) ` n ) = 0 ) -> ( 0 x. ( F ` ( n + 1 ) ) ) = 0 )
49 34 36 48 3eqtrd 
 |-  ( ( n e. ( ZZ>= ` N ) /\ ph /\ ( seq M ( x. , F ) ` n ) = 0 ) -> ( seq M ( x. , F ) ` ( n + 1 ) ) = 0 )
50 49 3exp 
 |-  ( n e. ( ZZ>= ` N ) -> ( ph -> ( ( seq M ( x. , F ) ` n ) = 0 -> ( seq M ( x. , F ) ` ( n + 1 ) ) = 0 ) ) )
51 50 adantrd 
 |-  ( n e. ( ZZ>= ` N ) -> ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> ( ( seq M ( x. , F ) ` n ) = 0 -> ( seq M ( x. , F ) ` ( n + 1 ) ) = 0 ) ) )
52 51 a2d 
 |-  ( n e. ( ZZ>= ` N ) -> ( ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> ( seq M ( x. , F ) ` n ) = 0 ) -> ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> ( seq M ( x. , F ) ` ( n + 1 ) ) = 0 ) ) )
53 21 23 25 27 28 52 uzind4i 
 |-  ( k e. ( ZZ>= ` N ) -> ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> ( seq M ( x. , F ) ` k ) = 0 ) )
54 53 impcom 
 |-  ( ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) /\ k e. ( ZZ>= ` N ) ) -> ( seq M ( x. , F ) ` k ) = 0 )
55 12 16 18 19 54 climconst 
 |-  ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> seq M ( x. , F ) ~~> 0 )
56 funbrfv 
 |-  ( Fun ~~> -> ( seq M ( x. , F ) ~~> 0 -> ( ~~> ` seq M ( x. , F ) ) = 0 ) )
57 8 55 56 mpsyl 
 |-  ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> ( ~~> ` seq M ( x. , F ) ) = 0 )
58 11 57 eqtr3d 
 |-  ( ( ph /\ ( seq M ( x. , F ) ` N ) = 0 ) -> X = 0 )
59 58 ex 
 |-  ( ph -> ( ( seq M ( x. , F ) ` N ) = 0 -> X = 0 ) )
60 59 necon3d 
 |-  ( ph -> ( X =/= 0 -> ( seq M ( x. , F ) ` N ) =/= 0 ) )
61 4 60 mpd 
 |-  ( ph -> ( seq M ( x. , F ) ` N ) =/= 0 )