Metamath Proof Explorer

Theorem ntrivcvgtail

Description: A tail of a non-trivially convergent sequence converges non-trivially. (Contributed by Scott Fenton, 20-Dec-2017)

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

Proof

Step Hyp Ref Expression
1 ntrivcvgtail.1 
 |-  Z = ( ZZ>= ` M )
2 ntrivcvgtail.2 
 |-  ( ph -> N e. Z )
3 ntrivcvgtail.3 
 |-  ( ph -> seq M ( x. , F ) ~~> X )
4 ntrivcvgtail.4 
 |-  ( ph -> X =/= 0 )
5 ntrivcvgtail.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 4 eqnetrd 
 |-  ( ph -> ( ~~> ` seq M ( x. , F ) ) =/= 0 )
12 3 10 breqtrrd 
 |-  ( ph -> seq M ( x. , F ) ~~> ( ~~> ` seq M ( x. , F ) ) )
13 11 12 jca 
 |-  ( ph -> ( ( ~~> ` seq M ( x. , F ) ) =/= 0 /\ seq M ( x. , F ) ~~> ( ~~> ` seq M ( x. , F ) ) ) )
14 13 adantr 
 |-  ( ( ph /\ N = M ) -> ( ( ~~> ` seq M ( x. , F ) ) =/= 0 /\ seq M ( x. , F ) ~~> ( ~~> ` seq M ( x. , F ) ) ) )
15 seqeq1 
 |-  ( N = M -> seq N ( x. , F ) = seq M ( x. , F ) )
16 15 fveq2d 
 |-  ( N = M -> ( ~~> ` seq N ( x. , F ) ) = ( ~~> ` seq M ( x. , F ) ) )
17 16 neeq1d 
 |-  ( N = M -> ( ( ~~> ` seq N ( x. , F ) ) =/= 0 <-> ( ~~> ` seq M ( x. , F ) ) =/= 0 ) )
18 15 16 breq12d 
 |-  ( N = M -> ( seq N ( x. , F ) ~~> ( ~~> ` seq N ( x. , F ) ) <-> seq M ( x. , F ) ~~> ( ~~> ` seq M ( x. , F ) ) ) )
19 17 18 anbi12d 
 |-  ( N = M -> ( ( ( ~~> ` seq N ( x. , F ) ) =/= 0 /\ seq N ( x. , F ) ~~> ( ~~> ` seq N ( x. , F ) ) ) <-> ( ( ~~> ` seq M ( x. , F ) ) =/= 0 /\ seq M ( x. , F ) ~~> ( ~~> ` seq M ( x. , F ) ) ) ) )
20 19 adantl 
 |-  ( ( ph /\ N = M ) -> ( ( ( ~~> ` seq N ( x. , F ) ) =/= 0 /\ seq N ( x. , F ) ~~> ( ~~> ` seq N ( x. , F ) ) ) <-> ( ( ~~> ` seq M ( x. , F ) ) =/= 0 /\ seq M ( x. , F ) ~~> ( ~~> ` seq M ( x. , F ) ) ) ) )
21 14 20 mpbird 
 |-  ( ( ph /\ N = M ) -> ( ( ~~> ` seq N ( x. , F ) ) =/= 0 /\ seq N ( x. , F ) ~~> ( ~~> ` seq N ( x. , F ) ) ) )
22 simpr 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )
23 22 1 eleqtrrdi 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( N - 1 ) e. Z )
24 5 adantlr 
 |-  ( ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) /\ k e. Z ) -> ( F ` k ) e. CC )
25 3 adantr 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> seq M ( x. , F ) ~~> X )
26 4 adantr 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> X =/= 0 )
27 1 23 25 26 24 ntrivcvgfvn0 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( seq M ( x. , F ) ` ( N - 1 ) ) =/= 0 )
28 1 23 24 25 27 clim2div 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> seq ( ( N - 1 ) + 1 ) ( x. , F ) ~~> ( X / ( seq M ( x. , F ) ` ( N - 1 ) ) ) )
29 funbrfv 
 |-  ( Fun ~~> -> ( seq ( ( N - 1 ) + 1 ) ( x. , F ) ~~> ( X / ( seq M ( x. , F ) ` ( N - 1 ) ) ) -> ( ~~> ` seq ( ( N - 1 ) + 1 ) ( x. , F ) ) = ( X / ( seq M ( x. , F ) ` ( N - 1 ) ) ) ) )
30 8 28 29 mpsyl 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( ~~> ` seq ( ( N - 1 ) + 1 ) ( x. , F ) ) = ( X / ( seq M ( x. , F ) ` ( N - 1 ) ) ) )
31 climcl 
 |-  ( seq M ( x. , F ) ~~> X -> X e. CC )
32 3 31 syl 
 |-  ( ph -> X e. CC )
33 32 adantr 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> X e. CC )
34 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
35 34 1 eleq2s 
 |-  ( N e. Z -> M e. ZZ )
36 2 35 syl 
 |-  ( ph -> M e. ZZ )
37 1 36 5 prodf 
 |-  ( ph -> seq M ( x. , F ) : Z --> CC )
38 1 feq2i 
 |-  ( seq M ( x. , F ) : Z --> CC <-> seq M ( x. , F ) : ( ZZ>= ` M ) --> CC )
39 37 38 sylib 
 |-  ( ph -> seq M ( x. , F ) : ( ZZ>= ` M ) --> CC )
40 39 ffvelrnda 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( seq M ( x. , F ) ` ( N - 1 ) ) e. CC )
41 33 40 26 27 divne0d 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( X / ( seq M ( x. , F ) ` ( N - 1 ) ) ) =/= 0 )
42 30 41 eqnetrd 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( ~~> ` seq ( ( N - 1 ) + 1 ) ( x. , F ) ) =/= 0 )
43 28 30 breqtrrd 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> seq ( ( N - 1 ) + 1 ) ( x. , F ) ~~> ( ~~> ` seq ( ( N - 1 ) + 1 ) ( x. , F ) ) )
44 uzssz 
 |-  ( ZZ>= ` M ) C_ ZZ
45 1 44 eqsstri 
 |-  Z C_ ZZ
46 45 2 sselid 
 |-  ( ph -> N e. ZZ )
47 46 zcnd 
 |-  ( ph -> N e. CC )
48 47 adantr 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> N e. CC )
49 1cnd 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> 1 e. CC )
50 48 49 npcand 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( ( N - 1 ) + 1 ) = N )
51 50 seqeq1d 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> seq ( ( N - 1 ) + 1 ) ( x. , F ) = seq N ( x. , F ) )
52 51 fveq2d 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( ~~> ` seq ( ( N - 1 ) + 1 ) ( x. , F ) ) = ( ~~> ` seq N ( x. , F ) ) )
53 52 neeq1d 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( ( ~~> ` seq ( ( N - 1 ) + 1 ) ( x. , F ) ) =/= 0 <-> ( ~~> ` seq N ( x. , F ) ) =/= 0 ) )
54 51 52 breq12d 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( seq ( ( N - 1 ) + 1 ) ( x. , F ) ~~> ( ~~> ` seq ( ( N - 1 ) + 1 ) ( x. , F ) ) <-> seq N ( x. , F ) ~~> ( ~~> ` seq N ( x. , F ) ) ) )
55 53 54 anbi12d 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( ( ( ~~> ` seq ( ( N - 1 ) + 1 ) ( x. , F ) ) =/= 0 /\ seq ( ( N - 1 ) + 1 ) ( x. , F ) ~~> ( ~~> ` seq ( ( N - 1 ) + 1 ) ( x. , F ) ) ) <-> ( ( ~~> ` seq N ( x. , F ) ) =/= 0 /\ seq N ( x. , F ) ~~> ( ~~> ` seq N ( x. , F ) ) ) ) )
56 42 43 55 mpbi2and 
 |-  ( ( ph /\ ( N - 1 ) e. ( ZZ>= ` M ) ) -> ( ( ~~> ` seq N ( x. , F ) ) =/= 0 /\ seq N ( x. , F ) ~~> ( ~~> ` seq N ( x. , F ) ) ) )
57 2 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
58 uzm1 
 |-  ( N e. ( ZZ>= ` M ) -> ( N = M \/ ( N - 1 ) e. ( ZZ>= ` M ) ) )
59 57 58 syl 
 |-  ( ph -> ( N = M \/ ( N - 1 ) e. ( ZZ>= ` M ) ) )
60 21 56 59 mpjaodan 
 |-  ( ph -> ( ( ~~> ` seq N ( x. , F ) ) =/= 0 /\ seq N ( x. , F ) ~~> ( ~~> ` seq N ( x. , F ) ) ) )