Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  cvgratz Unicode version

Theorem cvgratz 11252
 Description: Ratio test for convergence of a complex infinite series. If the ratio of the absolute values of successive terms in an infinite sequence is less than 1 for all terms, then the infinite sum of the terms of converges to a complex number. (Contributed by NM, 26-Apr-2005.) (Revised by Jim Kingdon, 11-Nov-2022.)
Hypotheses
Ref Expression
cvgratz.1
cvgratz.m
cvgratz.3
cvgratz.4
cvgratz.gt0
cvgratz.6
cvgratz.7
Assertion
Ref Expression
cvgratz
Distinct variable groups:   ,   ,   ,   ,   ,

Proof of Theorem cvgratz
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvgratz.m . . . . 5
21adantr 272 . . . 4
3 fveq2 5387 . . . . . 6
43eleq1d 2184 . . . . 5
5 cvgratz.6 . . . . . . 7
65ralrimiva 2480 . . . . . 6
76ad2antrr 477 . . . . 5
8 cvgratz.1 . . . . . . . 8
98eleq2i 2182 . . . . . . 7
109biimpri 132 . . . . . 6
1110adantl 273 . . . . 5
124, 7, 11rspcdva 2766 . . . 4
13 eluzelz 9287 . . . . . . . 8
1413adantl 273 . . . . . . 7
15 1red 7745 . . . . . . . 8
161zred 9127 . . . . . . . . 9
1716ad2antrr 477 . . . . . . . 8
1814zred 9127 . . . . . . . 8
19 simplr 502 . . . . . . . 8
20 eluzle 9290 . . . . . . . . 9
2120adantl 273 . . . . . . . 8
2215, 17, 18, 19, 21letrd 7850 . . . . . . 7
23 elnnz1 9031 . . . . . . 7
2414, 22, 23sylanbrc 411 . . . . . 6
25 elnnuz 9314 . . . . . . . 8
26 fveq2 5387 . . . . . . . . . . . . 13
2726eleq1d 2184 . . . . . . . . . . . 12
28 uzid 9292 . . . . . . . . . . . . . 14
291, 28syl 14 . . . . . . . . . . . . 13
3029, 8syl6eleqr 2209 . . . . . . . . . . . 12
3127, 6, 30rspcdva 2766 . . . . . . . . . . 11
3231ad3antrrr 481 . . . . . . . . . 10
33 cvgratz.3 . . . . . . . . . . . . . 14
34 cvgratz.gt0 . . . . . . . . . . . . . 14
3533, 34elrpd 9432 . . . . . . . . . . . . 13
3635ad3antrrr 481 . . . . . . . . . . . 12
372adantr 272 . . . . . . . . . . . . . 14
3837adantr 272 . . . . . . . . . . . . 13
3925biimpri 132 . . . . . . . . . . . . . . . 16
4039adantl 273 . . . . . . . . . . . . . . 15
4140nnzd 9126 . . . . . . . . . . . . . 14
4241adantr 272 . . . . . . . . . . . . 13
4338, 42zsubcld 9132 . . . . . . . . . . . 12
4436, 43rpexpcld 10399 . . . . . . . . . . 11
4544rpcnd 9436 . . . . . . . . . 10
4644rpap0d 9440 . . . . . . . . . 10 #
4732, 45, 46divclapd 8513 . . . . . . . . 9
48 simplll 505 . . . . . . . . . 10
4937adantr 272 . . . . . . . . . . . 12
5041adantr 272 . . . . . . . . . . . 12
5116ad3antrrr 481 . . . . . . . . . . . . 13
5250zred 9127 . . . . . . . . . . . . 13
53 simpr 109 . . . . . . . . . . . . 13
5451, 52, 53nltled 7847 . . . . . . . . . . . 12
55 eluz2 9284 . . . . . . . . . . . 12
5649, 50, 54, 55syl3anbrc 1148 . . . . . . . . . . 11
5756, 8syl6eleqr 2209 . . . . . . . . . 10
5848, 57, 5syl2anc 406 . . . . . . . . 9
59 zdclt 9082 . . . . . . . . . 10 DECID
6041, 37, 59syl2anc 406 . . . . . . . . 9 DECID
6147, 58, 60ifcldadc 3469 . . . . . . . 8
6225, 61sylan2b 283 . . . . . . 7
6324, 62syldan 278 . . . . . 6
64 breq1 3900 . . . . . . . 8
65 oveq2 5748 . . . . . . . . . 10
6665oveq2d 5756 . . . . . . . . 9
6766oveq2d 5756 . . . . . . . 8
68 fveq2 5387 . . . . . . . 8
6964, 67, 68ifbieq12d 3466 . . . . . . 7
70 eqid 2115 . . . . . . 7
7169, 70fvmptg 5463 . . . . . 6
7224, 63, 71syl2anc 406 . . . . 5
7317, 18, 21lensymd 7848 . . . . . 6
7473iffalsed 3452 . . . . 5
7572, 74eqtr2d 2149 . . . 4
76 addcl 7709 . . . . 5
7776adantl 273 . . . 4
782, 12, 75, 77seq3feq 10196 . . 3
7933adantr 272 . . . . 5
80 cvgratz.4 . . . . . 6
8180adantr 272 . . . . 5
8234adantr 272 . . . . 5
8371eleq1d 2184 . . . . . . . 8
8440, 61, 83syl2anc 406 . . . . . . 7
8561, 84mpbird 166 . . . . . 6
8625, 85sylan2b 283 . . . . 5
8731ad3antrrr 481 . . . . . . . . . . 11
8835ad3antrrr 481 . . . . . . . . . . . . 13
892ad2antrr 477 . . . . . . . . . . . . . 14
9025, 41sylan2b 283 . . . . . . . . . . . . . . . 16
9190adantr 272 . . . . . . . . . . . . . . 15
9291peano2zd 9130 . . . . . . . . . . . . . 14
9389, 92zsubcld 9132 . . . . . . . . . . . . 13
9488, 93rpexpcld 10399 . . . . . . . . . . . 12
9594rpcnd 9436 . . . . . . . . . . 11
9694rpap0d 9440 . . . . . . . . . . 11 #
9787, 95, 96divclapd 8513 . . . . . . . . . 10
98 fveq2 5387 . . . . . . . . . . . 12
9998eleq1d 2184 . . . . . . . . . . 11
100 fveq2 5387 . . . . . . . . . . . . . . 15
101100eleq1d 2184 . . . . . . . . . . . . . 14
102101cbvralv 2629 . . . . . . . . . . . . 13
1036, 102sylib 121 . . . . . . . . . . . 12
104103ad3antrrr 481 . . . . . . . . . . 11
1052ad2antrr 477 . . . . . . . . . . . . 13
106 peano2nn 8692 . . . . . . . . . . . . . . . 16
107106adantl 273 . . . . . . . . . . . . . . 15
108107nnzd 9126 . . . . . . . . . . . . . 14
109108adantr 272 . . . . . . . . . . . . 13
11016ad3antrrr 481 . . . . . . . . . . . . . 14
111107nnred 8693 . . . . . . . . . . . . . . 15
112111adantr 272 . . . . . . . . . . . . . 14
113 simpr 109 . . . . . . . . . . . . . 14
114110, 112, 113nltled 7847 . . . . . . . . . . . . 13
115 eluz2 9284 . . . . . . . . . . . . 13
116105, 109, 114, 115syl3anbrc 1148 . . . . . . . . . . . 12
117116, 8syl6eleqr 2209 . . . . . . . . . . 11
11899, 104, 117rspcdva 2766 . . . . . . . . . 10
1192adantr 272 . . . . . . . . . . 11
120 zdclt 9082 . . . . . . . . . . 11 DECID
121108, 119, 120syl2anc 406 . . . . . . . . . 10 DECID
12297, 118, 121ifcldadc 3469 . . . . . . . . 9
123122abscld 10904 . . . . . . . 8
12416recnd 7758 . . . . . . . . . . . . . . . . 17
125124ad2antrr 477 . . . . . . . . . . . . . . . 16
126 simpr 109 . . . . . . . . . . . . . . . . 17
127126nncnd 8694 . . . . . . . . . . . . . . . 16
128 1cnd 7746 . . . . . . . . . . . . . . . 16
129125, 127, 128subsub4d 8068 . . . . . . . . . . . . . . 15
130129oveq2d 5756 . . . . . . . . . . . . . 14
13133recnd 7758 . . . . . . . . . . . . . . . 16
132131ad2antrr 477 . . . . . . . . . . . . . . 15
13333, 34gt0ap0d 8354 . . . . . . . . . . . . . . . 16 #
134133ad2antrr 477 . . . . . . . . . . . . . . 15 #
135119, 90zsubcld 9132 . . . . . . . . . . . . . . 15
136132, 134, 135expm1apd 10385 . . . . . . . . . . . . . 14
137130, 136eqtr3d 2150 . . . . . . . . . . . . 13
138137oveq2d 5756 . . . . . . . . . . . 12
139138adantr 272 . . . . . . . . . . 11
140 simpr 109 . . . . . . . . . . . 12
141140iftrued 3449 . . . . . . . . . . 11
142126nnred 8693 . . . . . . . . . . . . . . . 16
143142adantr 272 . . . . . . . . . . . . . . 15
144 peano2re 7862 . . . . . . . . . . . . . . . 16
145143, 144syl 14 . . . . . . . . . . . . . . 15
14616ad3antrrr 481 . . . . . . . . . . . . . . 15
147143ltp1d 8648 . . . . . . . . . . . . . . 15
148143, 145, 146, 147, 140lttrd 7852 . . . . . . . . . . . . . 14
149148iftrued 3449 . . . . . . . . . . . . 13
150149oveq2d 5756 . . . . . . . . . . . 12
15131ad2antrr 477 . . . . . . . . . . . . . . 15
152132, 134, 135expclzapd 10380 . . . . . . . . . . . . . . 15
153132, 134, 135expap0d 10381 . . . . . . . . . . . . . . 15 #
154151, 152, 132, 153, 134divdivap2d 8546 . . . . . . . . . . . . . 14
155151, 132mulcomd 7751 . . . . . . . . . . . . . . 15
156155oveq1d 5755 . . . . . . . . . . . . . 14
157132, 151, 152, 153divassapd 8549 . . . . . . . . . . . . . 14
158154, 156, 1573eqtrd 2152 . . . . . . . . . . . . 13
159158adantr 272 . . . . . . . . . . . 12
160150, 159eqtr4d 2151 . . . . . . . . . . 11
161139, 141, 1603eqtr4d 2158 . . . . . . . . . 10
162161fveq2d 5391 . . . . . . . . 9
163132, 62absmuld 10917 . . . . . . . . . 10
164163adantr 272 . . . . . . . . 9
16535rpge0d 9438 . . . . . . . . . . . 12
16633, 165absidd 10890 . . . . . . . . . . 11
167166oveq1d 5755 . . . . . . . . . 10
168167ad3antrrr 481 . . . . . . . . 9
169162, 164, 1683eqtrd 2152 . . . . . . . 8
170 eqle 7819 . . . . . . . 8
171123, 169, 170syl2an2r 567 . . . . . . 7
17216ad2antrr 477 . . . . . . . . . . . . . 14
173111, 172lttri3d 7842 . . . . . . . . . . . . 13
174173simprbda 378 . . . . . . . . . . . 12
175174iffalsed 3452 . . . . . . . . . . 11
176 simpr 109 . . . . . . . . . . . 12
177176fveq2d 5391 . . . . . . . . . . 11
178175, 177eqtrd 2148 . . . . . . . . . 10
179178fveq2d 5391 . . . . . . . . 9
180142adantr 272 . . . . . . . . . . . . . . . 16
181180ltp1d 8648 . . . . . . . . . . . . . . 15
182 breq2 3901 . . . . . . . . . . . . . . . 16
183182adantl 273 . . . . . . . . . . . . . . 15
184181, 183mpbid 146 . . . . . . . . . . . . . 14
185184iftrued 3449 . . . . . . . . . . . . 13
186176oveq1d 5755 . . . . . . . . . . . . . . . . 17
187127adantr 272 . . . . . . . . . . . . . . . . . 18
188 1cnd 7746 . . . . . . . . . . . . . . . . . 18
189187, 188pncan2d 8039 . . . . . . . . . . . . . . . . 17
190186, 189eqtr3d 2150 . . . . . . . . . . . . . . . 16
191190oveq2d 5756 . . . . . . . . . . . . . . 15
192132adantr 272 . . . . . . . . . . . . . . . 16
193192exp1d 10370 . . . . . . . . . . . . . . 15
194191, 193eqtrd 2148 . . . . . . . . . . . . . 14
195194oveq2d 5756 . . . . . . . . . . . . 13
196185, 195eqtrd 2148 . . . . . . . . . . . 12
197196oveq2d 5756 . . . . . . . . . . 11
19831, 131, 133divcanap2d 8515 . . . . . . . . . . . 12
199198ad3antrrr 481 . . . . . . . . . . 11
200197, 199eqtrd 2148 . . . . . . . . . 10
201200fveq2d 5391 . . . . . . . . 9
202167ad2antrr 477 . . . . . . . . . . 11
203163, 202eqtrd 2148 . . . . . . . . . 10
204203adantr 272 . . . . . . . . 9
205179, 201, 2043eqtr2d 2154 . . . . . . . 8
206123, 205, 170syl2an2r 567 . . . . . . 7
207 simplll 505 . . . . . . . . 9
208119adantr 272 . . . . . . . . . . 11
20990adantr 272 . . . . . . . . . . 11
210 simpr 109 . . . . . . . . . . . 12
211 zleltp1 9063 . . . . . . . . . . . . 13
212119, 209, 211syl2an2r 567 . . . . . . . . . . . 12
213210, 212mpbird 166 . . . . . . . . . . 11
214208, 209, 213, 55syl3anbrc 1148 . . . . . . . . . 10
215214, 8syl6eleqr 2209 . . . . . . . . 9
216 cvgratz.7 . . . . . . . . 9
217207, 215, 216syl2anc 406 . . . . . . . 8
218172adantr 272 . . . . . . . . . . 11
219111adantr 272 . . . . . . . . . . 11
220218, 219, 210ltnsymd 7846 . . . . . . . . . 10
221220iffalsed 3452 . . . . . . . . 9
222221fveq2d 5391 . . . . . . . 8
223142adantr 272 . . . . . . . . . . . 12
224218, 223, 213lensymd 7848 . . . . . . . . . . 11
225224iffalsed 3452 . . . . . . . . . 10
226225fveq2d 5391 . . . . . . . . 9
227226oveq2d 5756 . . . . . . . 8
228217, 222, 2273brtr4d 3928 . . . . . . 7
229 ztri3or 9051 . . . . . . . 8
230108, 119, 229syl2anc 406 . . . . . . 7
231171, 206, 228, 230mpjao3dan 1268 . . . . . 6
232 breq1 3900 . . . . . . . . . 10
233 oveq2 5748 . . . . . . . . . . . 12
234233oveq2d 5756 . . . . . . . . . . 11
235234oveq2d 5756 . . . . . . . . . 10
236 fveq2 5387 . . . . . . . . . 10
237232, 235, 236ifbieq12d 3466 . . . . . . . . 9
238237, 70fvmptg 5463 . . . . . . . 8
239107, 122, 238syl2anc 406 . . . . . . 7
240239fveq2d 5391 . . . . . 6
241126, 62, 71syl2anc 406 . . . . . . . 8
242241fveq2d 5391 . . . . . . 7
243242oveq2d 5756 . . . . . 6
244231, 240, 2433brtr4d 3928 . . . . 5
24579, 81, 82, 86, 244cvgratnn 11251 . . . 4
246 eqid 2115 . . . . 5
247 1zzd 9035 . . . . . 6
248 simpr 109 . . . . . 6
249 eluz2 9284 . . . . . 6
250247, 2, 248, 249syl3anbrc 1148 . . . . 5
251246, 250, 85iserex 11059 . . . 4
252245, 251mpbid 146 . . 3
25378, 252eqeltrd 2192 . 2
25433adantr 272 . . . 4
25580adantr 272 . . . 4
25634adantr 272 . . . 4
2571adantr 272 . . . . . . 7
258257adantr 272 . . . . . 6
259 nnz 9027 . . . . . . 7
260259adantl 273 . . . . . 6
261258zred 9127 . . . . . . 7
262 1red 7745 . . . . . . 7
263260zred 9127 . . . . . . 7
264 simplr 502 . . . . . . 7
265 nnge1 8703 . . . . . . . 8
266265adantl 273 . . . . . . 7
267261, 262, 263, 264, 266letrd 7850 . . . . . 6
268258, 260, 267, 55syl3anbrc 1148 . . . . 5
2698eleq2i 2182 . . . . . . 7
270269, 5sylan2br 284 . . . . . 6
271270adantlr 466 . . . . 5
272268, 271syldan 278 . . . 4
273269, 216sylan2br 284 . . . . . 6
274273adantlr 466 . . . . 5
275268, 274syldan 278 . . . 4
276254, 255, 256, 272, 275cvgratnn 11251 . . 3
277 eqid 2115 . . . 4
278 1zzd 9035 . . . . 5
279 simpr 109 . . . . 5
280 eluz2 9284 . . . . 5
281257, 278, 279, 280syl3anbrc 1148 . . . 4
282277, 281, 271iserex 11059 . . 3
283276, 282mpbird 166 . 2
284 1z 9034 . . 3
285 zletric 9052 . . 3
286284, 1, 285sylancr 408 . 2
287253, 283, 286mpjaodan 770 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103   wb 104   wo 680  DECID wdc 802   w3o 944   wceq 1314   wcel 1463  wral 2391  cif 3442   class class class wbr 3897   cmpt 3957   cdm 4507  cfv 5091  (class class class)co 5740  cc 7582  cr 7583  cc0 7584  c1 7585   caddc 7587   cmul 7589   clt 7764   cle 7765   cmin 7897   # cap 8306   cdiv 8395  cn 8680  cz 9008  cuz 9278  crp 9393   cseq 10169  cexp 10243  cabs 10720   cli 10998 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 586  ax-in2 587  ax-io 681  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-10 1466  ax-11 1467  ax-i12 1468  ax-bndl 1469  ax-4 1470  ax-13 1474  ax-14 1475  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097  ax-coll 4011  ax-sep 4014  ax-nul 4022  ax-pow 4066  ax-pr 4099  ax-un 4323  ax-setind 4420  ax-iinf 4470  ax-cnex 7675  ax-resscn 7676  ax-1cn 7677  ax-1re 7678  ax-icn 7679  ax-addcl 7680  ax-addrcl 7681  ax-mulcl 7682  ax-mulrcl 7683  ax-addcom 7684  ax-mulcom 7685  ax-addass 7686  ax-mulass 7687  ax-distr 7688  ax-i2m1 7689  ax-0lt1 7690  ax-1rid 7691  ax-0id 7692  ax-rnegex 7693  ax-precex 7694  ax-cnre 7695  ax-pre-ltirr 7696  ax-pre-ltwlin 7697  ax-pre-lttrn 7698  ax-pre-apti 7699  ax-pre-ltadd 7700  ax-pre-mulgt0 7701  ax-pre-mulext 7702  ax-arch 7703  ax-caucvg 7704 This theorem depends on definitions:  df-bi 116  df-dc 803  df-3or 946  df-3an 947  df-tru 1317  df-fal 1320  df-nf 1420  df-sb 1719  df-eu 1978  df-mo 1979  df-clab 2102  df-cleq 2108  df-clel 2111  df-nfc 2245  df-ne 2284  df-nel 2379  df-ral 2396  df-rex 2397  df-reu 2398  df-rmo 2399  df-rab 2400  df-v 2660  df-sbc 2881  df-csb 2974  df-dif 3041  df-un 3043  df-in 3045  df-ss 3052  df-nul 3332  df-if 3443  df-pw 3480  df-sn 3501  df-pr 3502  df-op 3504  df-uni 3705  df-int 3740  df-iun 3783  df-br 3898  df-opab 3958  df-mpt 3959  df-tr 3995  df-id 4183  df-po 4186  df-iso 4187  df-iord 4256  df-on 4258  df-ilim 4259  df-suc 4261  df-iom 4473  df-xp 4513  df-rel 4514  df-cnv 4515  df-co 4516  df-dm 4517  df-rn 4518  df-res 4519  df-ima 4520  df-iota 5056  df-fun 5093  df-fn 5094  df-f 5095  df-f1 5096  df-fo 5097  df-f1o 5098  df-fv 5099  df-isom 5100  df-riota 5696  df-ov 5743  df-oprab 5744  df-mpo 5745  df-1st 6004  df-2nd 6005  df-recs 6168  df-irdg 6233  df-frec 6254  df-1o 6279  df-oadd 6283  df-er 6395  df-en 6601  df-dom 6602  df-fin 6603  df-pnf 7766  df-mnf 7767  df-xr 7768  df-ltxr 7769  df-le 7770  df-sub 7899  df-neg 7900  df-reap 8300  df-ap 8307  df-div 8396  df-inn 8681  df-2 8739  df-3 8740  df-4 8741  df-n0 8932  df-z 9009  df-uz 9279  df-q 9364  df-rp 9394  df-ico 9628  df-fz 9742  df-fzo 9871  df-seqfrec 10170  df-exp 10244  df-ihash 10473  df-cj 10565  df-re 10566  df-im 10567  df-rsqrt 10721  df-abs 10722  df-clim 10999  df-sumdc 11074 This theorem is referenced by:  cvgratgt0  11253
 Copyright terms: Public domain W3C validator