Mathbox for Jim Kingdon < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  cvgcmp2nlemabs Unicode version

Theorem cvgcmp2nlemabs 13400
 Description: Lemma for cvgcmp2n 13401. The partial sums get closer to each other as we go further out. The proof proceeds by rewriting as the sum of and a term which gets smaller as gets large. (Contributed by Jim Kingdon, 25-Aug-2023.)
Hypotheses
Ref Expression
cvgcmp2n.cl
cvgcmp2n.ge0
cvgcmp2n.lt
cvgcmp2nlemabs.m
cvgcmp2nlemabs.n
Assertion
Ref Expression
cvgcmp2nlemabs
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem cvgcmp2nlemabs
StepHypRef Expression
1 eqidd 2141 . . . . . . . 8
2 cvgcmp2nlemabs.m . . . . . . . . . 10
3 cvgcmp2nlemabs.n . . . . . . . . . 10
4 eluznn 9420 . . . . . . . . . 10
52, 3, 4syl2anc 409 . . . . . . . . 9
6 elnnuz 9385 . . . . . . . . 9
75, 6sylib 121 . . . . . . . 8
8 elnnuz 9385 . . . . . . . . 9
9 cvgcmp2n.cl . . . . . . . . . 10
109recnd 7817 . . . . . . . . 9
118, 10sylan2br 286 . . . . . . . 8
121, 7, 11fsum3ser 11197 . . . . . . 7
13 nnuz 9384 . . . . . . . . 9
142, 13eleqtrdi 2233 . . . . . . . 8
151, 14, 11fsum3ser 11197 . . . . . . 7
1612, 15oveq12d 5799 . . . . . 6
172nnred 8756 . . . . . . . . . . 11
1817ltp1d 8711 . . . . . . . . . 10
19 fzdisj 9862 . . . . . . . . . 10
2018, 19syl 14 . . . . . . . . 9
21 eluzle 9361 . . . . . . . . . . . 12
223, 21syl 14 . . . . . . . . . . 11
23 elfz1b 9900 . . . . . . . . . . 11
242, 5, 22, 23syl3anbrc 1166 . . . . . . . . . 10
25 fzsplit 9861 . . . . . . . . . 10
2624, 25syl 14 . . . . . . . . 9
27 1zzd 9104 . . . . . . . . . 10
285nnzd 9195 . . . . . . . . . 10
2927, 28fzfigd 10234 . . . . . . . . 9
30 elfznn 9864 . . . . . . . . . 10
3130, 10sylan2 284 . . . . . . . . 9
3220, 26, 29, 31fsumsplit 11207 . . . . . . . 8
3332eqcomd 2146 . . . . . . 7
3429, 31fsumcl 11200 . . . . . . . 8
352nnzd 9195 . . . . . . . . . 10
3627, 35fzfigd 10234 . . . . . . . . 9
37 elfznn 9864 . . . . . . . . . 10
3837, 10sylan2 284 . . . . . . . . 9
3936, 38fsumcl 11200 . . . . . . . 8
4035peano2zd 9199 . . . . . . . . . 10
4140, 28fzfigd 10234 . . . . . . . . 9
422peano2nnd 8758 . . . . . . . . . . 11
43 elfzuz 9832 . . . . . . . . . . 11
44 eluznn 9420 . . . . . . . . . . 11
4542, 43, 44syl2an 287 . . . . . . . . . 10
4645, 10syldan 280 . . . . . . . . 9
4741, 46fsumcl 11200 . . . . . . . 8
4834, 39, 47subaddd 8114 . . . . . . 7
4933, 48mpbird 166 . . . . . 6
5016, 49eqtr3d 2175 . . . . 5
5145, 9syldan 280 . . . . . 6
5241, 51fsumrecl 11201 . . . . 5
5350, 52eqeltrd 2217 . . . 4
5442nnzd 9195 . . . . . . 7
5554, 28fzfigd 10234 . . . . . 6
56 cvgcmp2n.ge0 . . . . . . 7
5745, 56syldan 280 . . . . . 6
5855, 51, 57fsumge0 11259 . . . . 5
5958, 50breqtrrd 3963 . . . 4
6053, 59absidd 10970 . . 3
6160, 50eqtrd 2173 . 2
62 halfre 8956 . . . . . . 7
6362a1i 9 . . . . . 6
6442nnnn0d 9053 . . . . . 6
6563, 64reexpcld 10471 . . . . 5
665peano2nnd 8758 . . . . . . 7
6766nnnn0d 9053 . . . . . 6
6863, 67reexpcld 10471 . . . . 5
6965, 68resubcld 8166 . . . 4
70 1mhlfehlf 8961 . . . . . 6
71 2rp 9474 . . . . . . 7
72 rpreccl 9496 . . . . . . 7
7371, 72ax-mp 5 . . . . . 6
7470, 73eqeltri 2213 . . . . 5
7574a1i 9 . . . 4
7669, 75rerpdivcld 9544 . . 3
7771a1i 9 . . . . 5
782nnrpd 9510 . . . . 5
7977, 78rpdivcld 9530 . . . 4
8079rpred 9512 . . 3
8171a1i 9 . . . . . . . . 9
8245nnzd 9195 . . . . . . . . 9
8381, 82rpexpcld 10478 . . . . . . . 8
8483rprecred 9524 . . . . . . 7
85 cvgcmp2n.lt . . . . . . . 8
8645, 85syldan 280 . . . . . . 7
8741, 51, 84, 86fsumle 11263 . . . . . 6
88 2cnd 8816 . . . . . . . . 9
8981rpap0d 9518 . . . . . . . . 9 #
9088, 89, 82exprecapd 10462 . . . . . . . 8
9190eqcomd 2146 . . . . . . 7
9291sumeq2dv 11168 . . . . . 6
9387, 92breqtrd 3961 . . . . 5
94 fzval3 10011 . . . . . . 7 ..^
9528, 94syl 14 . . . . . 6 ..^
9695sumeq1d 11166 . . . . 5 ..^
9793, 96breqtrd 3961 . . . 4 ..^
98 halfcn 8957 . . . . . 6
9998a1i 9 . . . . 5
100 1re 7788 . . . . . . 7
101 halflt1 8960 . . . . . . 7
10262, 100, 101ltapii 8420 . . . . . 6 #
103102a1i 9 . . . . 5 #
104 eluzp1p1 9374 . . . . . 6
1053, 104syl 14 . . . . 5
10699, 103, 64, 105geosergap 11306 . . . 4 ..^
10797, 106breqtrd 3961 . . 3
10873a1i 9 . . . . . . . 8
10928peano2zd 9199 . . . . . . . 8
110108, 109rpexpcld 10478 . . . . . . 7
111110rpred 9512 . . . . . 6
11265, 111resubcld 8166 . . . . 5
1132nnrecred 8790 . . . . 5
11465, 110ltsubrpd 9545 . . . . . 6
115 2cnd 8816 . . . . . . . 8
11677rpap0d 9518 . . . . . . . 8 #
117115, 116, 40exprecapd 10462 . . . . . . 7
11842nnred 8756 . . . . . . . . 9
11977, 40rpexpcld 10478 . . . . . . . . . 10
120119rpred 9512 . . . . . . . . 9
121 2z 9105 . . . . . . . . . . . 12
122 uzid 9363 . . . . . . . . . . . 12
123121, 122ax-mp 5 . . . . . . . . . . 11
124123a1i 9 . . . . . . . . . 10
125 bernneq3 10444 . . . . . . . . . 10
126124, 64, 125syl2anc 409 . . . . . . . . 9
12717, 118, 120, 18, 126lttrd 7911 . . . . . . . 8
12878, 119ltrecd 9531 . . . . . . . 8
129127, 128mpbid 146 . . . . . . 7
130117, 129eqbrtrd 3957 . . . . . 6
131112, 65, 113, 114, 130lttrd 7911 . . . . 5
132112, 113, 77, 131ltmul1dd 9568 . . . 4
13370oveq2i 5792 . . . . . 6
134112recnd 7817 . . . . . . 7
135 1cnd 7805 . . . . . . 7
136 1ap0 8375 . . . . . . . 8 #
137136a1i 9 . . . . . . 7 #
138134, 135, 115, 137, 116divdivap2d 8606 . . . . . 6
139133, 138syl5eq 2185 . . . . 5
140134, 115mulcld 7809 . . . . . 6
141140div1d 8563 . . . . 5
142139, 141eqtrd 2173 . . . 4
14317recnd 7817 . . . . 5
1442nnap0d 8789 . . . . 5 #
145115, 143, 144divrecap2d 8577 . . . 4
146132, 142, 1453brtr4d 3967 . . 3
14752, 76, 80, 107, 146lelttrd 7910 . 2
14861, 147eqbrtrd 3957 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wceq 1332   wcel 1481   cun 3073   cin 3074  c0 3367   class class class wbr 3936  cfv 5130  (class class class)co 5781  cc 7641  cr 7642  cc0 7643  c1 7644   caddc 7646   cmul 7648   clt 7823   cle 7824   cmin 7956   # cap 8366   cdiv 8455  cn 8743  c2 8794  cn0 9000  cz 9077  cuz 9349  crp 9469  cfz 9820  ..^cfzo 9949   cseq 10248  cexp 10322  cabs 10800  csu 11153 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 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4050  ax-sep 4053  ax-nul 4061  ax-pow 4105  ax-pr 4138  ax-un 4362  ax-setind 4459  ax-iinf 4509  ax-cnex 7734  ax-resscn 7735  ax-1cn 7736  ax-1re 7737  ax-icn 7738  ax-addcl 7739  ax-addrcl 7740  ax-mulcl 7741  ax-mulrcl 7742  ax-addcom 7743  ax-mulcom 7744  ax-addass 7745  ax-mulass 7746  ax-distr 7747  ax-i2m1 7748  ax-0lt1 7749  ax-1rid 7750  ax-0id 7751  ax-rnegex 7752  ax-precex 7753  ax-cnre 7754  ax-pre-ltirr 7755  ax-pre-ltwlin 7756  ax-pre-lttrn 7757  ax-pre-apti 7758  ax-pre-ltadd 7759  ax-pre-mulgt0 7760  ax-pre-mulext 7761  ax-arch 7762  ax-caucvg 7763 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rmo 2425  df-rab 2426  df-v 2691  df-sbc 2913  df-csb 3007  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-nul 3368  df-if 3479  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-int 3779  df-iun 3822  df-br 3937  df-opab 3997  df-mpt 3998  df-tr 4034  df-id 4222  df-po 4225  df-iso 4226  df-iord 4295  df-on 4297  df-ilim 4298  df-suc 4300  df-iom 4512  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-rn 4557  df-res 4558  df-ima 4559  df-iota 5095  df-fun 5132  df-fn 5133  df-f 5134  df-f1 5135  df-fo 5136  df-f1o 5137  df-fv 5138  df-isom 5139  df-riota 5737  df-ov 5784  df-oprab 5785  df-mpo 5786  df-1st 6045  df-2nd 6046  df-recs 6209  df-irdg 6274  df-frec 6295  df-1o 6320  df-oadd 6324  df-er 6436  df-en 6642  df-dom 6643  df-fin 6644  df-pnf 7825  df-mnf 7826  df-xr 7827  df-ltxr 7828  df-le 7829  df-sub 7958  df-neg 7959  df-reap 8360  df-ap 8367  df-div 8456  df-inn 8744  df-2 8802  df-3 8803  df-4 8804  df-n0 9001  df-z 9078  df-uz 9350  df-q 9438  df-rp 9470  df-ico 9706  df-fz 9821  df-fzo 9950  df-seqfrec 10249  df-exp 10323  df-ihash 10553  df-cj 10645  df-re 10646  df-im 10647  df-rsqrt 10801  df-abs 10802  df-clim 11079  df-sumdc 11154 This theorem is referenced by:  cvgcmp2n  13401
 Copyright terms: Public domain W3C validator