Metamath Proof Explorer

Theorem cvgdvgrat

Description: Ratio test for convergence and divergence of a complex infinite series. If the ratio R of the absolute values of successive terms in an infinite sequence F converges to less than one, then the infinite sum of the terms of F converges to a complex number; and if R convergesgreater then the sum diverges. This combined form of cvgrat and dvgrat directly uses the limit of the ratio.

(It also demonstrates how to use climi2 and absltd to transform a limit to an inequality cf. https://math.stackexchange.com/q/2215191 , and how to use r19.29a in a similar fashion to Mario Carneiro's proof sketch with rexlimdva at https://groups.google.com/g/metamath/c/2RPikOiXLMo .) (Contributed by Steve Rodriguez, 28-Feb-2020)

Ref Expression
Hypotheses cvgdvgrat.z 
|- Z = ( ZZ>= ` M )
cvgdvgrat.w 
|- W = ( ZZ>= ` N )
cvgdvgrat.n 
|- ( ph -> N e. Z )
cvgdvgrat.f 
|- ( ph -> F e. V )
cvgdvgrat.c 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
cvgdvgrat.n0 
|- ( ( ph /\ k e. W ) -> ( F ` k ) =/= 0 )
cvgdvgrat.r 
|- R = ( k e. W |-> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) )
cvgdvgrat.cvg 
|- ( ph -> R ~~> L )
cvgdvgrat.n1 
|- ( ph -> L =/= 1 )
Assertion cvgdvgrat 
|- ( ph -> ( L < 1 <-> seq M ( + , F ) e. dom ~~> ) )

Proof

Step Hyp Ref Expression
1 cvgdvgrat.z 
 |-  Z = ( ZZ>= ` M )
2 cvgdvgrat.w 
 |-  W = ( ZZ>= ` N )
3 cvgdvgrat.n 
 |-  ( ph -> N e. Z )
4 cvgdvgrat.f 
 |-  ( ph -> F e. V )
5 cvgdvgrat.c 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
6 cvgdvgrat.n0 
 |-  ( ( ph /\ k e. W ) -> ( F ` k ) =/= 0 )
7 cvgdvgrat.r 
 |-  R = ( k e. W |-> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) )
8 cvgdvgrat.cvg 
 |-  ( ph -> R ~~> L )
9 cvgdvgrat.n1 
 |-  ( ph -> L =/= 1 )
10 eqid 
 |-  ( ZZ>= ` n ) = ( ZZ>= ` n )
11 elioore 
 |-  ( r e. ( L (,) 1 ) -> r e. RR )
12 11 ad3antlr 
 |-  ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ A. k e. ( ZZ>= ` n ) ( abs ` ( F ` ( k + 1 ) ) ) <_ ( r x. ( abs ` ( F ` k ) ) ) ) -> r e. RR )
13 3 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
14 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
15 13 14 syl 
 |-  ( ph -> N e. ZZ )
16 7 a1i 
 |-  ( ph -> R = ( k e. W |-> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) ) )
17 2 peano2uzs 
 |-  ( k e. W -> ( k + 1 ) e. W )
18 ovex 
 |-  ( k + 1 ) e. _V
19 eleq1 
 |-  ( i = ( k + 1 ) -> ( i e. W <-> ( k + 1 ) e. W ) )
20 19 anbi2d 
 |-  ( i = ( k + 1 ) -> ( ( ph /\ i e. W ) <-> ( ph /\ ( k + 1 ) e. W ) ) )
21 fveq2 
 |-  ( i = ( k + 1 ) -> ( F ` i ) = ( F ` ( k + 1 ) ) )
22 21 eleq1d 
 |-  ( i = ( k + 1 ) -> ( ( F ` i ) e. CC <-> ( F ` ( k + 1 ) ) e. CC ) )
23 20 22 imbi12d 
 |-  ( i = ( k + 1 ) -> ( ( ( ph /\ i e. W ) -> ( F ` i ) e. CC ) <-> ( ( ph /\ ( k + 1 ) e. W ) -> ( F ` ( k + 1 ) ) e. CC ) ) )
24 eleq1 
 |-  ( k = i -> ( k e. W <-> i e. W ) )
25 24 anbi2d 
 |-  ( k = i -> ( ( ph /\ k e. W ) <-> ( ph /\ i e. W ) ) )
26 fveq2 
 |-  ( k = i -> ( F ` k ) = ( F ` i ) )
27 26 eleq1d 
 |-  ( k = i -> ( ( F ` k ) e. CC <-> ( F ` i ) e. CC ) )
28 25 27 imbi12d 
 |-  ( k = i -> ( ( ( ph /\ k e. W ) -> ( F ` k ) e. CC ) <-> ( ( ph /\ i e. W ) -> ( F ` i ) e. CC ) ) )
29 2 eleq2i 
 |-  ( k e. W <-> k e. ( ZZ>= ` N ) )
30 1 uztrn2 
 |-  ( ( N e. Z /\ k e. ( ZZ>= ` N ) ) -> k e. Z )
31 3 30 sylan 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> k e. Z )
32 29 31 sylan2b 
 |-  ( ( ph /\ k e. W ) -> k e. Z )
33 32 5 syldan 
 |-  ( ( ph /\ k e. W ) -> ( F ` k ) e. CC )
34 28 33 chvarvv 
 |-  ( ( ph /\ i e. W ) -> ( F ` i ) e. CC )
35 18 23 34 vtocl 
 |-  ( ( ph /\ ( k + 1 ) e. W ) -> ( F ` ( k + 1 ) ) e. CC )
36 17 35 sylan2 
 |-  ( ( ph /\ k e. W ) -> ( F ` ( k + 1 ) ) e. CC )
37 36 33 6 divcld 
 |-  ( ( ph /\ k e. W ) -> ( ( F ` ( k + 1 ) ) / ( F ` k ) ) e. CC )
38 37 abscld 
 |-  ( ( ph /\ k e. W ) -> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) e. RR )
39 16 38 fvmpt2d 
 |-  ( ( ph /\ k e. W ) -> ( R ` k ) = ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) )
40 39 38 eqeltrd 
 |-  ( ( ph /\ k e. W ) -> ( R ` k ) e. RR )
41 2 15 8 40 climrecl 
 |-  ( ph -> L e. RR )
42 41 rexrd 
 |-  ( ph -> L e. RR* )
43 1xr 
 |-  1 e. RR*
44 elioo2 
 |-  ( ( L e. RR* /\ 1 e. RR* ) -> ( r e. ( L (,) 1 ) <-> ( r e. RR /\ L < r /\ r < 1 ) ) )
45 42 43 44 sylancl 
 |-  ( ph -> ( r e. ( L (,) 1 ) <-> ( r e. RR /\ L < r /\ r < 1 ) ) )
46 45 biimpa 
 |-  ( ( ph /\ r e. ( L (,) 1 ) ) -> ( r e. RR /\ L < r /\ r < 1 ) )
47 46 simp3d 
 |-  ( ( ph /\ r e. ( L (,) 1 ) ) -> r < 1 )
48 47 ad2antrr 
 |-  ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ A. k e. ( ZZ>= ` n ) ( abs ` ( F ` ( k + 1 ) ) ) <_ ( r x. ( abs ` ( F ` k ) ) ) ) -> r < 1 )
49 simplr 
 |-  ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ A. k e. ( ZZ>= ` n ) ( abs ` ( F ` ( k + 1 ) ) ) <_ ( r x. ( abs ` ( F ` k ) ) ) ) -> n e. W )
50 34 ex 
 |-  ( ph -> ( i e. W -> ( F ` i ) e. CC ) )
51 50 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ A. k e. ( ZZ>= ` n ) ( abs ` ( F ` ( k + 1 ) ) ) <_ ( r x. ( abs ` ( F ` k ) ) ) ) -> ( i e. W -> ( F ` i ) e. CC ) )
52 51 imp 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ A. k e. ( ZZ>= ` n ) ( abs ` ( F ` ( k + 1 ) ) ) <_ ( r x. ( abs ` ( F ` k ) ) ) ) /\ i e. W ) -> ( F ` i ) e. CC )
53 fvoveq1 
 |-  ( k = i -> ( F ` ( k + 1 ) ) = ( F ` ( i + 1 ) ) )
54 53 fveq2d 
 |-  ( k = i -> ( abs ` ( F ` ( k + 1 ) ) ) = ( abs ` ( F ` ( i + 1 ) ) ) )
55 26 fveq2d 
 |-  ( k = i -> ( abs ` ( F ` k ) ) = ( abs ` ( F ` i ) ) )
56 55 oveq2d 
 |-  ( k = i -> ( r x. ( abs ` ( F ` k ) ) ) = ( r x. ( abs ` ( F ` i ) ) ) )
57 54 56 breq12d 
 |-  ( k = i -> ( ( abs ` ( F ` ( k + 1 ) ) ) <_ ( r x. ( abs ` ( F ` k ) ) ) <-> ( abs ` ( F ` ( i + 1 ) ) ) <_ ( r x. ( abs ` ( F ` i ) ) ) ) )
58 57 rspccva 
 |-  ( ( A. k e. ( ZZ>= ` n ) ( abs ` ( F ` ( k + 1 ) ) ) <_ ( r x. ( abs ` ( F ` k ) ) ) /\ i e. ( ZZ>= ` n ) ) -> ( abs ` ( F ` ( i + 1 ) ) ) <_ ( r x. ( abs ` ( F ` i ) ) ) )
59 58 adantll 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ A. k e. ( ZZ>= ` n ) ( abs ` ( F ` ( k + 1 ) ) ) <_ ( r x. ( abs ` ( F ` k ) ) ) ) /\ i e. ( ZZ>= ` n ) ) -> ( abs ` ( F ` ( i + 1 ) ) ) <_ ( r x. ( abs ` ( F ` i ) ) ) )
60 2 10 12 48 49 52 59 cvgrat 
 |-  ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ A. k e. ( ZZ>= ` n ) ( abs ` ( F ` ( k + 1 ) ) ) <_ ( r x. ( abs ` ( F ` k ) ) ) ) -> seq N ( + , F ) e. dom ~~> )
61 15 adantr 
 |-  ( ( ph /\ r e. ( L (,) 1 ) ) -> N e. ZZ )
62 46 simp2d 
 |-  ( ( ph /\ r e. ( L (,) 1 ) ) -> L < r )
63 difrp 
 |-  ( ( L e. RR /\ r e. RR ) -> ( L < r <-> ( r - L ) e. RR+ ) )
64 41 11 63 syl2an 
 |-  ( ( ph /\ r e. ( L (,) 1 ) ) -> ( L < r <-> ( r - L ) e. RR+ ) )
65 62 64 mpbid 
 |-  ( ( ph /\ r e. ( L (,) 1 ) ) -> ( r - L ) e. RR+ )
66 39 adantlr 
 |-  ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ k e. W ) -> ( R ` k ) = ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) )
67 8 adantr 
 |-  ( ( ph /\ r e. ( L (,) 1 ) ) -> R ~~> L )
68 2 61 65 66 67 climi2 
 |-  ( ( ph /\ r e. ( L (,) 1 ) ) -> E. n e. W A. k e. ( ZZ>= ` n ) ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) )
69 2 uztrn2 
 |-  ( ( n e. W /\ k e. ( ZZ>= ` n ) ) -> k e. W )
70 69 36 sylan2 
 |-  ( ( ph /\ ( n e. W /\ k e. ( ZZ>= ` n ) ) ) -> ( F ` ( k + 1 ) ) e. CC )
71 70 anassrs 
 |-  ( ( ( ph /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( F ` ( k + 1 ) ) e. CC )
72 71 adantllr 
 |-  ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( F ` ( k + 1 ) ) e. CC )
73 72 adantr 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( F ` ( k + 1 ) ) e. CC )
74 73 abscld 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( abs ` ( F ` ( k + 1 ) ) ) e. RR )
75 11 ad4antlr 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> r e. RR )
76 69 33 sylan2 
 |-  ( ( ph /\ ( n e. W /\ k e. ( ZZ>= ` n ) ) ) -> ( F ` k ) e. CC )
77 76 anassrs 
 |-  ( ( ( ph /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( F ` k ) e. CC )
78 77 adantllr 
 |-  ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( F ` k ) e. CC )
79 78 adantr 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( F ` k ) e. CC )
80 79 abscld 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( abs ` ( F ` k ) ) e. RR )
81 75 80 remulcld 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( r x. ( abs ` ( F ` k ) ) ) e. RR )
82 69 6 sylan2 
 |-  ( ( ph /\ ( n e. W /\ k e. ( ZZ>= ` n ) ) ) -> ( F ` k ) =/= 0 )
83 82 anassrs 
 |-  ( ( ( ph /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( F ` k ) =/= 0 )
84 83 adantllr 
 |-  ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( F ` k ) =/= 0 )
85 84 adantr 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( F ` k ) =/= 0 )
86 73 79 85 absdivd 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) = ( ( abs ` ( F ` ( k + 1 ) ) ) / ( abs ` ( F ` k ) ) ) )
87 72 78 84 divcld 
 |-  ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( ( F ` ( k + 1 ) ) / ( F ` k ) ) e. CC )
88 87 abscld 
 |-  ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) e. RR )
89 41 ad3antrrr 
 |-  ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> L e. RR )
90 88 89 resubcld 
 |-  ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) e. RR )
91 11 ad3antlr 
 |-  ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> r e. RR )
92 91 89 resubcld 
 |-  ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( r - L ) e. RR )
93 90 92 absltd 
 |-  ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) <-> ( -u ( r - L ) < ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) /\ ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) < ( r - L ) ) ) )
94 93 simplbda 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) < ( r - L ) )
95 73 79 85 divcld 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( ( F ` ( k + 1 ) ) / ( F ` k ) ) e. CC )
96 95 abscld 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) e. RR )
97 41 ad4antr 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> L e. RR )
98 96 75 97 ltsub1d 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) < r <-> ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) < ( r - L ) ) )
99 94 98 mpbird 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) < r )
100 86 99 eqbrtrrd 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( ( abs ` ( F ` ( k + 1 ) ) ) / ( abs ` ( F ` k ) ) ) < r )
101 79 85 absrpcld 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( abs ` ( F ` k ) ) e. RR+ )
102 74 75 101 ltdivmuld 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( ( ( abs ` ( F ` ( k + 1 ) ) ) / ( abs ` ( F ` k ) ) ) < r <-> ( abs ` ( F ` ( k + 1 ) ) ) < ( ( abs ` ( F ` k ) ) x. r ) ) )
103 100 102 mpbid 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( abs ` ( F ` ( k + 1 ) ) ) < ( ( abs ` ( F ` k ) ) x. r ) )
104 101 rpcnd 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( abs ` ( F ` k ) ) e. CC )
105 75 recnd 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> r e. CC )
106 104 105 mulcomd 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( ( abs ` ( F ` k ) ) x. r ) = ( r x. ( abs ` ( F ` k ) ) ) )
107 103 106 breqtrd 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( abs ` ( F ` ( k + 1 ) ) ) < ( r x. ( abs ` ( F ` k ) ) ) )
108 74 81 107 ltled 
 |-  ( ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( r x. ( abs ` ( F ` k ) ) ) )
109 108 ex 
 |-  ( ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) -> ( abs ` ( F ` ( k + 1 ) ) ) <_ ( r x. ( abs ` ( F ` k ) ) ) ) )
110 109 ralimdva 
 |-  ( ( ( ph /\ r e. ( L (,) 1 ) ) /\ n e. W ) -> ( A. k e. ( ZZ>= ` n ) ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) -> A. k e. ( ZZ>= ` n ) ( abs ` ( F ` ( k + 1 ) ) ) <_ ( r x. ( abs ` ( F ` k ) ) ) ) )
111 110 reximdva 
 |-  ( ( ph /\ r e. ( L (,) 1 ) ) -> ( E. n e. W A. k e. ( ZZ>= ` n ) ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( r - L ) -> E. n e. W A. k e. ( ZZ>= ` n ) ( abs ` ( F ` ( k + 1 ) ) ) <_ ( r x. ( abs ` ( F ` k ) ) ) ) )
112 68 111 mpd 
 |-  ( ( ph /\ r e. ( L (,) 1 ) ) -> E. n e. W A. k e. ( ZZ>= ` n ) ( abs ` ( F ` ( k + 1 ) ) ) <_ ( r x. ( abs ` ( F ` k ) ) ) )
113 60 112 r19.29a 
 |-  ( ( ph /\ r e. ( L (,) 1 ) ) -> seq N ( + , F ) e. dom ~~> )
114 113 ralrimiva 
 |-  ( ph -> A. r e. ( L (,) 1 ) seq N ( + , F ) e. dom ~~> )
115 114 adantr 
 |-  ( ( ph /\ L < 1 ) -> A. r e. ( L (,) 1 ) seq N ( + , F ) e. dom ~~> )
116 ioon0 
 |-  ( ( L e. RR* /\ 1 e. RR* ) -> ( ( L (,) 1 ) =/= (/) <-> L < 1 ) )
117 42 43 116 sylancl 
 |-  ( ph -> ( ( L (,) 1 ) =/= (/) <-> L < 1 ) )
118 117 biimpar 
 |-  ( ( ph /\ L < 1 ) -> ( L (,) 1 ) =/= (/) )
119 r19.3rzv 
 |-  ( ( L (,) 1 ) =/= (/) -> ( seq N ( + , F ) e. dom ~~> <-> A. r e. ( L (,) 1 ) seq N ( + , F ) e. dom ~~> ) )
120 118 119 syl 
 |-  ( ( ph /\ L < 1 ) -> ( seq N ( + , F ) e. dom ~~> <-> A. r e. ( L (,) 1 ) seq N ( + , F ) e. dom ~~> ) )
121 115 120 mpbird 
 |-  ( ( ph /\ L < 1 ) -> seq N ( + , F ) e. dom ~~> )
122 1 3 5 iserex 
 |-  ( ph -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) )
123 122 adantr 
 |-  ( ( ph /\ L < 1 ) -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) )
124 121 123 mpbird 
 |-  ( ( ph /\ L < 1 ) -> seq M ( + , F ) e. dom ~~> )
125 124 ex 
 |-  ( ph -> ( L < 1 -> seq M ( + , F ) e. dom ~~> ) )
126 1red 
 |-  ( ph -> 1 e. RR )
127 41 126 lttri2d 
 |-  ( ph -> ( L =/= 1 <-> ( L < 1 \/ 1 < L ) ) )
128 9 127 mpbid 
 |-  ( ph -> ( L < 1 \/ 1 < L ) )
129 128 orcanai 
 |-  ( ( ph /\ -. L < 1 ) -> 1 < L )
130 simplr 
 |-  ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) ) -> n e. W )
131 4 ad3antrrr 
 |-  ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) ) -> F e. V )
132 50 ad3antrrr 
 |-  ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) ) -> ( i e. W -> ( F ` i ) e. CC ) )
133 132 imp 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) ) /\ i e. W ) -> ( F ` i ) e. CC )
134 2 uztrn2 
 |-  ( ( n e. W /\ i e. ( ZZ>= ` n ) ) -> i e. W )
135 26 neeq1d 
 |-  ( k = i -> ( ( F ` k ) =/= 0 <-> ( F ` i ) =/= 0 ) )
136 25 135 imbi12d 
 |-  ( k = i -> ( ( ( ph /\ k e. W ) -> ( F ` k ) =/= 0 ) <-> ( ( ph /\ i e. W ) -> ( F ` i ) =/= 0 ) ) )
137 136 6 chvarvv 
 |-  ( ( ph /\ i e. W ) -> ( F ` i ) =/= 0 )
138 134 137 sylan2 
 |-  ( ( ph /\ ( n e. W /\ i e. ( ZZ>= ` n ) ) ) -> ( F ` i ) =/= 0 )
139 138 anassrs 
 |-  ( ( ( ph /\ n e. W ) /\ i e. ( ZZ>= ` n ) ) -> ( F ` i ) =/= 0 )
140 139 adantllr 
 |-  ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ i e. ( ZZ>= ` n ) ) -> ( F ` i ) =/= 0 )
141 140 adantlr 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) ) /\ i e. ( ZZ>= ` n ) ) -> ( F ` i ) =/= 0 )
142 55 54 breq12d 
 |-  ( k = i -> ( ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) <-> ( abs ` ( F ` i ) ) <_ ( abs ` ( F ` ( i + 1 ) ) ) ) )
143 142 rspccva 
 |-  ( ( A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) /\ i e. ( ZZ>= ` n ) ) -> ( abs ` ( F ` i ) ) <_ ( abs ` ( F ` ( i + 1 ) ) ) )
144 143 adantll 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) ) /\ i e. ( ZZ>= ` n ) ) -> ( abs ` ( F ` i ) ) <_ ( abs ` ( F ` ( i + 1 ) ) ) )
145 2 10 130 131 133 141 144 dvgrat 
 |-  ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) ) -> seq N ( + , F ) e/ dom ~~> )
146 15 adantr 
 |-  ( ( ph /\ 1 < L ) -> N e. ZZ )
147 1re 
 |-  1 e. RR
148 difrp 
 |-  ( ( 1 e. RR /\ L e. RR ) -> ( 1 < L <-> ( L - 1 ) e. RR+ ) )
149 147 41 148 sylancr 
 |-  ( ph -> ( 1 < L <-> ( L - 1 ) e. RR+ ) )
150 149 biimpa 
 |-  ( ( ph /\ 1 < L ) -> ( L - 1 ) e. RR+ )
151 39 adantlr 
 |-  ( ( ( ph /\ 1 < L ) /\ k e. W ) -> ( R ` k ) = ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) )
152 8 adantr 
 |-  ( ( ph /\ 1 < L ) -> R ~~> L )
153 2 146 150 151 152 climi2 
 |-  ( ( ph /\ 1 < L ) -> E. n e. W A. k e. ( ZZ>= ` n ) ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) )
154 77 adantllr 
 |-  ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( F ` k ) e. CC )
155 154 adantr 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( F ` k ) e. CC )
156 155 abscld 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( abs ` ( F ` k ) ) e. RR )
157 71 adantllr 
 |-  ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( F ` ( k + 1 ) ) e. CC )
158 157 adantr 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( F ` ( k + 1 ) ) e. CC )
159 158 abscld 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( abs ` ( F ` ( k + 1 ) ) ) e. RR )
160 83 adantllr 
 |-  ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( F ` k ) =/= 0 )
161 160 adantr 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( F ` k ) =/= 0 )
162 155 161 absrpcld 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( abs ` ( F ` k ) ) e. RR+ )
163 162 rpcnd 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( abs ` ( F ` k ) ) e. CC )
164 163 mulid2d 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( 1 x. ( abs ` ( F ` k ) ) ) = ( abs ` ( F ` k ) ) )
165 41 ad4antr 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> L e. RR )
166 165 recnd 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> L e. CC )
167 1cnd 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> 1 e. CC )
168 166 167 negsubdi2d 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> -u ( L - 1 ) = ( 1 - L ) )
169 157 154 160 divcld 
 |-  ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( ( F ` ( k + 1 ) ) / ( F ` k ) ) e. CC )
170 169 abscld 
 |-  ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) e. RR )
171 41 ad3antrrr 
 |-  ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> L e. RR )
172 170 171 resubcld 
 |-  ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) e. RR )
173 1red 
 |-  ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> 1 e. RR )
174 171 173 resubcld 
 |-  ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( L - 1 ) e. RR )
175 172 174 absltd 
 |-  ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) <-> ( -u ( L - 1 ) < ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) /\ ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) < ( L - 1 ) ) ) )
176 175 simprbda 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> -u ( L - 1 ) < ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) )
177 168 176 eqbrtrrd 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( 1 - L ) < ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) )
178 1red 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> 1 e. RR )
179 158 155 161 divcld 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( ( F ` ( k + 1 ) ) / ( F ` k ) ) e. CC )
180 179 abscld 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) e. RR )
181 178 180 165 ltsub1d 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( 1 < ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) <-> ( 1 - L ) < ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) )
182 177 181 mpbird 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> 1 < ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) )
183 158 155 161 absdivd 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) = ( ( abs ` ( F ` ( k + 1 ) ) ) / ( abs ` ( F ` k ) ) ) )
184 182 183 breqtrd 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> 1 < ( ( abs ` ( F ` ( k + 1 ) ) ) / ( abs ` ( F ` k ) ) ) )
185 178 159 162 ltmuldivd 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( ( 1 x. ( abs ` ( F ` k ) ) ) < ( abs ` ( F ` ( k + 1 ) ) ) <-> 1 < ( ( abs ` ( F ` ( k + 1 ) ) ) / ( abs ` ( F ` k ) ) ) ) )
186 184 185 mpbird 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( 1 x. ( abs ` ( F ` k ) ) ) < ( abs ` ( F ` ( k + 1 ) ) ) )
187 164 186 eqbrtrrd 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( abs ` ( F ` k ) ) < ( abs ` ( F ` ( k + 1 ) ) ) )
188 156 159 187 ltled 
 |-  ( ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) /\ ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) ) -> ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) )
189 188 ex 
 |-  ( ( ( ( ph /\ 1 < L ) /\ n e. W ) /\ k e. ( ZZ>= ` n ) ) -> ( ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) -> ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) ) )
190 189 ralimdva 
 |-  ( ( ( ph /\ 1 < L ) /\ n e. W ) -> ( A. k e. ( ZZ>= ` n ) ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) -> A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) ) )
191 190 reximdva 
 |-  ( ( ph /\ 1 < L ) -> ( E. n e. W A. k e. ( ZZ>= ` n ) ( abs ` ( ( abs ` ( ( F ` ( k + 1 ) ) / ( F ` k ) ) ) - L ) ) < ( L - 1 ) -> E. n e. W A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) ) )
192 153 191 mpd 
 |-  ( ( ph /\ 1 < L ) -> E. n e. W A. k e. ( ZZ>= ` n ) ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) )
193 145 192 r19.29a 
 |-  ( ( ph /\ 1 < L ) -> seq N ( + , F ) e/ dom ~~> )
194 df-nel 
 |-  ( seq N ( + , F ) e/ dom ~~> <-> -. seq N ( + , F ) e. dom ~~> )
195 193 194 sylib 
 |-  ( ( ph /\ 1 < L ) -> -. seq N ( + , F ) e. dom ~~> )
196 122 adantr 
 |-  ( ( ph /\ 1 < L ) -> ( seq M ( + , F ) e. dom ~~> <-> seq N ( + , F ) e. dom ~~> ) )
197 195 196 mtbird 
 |-  ( ( ph /\ 1 < L ) -> -. seq M ( + , F ) e. dom ~~> )
198 129 197 syldan 
 |-  ( ( ph /\ -. L < 1 ) -> -. seq M ( + , F ) e. dom ~~> )
199 198 ex 
 |-  ( ph -> ( -. L < 1 -> -. seq M ( + , F ) e. dom ~~> ) )
200 125 199 impcon4bid 
 |-  ( ph -> ( L < 1 <-> seq M ( + , F ) e. dom ~~> ) )