Metamath Proof Explorer

Theorem dvgrat

Description: Ratio test for divergence of a complex infinite series. See e.g. remark "if ( abs( ( a( n + 1 ) ) / ( an ) ) ) >_ 1 for all large n..." in https://en.wikipedia.org/wiki/Ratio_test#The_test . (Contributed by Steve Rodriguez, 28-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 dvgrat.z 
 |-  Z = ( ZZ>= ` M )
2 dvgrat.w 
 |-  W = ( ZZ>= ` N )
3 dvgrat.n 
 |-  ( ph -> N e. Z )
4 dvgrat.f 
 |-  ( ph -> F e. V )
5 dvgrat.c 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
6 dvgrat.n0 
 |-  ( ( ph /\ k e. W ) -> ( F ` k ) =/= 0 )
7 dvgrat.le 
 |-  ( ( ph /\ k e. W ) -> ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) )
8 3 1 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
9 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
10 8 9 syl 
 |-  ( ph -> N e. ZZ )
11 uzid 
 |-  ( N e. ZZ -> N e. ( ZZ>= ` N ) )
12 11 2 eleqtrrdi 
 |-  ( N e. ZZ -> N e. W )
13 10 12 syl 
 |-  ( ph -> N e. W )
14 simpr 
 |-  ( ( ph /\ k = N ) -> k = N )
15 14 eleq1d 
 |-  ( ( ph /\ k = N ) -> ( k e. W <-> N e. W ) )
16 14 fveq2d 
 |-  ( ( ph /\ k = N ) -> ( F ` k ) = ( F ` N ) )
17 16 fveq2d 
 |-  ( ( ph /\ k = N ) -> ( abs ` ( F ` k ) ) = ( abs ` ( F ` N ) ) )
18 17 breq2d 
 |-  ( ( ph /\ k = N ) -> ( 0 < ( abs ` ( F ` k ) ) <-> 0 < ( abs ` ( F ` N ) ) ) )
19 15 18 imbi12d 
 |-  ( ( ph /\ k = N ) -> ( ( k e. W -> 0 < ( abs ` ( F ` k ) ) ) <-> ( N e. W -> 0 < ( abs ` ( F ` N ) ) ) ) )
20 2 eleq2i 
 |-  ( k e. W <-> k e. ( ZZ>= ` N ) )
21 1 uztrn2 
 |-  ( ( N e. Z /\ k e. ( ZZ>= ` N ) ) -> k e. Z )
22 20 21 sylan2b 
 |-  ( ( N e. Z /\ k e. W ) -> k e. Z )
23 3 22 sylan 
 |-  ( ( ph /\ k e. W ) -> k e. Z )
24 23 5 syldan 
 |-  ( ( ph /\ k e. W ) -> ( F ` k ) e. CC )
25 absgt0 
 |-  ( ( F ` k ) e. CC -> ( ( F ` k ) =/= 0 <-> 0 < ( abs ` ( F ` k ) ) ) )
26 24 25 syl 
 |-  ( ( ph /\ k e. W ) -> ( ( F ` k ) =/= 0 <-> 0 < ( abs ` ( F ` k ) ) ) )
27 6 26 mpbid 
 |-  ( ( ph /\ k e. W ) -> 0 < ( abs ` ( F ` k ) ) )
28 27 ex 
 |-  ( ph -> ( k e. W -> 0 < ( abs ` ( F ` k ) ) ) )
29 3 19 28 vtocld 
 |-  ( ph -> ( N e. W -> 0 < ( abs ` ( F ` N ) ) ) )
30 13 29 mpd 
 |-  ( ph -> 0 < ( abs ` ( F ` N ) ) )
31 0red 
 |-  ( ph -> 0 e. RR )
32 14 eleq1d 
 |-  ( ( ph /\ k = N ) -> ( k e. Z <-> N e. Z ) )
33 16 eleq1d 
 |-  ( ( ph /\ k = N ) -> ( ( F ` k ) e. CC <-> ( F ` N ) e. CC ) )
34 32 33 imbi12d 
 |-  ( ( ph /\ k = N ) -> ( ( k e. Z -> ( F ` k ) e. CC ) <-> ( N e. Z -> ( F ` N ) e. CC ) ) )
35 5 ex 
 |-  ( ph -> ( k e. Z -> ( F ` k ) e. CC ) )
36 3 34 35 vtocld 
 |-  ( ph -> ( N e. Z -> ( F ` N ) e. CC ) )
37 3 36 mpd 
 |-  ( ph -> ( F ` N ) e. CC )
38 37 abscld 
 |-  ( ph -> ( abs ` ( F ` N ) ) e. RR )
39 31 38 ltnled 
 |-  ( ph -> ( 0 < ( abs ` ( F ` N ) ) <-> -. ( abs ` ( F ` N ) ) <_ 0 ) )
40 30 39 mpbid 
 |-  ( ph -> -. ( abs ` ( F ` N ) ) <_ 0 )
41 10 adantr 
 |-  ( ( ph /\ F ~~> 0 ) -> N e. ZZ )
42 38 adantr 
 |-  ( ( ph /\ F ~~> 0 ) -> ( abs ` ( F ` N ) ) e. RR )
43 simpr 
 |-  ( ( ph /\ F ~~> 0 ) -> F ~~> 0 )
44 2 fvexi 
 |-  W e. _V
45 44 mptex 
 |-  ( i e. W |-> ( abs ` ( F ` i ) ) ) e. _V
46 45 a1i 
 |-  ( ( ph /\ F ~~> 0 ) -> ( i e. W |-> ( abs ` ( F ` i ) ) ) e. _V )
47 24 adantlr 
 |-  ( ( ( ph /\ F ~~> 0 ) /\ k e. W ) -> ( F ` k ) e. CC )
48 eqidd 
 |-  ( ( ( ph /\ F ~~> 0 ) /\ k e. W ) -> ( i e. W |-> ( abs ` ( F ` i ) ) ) = ( i e. W |-> ( abs ` ( F ` i ) ) ) )
49 simpr 
 |-  ( ( ( ( ph /\ F ~~> 0 ) /\ k e. W ) /\ i = k ) -> i = k )
50 49 fveq2d 
 |-  ( ( ( ( ph /\ F ~~> 0 ) /\ k e. W ) /\ i = k ) -> ( F ` i ) = ( F ` k ) )
51 50 fveq2d 
 |-  ( ( ( ( ph /\ F ~~> 0 ) /\ k e. W ) /\ i = k ) -> ( abs ` ( F ` i ) ) = ( abs ` ( F ` k ) ) )
52 simpr 
 |-  ( ( ( ph /\ F ~~> 0 ) /\ k e. W ) -> k e. W )
53 fvex 
 |-  ( abs ` ( F ` k ) ) e. _V
54 53 a1i 
 |-  ( ( ( ph /\ F ~~> 0 ) /\ k e. W ) -> ( abs ` ( F ` k ) ) e. _V )
55 48 51 52 54 fvmptd 
 |-  ( ( ( ph /\ F ~~> 0 ) /\ k e. W ) -> ( ( i e. W |-> ( abs ` ( F ` i ) ) ) ` k ) = ( abs ` ( F ` k ) ) )
56 2 43 46 41 47 55 climabs 
 |-  ( ( ph /\ F ~~> 0 ) -> ( i e. W |-> ( abs ` ( F ` i ) ) ) ~~> ( abs ` 0 ) )
57 abs0 
 |-  ( abs ` 0 ) = 0
58 56 57 breqtrdi 
 |-  ( ( ph /\ F ~~> 0 ) -> ( i e. W |-> ( abs ` ( F ` i ) ) ) ~~> 0 )
59 47 abscld 
 |-  ( ( ( ph /\ F ~~> 0 ) /\ k e. W ) -> ( abs ` ( F ` k ) ) e. RR )
60 55 59 eqeltrd 
 |-  ( ( ( ph /\ F ~~> 0 ) /\ k e. W ) -> ( ( i e. W |-> ( abs ` ( F ` i ) ) ) ` k ) e. RR )
61 2fveq3 
 |-  ( i = N -> ( abs ` ( F ` i ) ) = ( abs ` ( F ` N ) ) )
62 61 breq2d 
 |-  ( i = N -> ( ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` i ) ) <-> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` N ) ) ) )
63 62 imbi2d 
 |-  ( i = N -> ( ( ph -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` i ) ) ) <-> ( ph -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` N ) ) ) ) )
64 2fveq3 
 |-  ( i = k -> ( abs ` ( F ` i ) ) = ( abs ` ( F ` k ) ) )
65 64 breq2d 
 |-  ( i = k -> ( ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` i ) ) <-> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) ) )
66 65 imbi2d 
 |-  ( i = k -> ( ( ph -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` i ) ) ) <-> ( ph -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) ) ) )
67 2fveq3 
 |-  ( i = ( k + 1 ) -> ( abs ` ( F ` i ) ) = ( abs ` ( F ` ( k + 1 ) ) ) )
68 67 breq2d 
 |-  ( i = ( k + 1 ) -> ( ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` i ) ) <-> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) ) )
69 68 imbi2d 
 |-  ( i = ( k + 1 ) -> ( ( ph -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` i ) ) ) <-> ( ph -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) ) ) )
70 38 adantr 
 |-  ( ( ph /\ N e. ZZ ) -> ( abs ` ( F ` N ) ) e. RR )
71 70 leidd 
 |-  ( ( ph /\ N e. ZZ ) -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` N ) ) )
72 71 expcom 
 |-  ( N e. ZZ -> ( ph -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` N ) ) ) )
73 38 ad2antrr 
 |-  ( ( ( ph /\ k e. W ) /\ ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) ) -> ( abs ` ( F ` N ) ) e. RR )
74 24 adantr 
 |-  ( ( ( ph /\ k e. W ) /\ ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) ) -> ( F ` k ) e. CC )
75 74 abscld 
 |-  ( ( ( ph /\ k e. W ) /\ ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) ) -> ( abs ` ( F ` k ) ) e. RR )
76 2 peano2uzs 
 |-  ( k e. W -> ( k + 1 ) e. W )
77 ovex 
 |-  ( k + 1 ) e. _V
78 eleq1 
 |-  ( i = ( k + 1 ) -> ( i e. W <-> ( k + 1 ) e. W ) )
79 78 anbi2d 
 |-  ( i = ( k + 1 ) -> ( ( ph /\ i e. W ) <-> ( ph /\ ( k + 1 ) e. W ) ) )
80 fveq2 
 |-  ( i = ( k + 1 ) -> ( F ` i ) = ( F ` ( k + 1 ) ) )
81 80 eleq1d 
 |-  ( i = ( k + 1 ) -> ( ( F ` i ) e. CC <-> ( F ` ( k + 1 ) ) e. CC ) )
82 79 81 imbi12d 
 |-  ( i = ( k + 1 ) -> ( ( ( ph /\ i e. W ) -> ( F ` i ) e. CC ) <-> ( ( ph /\ ( k + 1 ) e. W ) -> ( F ` ( k + 1 ) ) e. CC ) ) )
83 eleq1 
 |-  ( k = i -> ( k e. W <-> i e. W ) )
84 83 anbi2d 
 |-  ( k = i -> ( ( ph /\ k e. W ) <-> ( ph /\ i e. W ) ) )
85 fveq2 
 |-  ( k = i -> ( F ` k ) = ( F ` i ) )
86 85 eleq1d 
 |-  ( k = i -> ( ( F ` k ) e. CC <-> ( F ` i ) e. CC ) )
87 84 86 imbi12d 
 |-  ( k = i -> ( ( ( ph /\ k e. W ) -> ( F ` k ) e. CC ) <-> ( ( ph /\ i e. W ) -> ( F ` i ) e. CC ) ) )
88 87 24 chvarvv 
 |-  ( ( ph /\ i e. W ) -> ( F ` i ) e. CC )
89 77 82 88 vtocl 
 |-  ( ( ph /\ ( k + 1 ) e. W ) -> ( F ` ( k + 1 ) ) e. CC )
90 76 89 sylan2 
 |-  ( ( ph /\ k e. W ) -> ( F ` ( k + 1 ) ) e. CC )
91 90 adantr 
 |-  ( ( ( ph /\ k e. W ) /\ ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) ) -> ( F ` ( k + 1 ) ) e. CC )
92 91 abscld 
 |-  ( ( ( ph /\ k e. W ) /\ ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) ) -> ( abs ` ( F ` ( k + 1 ) ) ) e. RR )
93 simpr 
 |-  ( ( ( ph /\ k e. W ) /\ ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) ) -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) )
94 7 adantr 
 |-  ( ( ( ph /\ k e. W ) /\ ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) ) -> ( abs ` ( F ` k ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) )
95 73 75 92 93 94 letrd 
 |-  ( ( ( ph /\ k e. W ) /\ ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) ) -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) )
96 95 ex 
 |-  ( ( ph /\ k e. W ) -> ( ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) ) )
97 20 96 sylan2br 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) ) )
98 97 expcom 
 |-  ( k e. ( ZZ>= ` N ) -> ( ph -> ( ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) ) ) )
99 98 a2d 
 |-  ( k e. ( ZZ>= ` N ) -> ( ( ph -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) ) -> ( ph -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` ( k + 1 ) ) ) ) ) )
100 63 66 69 66 72 99 uzind4 
 |-  ( k e. ( ZZ>= ` N ) -> ( ph -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) ) )
101 100 impcom 
 |-  ( ( ph /\ k e. ( ZZ>= ` N ) ) -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) )
102 20 101 sylan2b 
 |-  ( ( ph /\ k e. W ) -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) )
103 102 adantlr 
 |-  ( ( ( ph /\ F ~~> 0 ) /\ k e. W ) -> ( abs ` ( F ` N ) ) <_ ( abs ` ( F ` k ) ) )
104 103 55 breqtrrd 
 |-  ( ( ( ph /\ F ~~> 0 ) /\ k e. W ) -> ( abs ` ( F ` N ) ) <_ ( ( i e. W |-> ( abs ` ( F ` i ) ) ) ` k ) )
105 2 41 42 58 60 104 climlec2 
 |-  ( ( ph /\ F ~~> 0 ) -> ( abs ` ( F ` N ) ) <_ 0 )
106 40 105 mtand 
 |-  ( ph -> -. F ~~> 0 )
107 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
108 8 107 syl 
 |-  ( ph -> M e. ZZ )
109 108 adantr 
 |-  ( ( ph /\ seq M ( + , F ) e. dom ~~> ) -> M e. ZZ )
110 4 adantr 
 |-  ( ( ph /\ seq M ( + , F ) e. dom ~~> ) -> F e. V )
111 simpr 
 |-  ( ( ph /\ seq M ( + , F ) e. dom ~~> ) -> seq M ( + , F ) e. dom ~~> )
112 5 adantlr 
 |-  ( ( ( ph /\ seq M ( + , F ) e. dom ~~> ) /\ k e. Z ) -> ( F ` k ) e. CC )
113 1 109 110 111 112 serf0 
 |-  ( ( ph /\ seq M ( + , F ) e. dom ~~> ) -> F ~~> 0 )
114 106 113 mtand 
 |-  ( ph -> -. seq M ( + , F ) e. dom ~~> )
115 df-nel 
 |-  ( seq M ( + , F ) e/ dom ~~> <-> -. seq M ( + , F ) e. dom ~~> )
116 114 115 sylibr 
 |-  ( ph -> seq M ( + , F ) e/ dom ~~> )