Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  iseraltlem2 Unicode version

Theorem iseraltlem2 12155
 Description: Lemma for iseralt 12157. The terms of an alternating series form a chain of inequalities in alternate terms, so that for example and (assuming so that these terms are defined). (Contributed by Mario Carneiro, 6-Apr-2015.)
Hypotheses
Ref Expression
iseralt.1
iseralt.2
iseralt.3
iseralt.4
iseralt.5
iseralt.6
Assertion
Ref Expression
iseraltlem2
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,

Proof of Theorem iseraltlem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 5866 . . . . . . . . . 10
2 2cn 9816 . . . . . . . . . . 11
32mul01i 9002 . . . . . . . . . 10
41, 3syl6eq 2331 . . . . . . . . 9
54oveq2d 5874 . . . . . . . 8
65fveq2d 5529 . . . . . . 7
76oveq2d 5874 . . . . . 6
87breq1d 4033 . . . . 5
98imbi2d 307 . . . 4
10 oveq2 5866 . . . . . . . . 9
1110oveq2d 5874 . . . . . . . 8
1211fveq2d 5529 . . . . . . 7
1312oveq2d 5874 . . . . . 6
1413breq1d 4033 . . . . 5
1514imbi2d 307 . . . 4
16 oveq2 5866 . . . . . . . . 9
1716oveq2d 5874 . . . . . . . 8
1817fveq2d 5529 . . . . . . 7
1918oveq2d 5874 . . . . . 6
2019breq1d 4033 . . . . 5
2120imbi2d 307 . . . 4
22 oveq2 5866 . . . . . . . . 9
2322oveq2d 5874 . . . . . . . 8
2423fveq2d 5529 . . . . . . 7
2524oveq2d 5874 . . . . . 6
2625breq1d 4033 . . . . 5
2726imbi2d 307 . . . 4
28 iseralt.1 . . . . . . . . . . . 12
29 uzssz 10247 . . . . . . . . . . . 12
3028, 29eqsstri 3208 . . . . . . . . . . 11
3130a1i 10 . . . . . . . . . 10
3231sselda 3180 . . . . . . . . 9
3332zcnd 10118 . . . . . . . 8
3433addid1d 9012 . . . . . . 7
3534fveq2d 5529 . . . . . 6
3635oveq2d 5874 . . . . 5
37 1re 8837 . . . . . . . . . 10
3837renegcli 9108 . . . . . . . . 9
39 ax-1cn 8795 . . . . . . . . . 10
40 ax-1ne0 8806 . . . . . . . . . 10
4139, 40negne0i 9121 . . . . . . . . 9
42 reexpclz 11123 . . . . . . . . 9
4338, 41, 42mp3an12 1267 . . . . . . . 8
4432, 43syl 15 . . . . . . 7
45 iseralt.2 . . . . . . . . 9
46 iseralt.6 . . . . . . . . . 10
4731sselda 3180 . . . . . . . . . . . 12
48 reexpclz 11123 . . . . . . . . . . . . 13
4938, 41, 48mp3an12 1267 . . . . . . . . . . . 12
5047, 49syl 15 . . . . . . . . . . 11
51 iseralt.3 . . . . . . . . . . . 12
52 ffvelrn 5663 . . . . . . . . . . . 12
5351, 52sylan 457 . . . . . . . . . . 11
5450, 53remulcld 8863 . . . . . . . . . 10
5546, 54eqeltrd 2357 . . . . . . . . 9
5628, 45, 55serfre 11075 . . . . . . . 8
57 ffvelrn 5663 . . . . . . . 8
5856, 57sylan 457 . . . . . . 7
5944, 58remulcld 8863 . . . . . 6
6059leidd 9339 . . . . 5
6136, 60eqbrtrd 4043 . . . 4
6251ad2antrr 706 . . . . . . . . . . 11
63392timesi 9845 . . . . . . . . . . . . . . 15
6463oveq2i 5869 . . . . . . . . . . . . . 14
65 simpr 447 . . . . . . . . . . . . . . . . . . 19
6665, 28syl6eleq 2373 . . . . . . . . . . . . . . . . . 18
6766adantr 451 . . . . . . . . . . . . . . . . 17
68 eluzelz 10238 . . . . . . . . . . . . . . . . 17
6967, 68syl 15 . . . . . . . . . . . . . . . 16
7069zcnd 10118 . . . . . . . . . . . . . . 15
71 nn0cn 9975 . . . . . . . . . . . . . . . . 17
7271adantl 452 . . . . . . . . . . . . . . . 16
73 mulcl 8821 . . . . . . . . . . . . . . . 16
742, 72, 73sylancr 644 . . . . . . . . . . . . . . 15
752, 39mulcli 8842 . . . . . . . . . . . . . . . 16
7675a1i 10 . . . . . . . . . . . . . . 15
7770, 74, 76addassd 8857 . . . . . . . . . . . . . 14
7864, 77syl5eqr 2329 . . . . . . . . . . . . 13
79 2nn0 9982 . . . . . . . . . . . . . . . . . 18
80 simpr 447 . . . . . . . . . . . . . . . . . 18
81 nn0mulcl 10000 . . . . . . . . . . . . . . . . . 18
8279, 80, 81sylancr 644 . . . . . . . . . . . . . . . . 17
83 uzaddcl 10275 . . . . . . . . . . . . . . . . 17
8467, 82, 83syl2anc 642 . . . . . . . . . . . . . . . 16
8529, 84sseldi 3178 . . . . . . . . . . . . . . 15
8685zcnd 10118 . . . . . . . . . . . . . 14
8739a1i 10 . . . . . . . . . . . . . 14
8886, 87, 87addassd 8857 . . . . . . . . . . . . 13
892a1i 10 . . . . . . . . . . . . . . 15
9089, 72, 87adddid 8859 . . . . . . . . . . . . . 14
9190oveq2d 5874 . . . . . . . . . . . . 13
9278, 88, 913eqtr4d 2325 . . . . . . . . . . . 12
93 peano2nn0 10004 . . . . . . . . . . . . . . . 16
9493adantl 452 . . . . . . . . . . . . . . 15
95 nn0mulcl 10000 . . . . . . . . . . . . . . 15
9679, 94, 95sylancr 644 . . . . . . . . . . . . . 14
97 uzaddcl 10275 . . . . . . . . . . . . . 14
9867, 96, 97syl2anc 642 . . . . . . . . . . . . 13
9998, 28syl6eleqr 2374 . . . . . . . . . . . 12
10092, 99eqeltrd 2357 . . . . . . . . . . 11
101 ffvelrn 5663 . . . . . . . . . . 11
10262, 100, 101syl2anc 642 . . . . . . . . . 10
103 peano2uz 10272 . . . . . . . . . . . . 13
10484, 103syl 15 . . . . . . . . . . . 12
105104, 28syl6eleqr 2374 . . . . . . . . . . 11
106 ffvelrn 5663 . . . . . . . . . . 11
10762, 105, 106syl2anc 642 . . . . . . . . . 10
108102, 107resubcld 9211 . . . . . . . . 9
109 0re 8838 . . . . . . . . . 10
110109a1i 10 . . . . . . . . 9
11144adantr 451 . . . . . . . . . 10
11256ad2antrr 706 . . . . . . . . . . 11
11384, 28syl6eleqr 2374 . . . . . . . . . . 11
114 ffvelrn 5663 . . . . . . . . . . 11
115112, 113, 114syl2anc 642 . . . . . . . . . 10
116111, 115remulcld 8863 . . . . . . . . 9
117 iseralt.4 . . . . . . . . . . . . 13
118117ralrimiva 2626 . . . . . . . . . . . 12
119118ad2antrr 706 . . . . . . . . . . 11
120 oveq1 5865 . . . . . . . . . . . . . 14
121120fveq2d 5529 . . . . . . . . . . . . 13
122 fveq2 5525 . . . . . . . . . . . . 13
123121, 122breq12d 4036 . . . . . . . . . . . 12
124123rspcv 2880 . . . . . . . . . . 11
125105, 119, 124sylc 56 . . . . . . . . . 10
126102, 107suble0d 9363 . . . . . . . . . 10
127125, 126mpbird 223 . . . . . . . . 9
128108, 110, 116, 127leadd2dd 9387 . . . . . . . 8
129 seqp1 11061 . . . . . . . . . . . . 13
130104, 129syl 15 . . . . . . . . . . . 12
131 seqp1 11061 . . . . . . . . . . . . . 14
13284, 131syl 15 . . . . . . . . . . . . 13
133132oveq1d 5873 . . . . . . . . . . . 12
134130, 133eqtrd 2315 . . . . . . . . . . 11
13592fveq2d 5529 . . . . . . . . . . 11
136115recnd 8861 . . . . . . . . . . . 12
13746ralrimiva 2626 . . . . . . . . . . . . . . . . 17
138137ad2antrr 706 . . . . . . . . . . . . . . . 16
139 fveq2 5525 . . . . . . . . . . . . . . . . . 18
140 oveq2 5866 . . . . . . . . . . . . . . . . . . 19
141140, 122oveq12d 5876 . . . . . . . . . . . . . . . . . 18
142139, 141eqeq12d 2297 . . . . . . . . . . . . . . . . 17
143142rspcv 2880 . . . . . . . . . . . . . . . 16
144105, 138, 143sylc 56 . . . . . . . . . . . . . . 15
145 neg1cn 9813 . . . . . . . . . . . . . . . . . . 19
146145a1i 10 . . . . . . . . . . . . . . . . . 18
14741a1i 10 . . . . . . . . . . . . . . . . . 18
148146, 147, 85expp1zd 11254 . . . . . . . . . . . . . . . . 17
14938a1i 10 . . . . . . . . . . . . . . . . . . . 20
150149, 147, 85reexpclzd 11270 . . . . . . . . . . . . . . . . . . 19
151150recnd 8861 . . . . . . . . . . . . . . . . . 18
152 mulcom 8823 . . . . . . . . . . . . . . . . . 18
153151, 145, 152sylancl 643 . . . . . . . . . . . . . . . . 17
154151mulm1d 9231 . . . . . . . . . . . . . . . . 17
155148, 153, 1543eqtrd 2319 . . . . . . . . . . . . . . . 16
156155oveq1d 5873 . . . . . . . . . . . . . . 15
157107recnd 8861 . . . . . . . . . . . . . . . 16
158 mulneg12 9218 . . . . . . . . . . . . . . . 16
159151, 157, 158syl2anc 642 . . . . . . . . . . . . . . 15
160144, 156, 1593eqtrd 2319 . . . . . . . . . . . . . 14
161107renegcld 9210 . . . . . . . . . . . . . . 15
162150, 161remulcld 8863 . . . . . . . . . . . . . 14
163160, 162eqeltrd 2357 . . . . . . . . . . . . 13
164163recnd 8861 . . . . . . . . . . . 12
165 fveq2 5525 . . . . . . . . . . . . . . . . . 18
166 oveq2 5866 . . . . . . . . . . . . . . . . . . 19
167 fveq2 5525 . . . . . . . . . . . . . . . . . . 19
168166, 167oveq12d 5876 . . . . . . . . . . . . . . . . . 18
169165, 168eqeq12d 2297 . . . . . . . . . . . . . . . . 17
170169rspcv 2880 . . . . . . . . . . . . . . . 16
171100, 138, 170sylc 56 . . . . . . . . . . . . . . 15
17285peano2zd 10120 . . . . . . . . . . . . . . . . . 18
173146, 147, 172expp1zd 11254 . . . . . . . . . . . . . . . . 17
174155oveq1d 5873 . . . . . . . . . . . . . . . . 17
175 mul2neg 9219 . . . . . . . . . . . . . . . . . . 19
176151, 39, 175sylancl 643 . . . . . . . . . . . . . . . . . 18
177151mulid1d 8852 . . . . . . . . . . . . . . . . . 18
178176, 177eqtrd 2315 . . . . . . . . . . . . . . . . 17
179173, 174, 1783eqtrd 2319 . . . . . . . . . . . . . . . 16
180179oveq1d 5873 . . . . . . . . . . . . . . 15
181171, 180eqtrd 2315 . . . . . . . . . . . . . 14
182150, 102remulcld 8863 . . . . . . . . . . . . . 14
183181, 182eqeltrd 2357 . . . . . . . . . . . . 13
184183recnd 8861 . . . . . . . . . . . 12
185136, 164, 184addassd 8857 . . . . . . . . . . 11
186134, 135, 1853eqtr3d 2323 . . . . . . . . . 10
187186oveq2d 5874 . . . . . . . . 9
188111recnd 8861 . . . . . . . . . 10
189163, 183readdcld 8862 . . . . . . . . . . 11
190189recnd 8861 . . . . . . . . . 10
191188, 136, 190adddid 8859 . . . . . . . . 9
192188, 164, 184adddid 8859 . . . . . . . . . . 11
193160oveq2d 5874 . . . . . . . . . . . . . 14
194161recnd 8861 . . . . . . . . . . . . . . 15
195188, 151, 194mulassd 8858 . . . . . . . . . . . . . 14
196193, 195eqtr4d 2318 . . . . . . . . . . . . 13
19789, 70, 72adddid 8859 . . . . . . . . . . . . . . . . 17
198702timesd 9954 . . . . . . . . . . . . . . . . . 18
199198oveq1d 5873 . . . . . . . . . . . . . . . . 17
20070, 70, 74addassd 8857 . . . . . . . . . . . . . . . . 17
201197, 199, 2003eqtrrd 2320 . . . . . . . . . . . . . . . 16
202201oveq2d 5874 . . . . . . . . . . . . . . 15
203 expaddz 11146 . . . . . . . . . . . . . . . 16
204146, 147, 69, 85, 203syl22anc 1183 . . . . . . . . . . . . . . 15
205 2z 10054 . . . . . . . . . . . . . . . . . 18
206205a1i 10 . . . . . . . . . . . . . . . . 17
207 nn0z 10046 . . . . . . . . . . . . . . . . . 18
208 zaddcl 10059 . . . . . . . . . . . . . . . . . 18
20932, 207, 208syl2an 463 . . . . . . . . . . . . . . . . 17
210 expmulz 11148 . . . . . . . . . . . . . . . . 17
211146, 147, 206, 209, 210syl22anc 1183 . . . . . . . . . . . . . . . 16
212 sqneg 11164 . . . . . . . . . . . . . . . . . . . 20
21339, 212ax-mp 8 . . . . . . . . . . . . . . . . . . 19
214 sq1 11198 . . . . . . . . . . . . . . . . . . 19
215213, 214eqtri 2303 . . . . . . . . . . . . . . . . . 18
216215oveq1i 5868 . . . . . . . . . . . . . . . . 17
217 1exp 11131 . . . . . . . . . . . . . . . . . 18
218209, 217syl 15 . . . . . . . . . . . . . . . . 17
219216, 218syl5eq 2327 . . . . . . . . . . . . . . . 16
220211, 219eqtrd 2315 . . . . . . . . . . . . . . 15
221202, 204, 2203eqtr3d 2323 . . . . . . . . . . . . . 14
222221oveq1d 5873 . . . . . . . . . . . . 13
223194mulid2d 8853 . . . . . . . . . . . . 13
224196, 222, 2233eqtrd 2319 . . . . . . . . . . . 12
225181oveq2d 5874 . . . . . . . . . . . . . 14
226102recnd 8861 . . . . . . . . . . . . . . 15
227188, 151, 226mulassd 8858 . . . . . . . . . . . . . 14
228225, 227eqtr4d 2318 . . . . . . . . . . . . 13
229221oveq1d 5873 . . . . . . . . . . . . 13
230226mulid2d 8853 . . . . . . . . . . . . 13
231228, 229, 2303eqtrd 2319 . . . . . . . . . . . 12
232224, 231oveq12d 5876 . . . . . . . . . . 11
233157negcld 9144 . . . . . . . . . . . . 13
234233, 226addcomd 9014 . . . . . . . . . . . 12
235226, 157negsubd 9163 . . . . . . . . . . . 12
236234, 235eqtrd 2315 . . . . . . . . . . 11
237192, 232, 2363eqtrd 2319 . . . . . . . . . 10
238237oveq2d 5874 . . . . . . . . 9
239187, 191, 2383eqtrrd 2320 . . . . . . . 8
240116recnd 8861 . . . . . . . . 9
241240addid1d 9012 . . . . . . . 8
242128, 239, 2413brtr3d 4052 . . . . . . 7
243 ffvelrn 5663 . . . . . . . . . 10
244112, 99, 243syl2anc 642 . . . . . . . . 9
245111, 244remulcld 8863 . . . . . . . 8
24659adantr 451 . . . . . . . 8
247 letr 8914 . . . . . . . 8
248245, 116, 246, 247syl3anc 1182 . . . . . . 7
249242, 248mpand 656 . . . . . 6
250249expcom 424 . . . . 5
251250a2d 23 . . . 4
2529, 15, 21, 27, 61, 251nn0ind 10108 . . 3
253252com12 27 . 2
2542533impia 1148 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 358   w3a 934   wceq 1623   wcel 1684   wne 2446  wral 2543   wss 3152   class class class wbr 4023  wf 5251  cfv 5255  (class class class)co 5858  cc 8735  cr 8736  cc0 8737  c1 8738   caddc 8740   cmul 8742   cle 8868   cmin 9037  cneg 9038  c2 9795  cn0 9965  cz 10024  cuz 10230   cseq 11046  cexp 11104   cli 11958 This theorem is referenced by:  iseraltlem3  12156 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-er 6660  df-en 6864  df-dom 6865  df-sdom 6866  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-div 9424  df-nn 9747  df-2 9804  df-n0 9966  df-z 10025  df-uz 10231  df-fz 10783  df-seq 11047  df-exp 11105
 Copyright terms: Public domain W3C validator