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

Theorem iseraltlem2 13101
Description: Lemma for iseralt 13103. The terms of an alternating series form a chain of inequalities in alternate terms, so that for example S(1) S(3) S(5) and S(4) S(2) S(0) (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:   ,   ,   ,M   ,   ,   ,N   ,

Proof of Theorem iseraltlem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6069 . . . . . . . . . 10
2 2t0e0 10423 . . . . . . . . . 10
31, 2syl6eq 2470 . . . . . . . . 9
43oveq2d 6077 . . . . . . . 8
54fveq2d 5665 . . . . . . 7
65oveq2d 6077 . . . . . 6
76breq1d 4277 . . . . 5
87imbi2d 310 . . . 4
9 oveq2 6069 . . . . . . . . 9
109oveq2d 6077 . . . . . . . 8
1110fveq2d 5665 . . . . . . 7
1211oveq2d 6077 . . . . . 6
1312breq1d 4277 . . . . 5
1413imbi2d 310 . . . 4
15 oveq2 6069 . . . . . . . . 9
1615oveq2d 6077 . . . . . . . 8
1716fveq2d 5665 . . . . . . 7
1817oveq2d 6077 . . . . . 6
1918breq1d 4277 . . . . 5
2019imbi2d 310 . . . 4
21 oveq2 6069 . . . . . . . . 9
2221oveq2d 6077 . . . . . . . 8
2322fveq2d 5665 . . . . . . 7
2423oveq2d 6077 . . . . . 6
2524breq1d 4277 . . . . 5
2625imbi2d 310 . . . 4
27 iseralt.1 . . . . . . . . . . . 12
28 uzssz 10825 . . . . . . . . . . . 12
2927, 28eqsstri 3363 . . . . . . . . . . 11
3029a1i 11 . . . . . . . . . 10
3130sselda 3333 . . . . . . . . 9
3231zcnd 10693 . . . . . . . 8
3332addid1d 9515 . . . . . . 7
3433fveq2d 5665 . . . . . 6
3534oveq2d 6077 . . . . 5
36 neg1rr 10372 . . . . . . . . 9
37 neg1ne0 10373 . . . . . . . . 9
38 reexpclz 11826 . . . . . . . . 9
3936, 37, 38mp3an12 1289 . . . . . . . 8
4031, 39syl 16 . . . . . . 7
41 iseralt.2 . . . . . . . . 9
42 iseralt.6 . . . . . . . . . 10
4330sselda 3333 . . . . . . . . . . . 12
44 reexpclz 11826 . . . . . . . . . . . . 13
4536, 37, 44mp3an12 1289 . . . . . . . . . . . 12
4643, 45syl 16 . . . . . . . . . . 11
47 iseralt.3 . . . . . . . . . . . 12
4847ffvelrnda 5813 . . . . . . . . . . 11
4946, 48remulcld 9360 . . . . . . . . . 10
5042, 49eqeltrd 2496 . . . . . . . . 9
5127, 41, 50serfre 11776 . . . . . . . 8
5251ffvelrnda 5813 . . . . . . 7
5340, 52remulcld 9360 . . . . . 6
5453leidd 9852 . . . . 5
5535, 54eqbrtrd 4287 . . . 4
5647ad2antrr 710 . . . . . . . . . . 11
57 ax-1cn 9286 . . . . . . . . . . . . . . . 16
58572timesi 10388 . . . . . . . . . . . . . . 15
5958oveq2i 6072 . . . . . . . . . . . . . 14
60 simpr 451 . . . . . . . . . . . . . . . . . . 19
6160, 27syl6eleq 2512 . . . . . . . . . . . . . . . . . 18
6261adantr 455 . . . . . . . . . . . . . . . . 17
63 eluzelz 10815 . . . . . . . . . . . . . . . . 17
6462, 63syl 16 . . . . . . . . . . . . . . . 16
6564zcnd 10693 . . . . . . . . . . . . . . 15
66 2cn 10338 . . . . . . . . . . . . . . . 16
67 nn0cn 10535 . . . . . . . . . . . . . . . . 17
6867adantl 456 . . . . . . . . . . . . . . . 16
69 mulcl 9312 . . . . . . . . . . . . . . . 16
7066, 68, 69sylancr 648 . . . . . . . . . . . . . . 15
7166, 57mulcli 9337 . . . . . . . . . . . . . . . 16
7271a1i 11 . . . . . . . . . . . . . . 15
7365, 70, 72addassd 9354 . . . . . . . . . . . . . 14
7459, 73syl5eqr 2468 . . . . . . . . . . . . 13
75 2nn0 10542 . . . . . . . . . . . . . . . . . 18
76 simpr 451 . . . . . . . . . . . . . . . . . 18
77 nn0mulcl 10562 . . . . . . . . . . . . . . . . . 18
7875, 76, 77sylancr 648 . . . . . . . . . . . . . . . . 17
79 uzaddcl 10856 . . . . . . . . . . . . . . . . 17
8062, 78, 79syl2anc 646 . . . . . . . . . . . . . . . 16
8128, 80sseldi 3331 . . . . . . . . . . . . . . 15
8281zcnd 10693 . . . . . . . . . . . . . 14
8357a1i 11 . . . . . . . . . . . . . 14
8482, 83, 83addassd 9354 . . . . . . . . . . . . 13
85 2cnd 10340 . . . . . . . . . . . . . . 15
8685, 68, 83adddid 9356 . . . . . . . . . . . . . 14
8786oveq2d 6077 . . . . . . . . . . . . 13
8874, 84, 873eqtr4d 2464 . . . . . . . . . . . 12
89 peano2nn0 10566 . . . . . . . . . . . . . . . 16
9089adantl 456 . . . . . . . . . . . . . . 15
91 nn0mulcl 10562 . . . . . . . . . . . . . . 15
9275, 90, 91sylancr 648 . . . . . . . . . . . . . 14
93 uzaddcl 10856 . . . . . . . . . . . . . 14
9462, 92, 93syl2anc 646 . . . . . . . . . . . . 13
9594, 27syl6eleqr 2513 . . . . . . . . . . . 12
9688, 95eqeltrd 2496 . . . . . . . . . . 11
9756, 96ffvelrnd 5814 . . . . . . . . . 10
98 peano2uz 10853 . . . . . . . . . . . . 13
9980, 98syl 16 . . . . . . . . . . . 12
10099, 27syl6eleqr 2513 . . . . . . . . . . 11
10156, 100ffvelrnd 5814 . . . . . . . . . 10
10297, 101resubcld 9722 . . . . . . . . 9
103 0red 9333 . . . . . . . . 9
10440adantr 455 . . . . . . . . . 10
10551ad2antrr 710 . . . . . . . . . . 11
10680, 27syl6eleqr 2513 . . . . . . . . . . 11
107105, 106ffvelrnd 5814 . . . . . . . . . 10
108104, 107remulcld 9360 . . . . . . . . 9
109 iseralt.4 . . . . . . . . . . . . 13
110109ralrimiva 2778 . . . . . . . . . . . 12
111110ad2antrr 710 . . . . . . . . . . 11
112 oveq1 6068 . . . . . . . . . . . . . 14
113112fveq2d 5665 . . . . . . . . . . . . 13
114 fveq2 5661 . . . . . . . . . . . . 13
115113, 114breq12d 4280 . . . . . . . . . . . 12
116115rspcv 3047 . . . . . . . . . . 11
117100, 111, 116sylc 59 . . . . . . . . . 10
11897, 101suble0d 9876 . . . . . . . . . 10
119117, 118mpbird 226 . . . . . . . . 9
120102, 103, 108, 119leadd2dd 9900 . . . . . . . 8
121 seqp1 11762 . . . . . . . . . . . . 13
12299, 121syl 16 . . . . . . . . . . . 12
123 seqp1 11762 . . . . . . . . . . . . . 14
12480, 123syl 16 . . . . . . . . . . . . 13
125124oveq1d 6076 . . . . . . . . . . . 12
126122, 125eqtrd 2454 . . . . . . . . . . 11
12788fveq2d 5665 . . . . . . . . . . 11
128107recnd 9358 . . . . . . . . . . . 12
12942ralrimiva 2778 . . . . . . . . . . . . . . . . 17
130129ad2antrr 710 . . . . . . . . . . . . . . . 16
131 fveq2 5661 . . . . . . . . . . . . . . . . . 18
132 oveq2 6069 . . . . . . . . . . . . . . . . . . 19
133132, 114oveq12d 6079 . . . . . . . . . . . . . . . . . 18
134131, 133eqeq12d 2436 . . . . . . . . . . . . . . . . 17
135134rspcv 3047 . . . . . . . . . . . . . . . 16
136100, 130, 135sylc 59 . . . . . . . . . . . . . . 15
137 neg1cn 10371 . . . . . . . . . . . . . . . . . . 19
138137a1i 11 . . . . . . . . . . . . . . . . . 18
13937a1i 11 . . . . . . . . . . . . . . . . . 18
140138, 139, 81expp1zd 11958 . . . . . . . . . . . . . . . . 17
14136a1i 11 . . . . . . . . . . . . . . . . . . . 20
142141, 139, 81reexpclzd 11974 . . . . . . . . . . . . . . . . . . 19
143142recnd 9358 . . . . . . . . . . . . . . . . . 18
144 mulcom 9314 . . . . . . . . . . . . . . . . . 18
145143, 137, 144sylancl 647 . . . . . . . . . . . . . . . . 17
146143mulm1d 9742 . . . . . . . . . . . . . . . . 17
147140, 145, 1463eqtrd 2458 . . . . . . . . . . . . . . . 16
148147oveq1d 6076 . . . . . . . . . . . . . . 15
149101recnd 9358 . . . . . . . . . . . . . . . 16
150 mulneg12 9729 . . . . . . . . . . . . . . . 16
151143, 149, 150syl2anc 646 . . . . . . . . . . . . . . 15
152136, 148, 1513eqtrd 2458 . . . . . . . . . . . . . 14
153101renegcld 9721 . . . . . . . . . . . . . . 15
154142, 153remulcld 9360 . . . . . . . . . . . . . 14
155152, 154eqeltrd 2496 . . . . . . . . . . . . 13
156155recnd 9358 . . . . . . . . . . . 12
157 fveq2 5661 . . . . . . . . . . . . . . . . . 18
158 oveq2 6069 . . . . . . . . . . . . . . . . . . 19
159 fveq2 5661 . . . . . . . . . . . . . . . . . . 19
160158, 159oveq12d 6079 . . . . . . . . . . . . . . . . . 18
161157, 160eqeq12d 2436 . . . . . . . . . . . . . . . . 17
162161rspcv 3047 . . . . . . . . . . . . . . . 16
16396, 130, 162sylc 59 . . . . . . . . . . . . . . 15
16481peano2zd 10695 . . . . . . . . . . . . . . . . . 18
165138, 139, 164expp1zd 11958 . . . . . . . . . . . . . . . . 17
166147oveq1d 6076 . . . . . . . . . . . . . . . . 17
167 mul2neg 9730 . . . . . . . . . . . . . . . . . . 19
168143, 57, 167sylancl 647 . . . . . . . . . . . . . . . . . 18
169143mulid1d 9349 . . . . . . . . . . . . . . . . . 18
170168, 169eqtrd 2454 . . . . . . . . . . . . . . . . 17
171165, 166, 1703eqtrd 2458 . . . . . . . . . . . . . . . 16
172171oveq1d 6076 . . . . . . . . . . . . . . 15
173163, 172eqtrd 2454 . . . . . . . . . . . . . 14
174142, 97remulcld 9360 . . . . . . . . . . . . . 14
175173, 174eqeltrd 2496 . . . . . . . . . . . . 13
176175recnd 9358 . . . . . . . . . . . 12
177128, 156, 176addassd 9354 . . . . . . . . . . 11
178126, 127, 1773eqtr3d 2462 . . . . . . . . . 10
179178oveq2d 6077 . . . . . . . . 9
180104recnd 9358 . . . . . . . . . 10
181155, 175readdcld 9359 . . . . . . . . . . 11
182181recnd 9358 . . . . . . . . . 10
183180, 128, 182adddid 9356 . . . . . . . . 9
184180, 156, 176adddid 9356 . . . . . . . . . . 11
185152oveq2d 6077 . . . . . . . . . . . . . 14
186153recnd 9358 . . . . . . . . . . . . . . 15
187180, 143, 186mulassd 9355 . . . . . . . . . . . . . 14
188185, 187eqtr4d 2457 . . . . . . . . . . . . 13
18985, 65, 68adddid 9356 . . . . . . . . . . . . . . . . 17
190652timesd 10513 . . . . . . . . . . . . . . . . . 18
191190oveq1d 6076 . . . . . . . . . . . . . . . . 17
19265, 65, 70addassd 9354 . . . . . . . . . . . . . . . . 17
193189, 191, 1923eqtrrd 2459 . . . . . . . . . . . . . . . 16
194193oveq2d 6077 . . . . . . . . . . . . . . 15
195 expaddz 11849 . . . . . . . . . . . . . . . 16
196138, 139, 64, 81, 195syl22anc 1204 . . . . . . . . . . . . . . 15
197 2z 10623 . . . . . . . . . . . . . . . . . 18
198197a1i 11 . . . . . . . . . . . . . . . . 17
199 nn0z 10614 . . . . . . . . . . . . . . . . . 18
200 zaddcl 10630 . . . . . . . . . . . . . . . . . 18
20131, 199, 200syl2an 467 . . . . . . . . . . . . . . . . 17
202 expmulz 11851 . . . . . . . . . . . . . . . . 17
203138, 139, 198, 201, 202syl22anc 1204 . . . . . . . . . . . . . . . 16
204 neg1sqe1 11902 . . . . . . . . . . . . . . . . . 18
205204oveq1i 6071 . . . . . . . . . . . . . . . . 17
206 1exp 11834 . . . . . . . . . . . . . . . . . 18
207201,