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

Theorem iseraltlem2 13160
Description: Lemma for iseralt 13162. 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 6099 . . . . . . . . . 10
2 2t0e0 10477 . . . . . . . . . 10
31, 2syl6eq 2491 . . . . . . . . 9
43oveq2d 6107 . . . . . . . 8
54fveq2d 5695 . . . . . . 7
65oveq2d 6107 . . . . . 6
76breq1d 4302 . . . . 5
87imbi2d 316 . . . 4
9 oveq2 6099 . . . . . . . . 9
109oveq2d 6107 . . . . . . . 8
1110fveq2d 5695 . . . . . . 7
1211oveq2d 6107 . . . . . 6
1312breq1d 4302 . . . . 5
1413imbi2d 316 . . . 4
15 oveq2 6099 . . . . . . . . 9
1615oveq2d 6107 . . . . . . . 8
1716fveq2d 5695 . . . . . . 7
1817oveq2d 6107 . . . . . 6
1918breq1d 4302 . . . . 5
2019imbi2d 316 . . . 4
21 oveq2 6099 . . . . . . . . 9
2221oveq2d 6107 . . . . . . . 8
2322fveq2d 5695 . . . . . . 7
2423oveq2d 6107 . . . . . 6
2524breq1d 4302 . . . . 5
2625imbi2d 316 . . . 4
27 iseralt.1 . . . . . . . . . . . 12
28 uzssz 10880 . . . . . . . . . . . 12
2927, 28eqsstri 3386 . . . . . . . . . . 11
3029a1i 11 . . . . . . . . . 10
3130sselda 3356 . . . . . . . . 9
3231zcnd 10748 . . . . . . . 8
3332addid1d 9569 . . . . . . 7
3433fveq2d 5695 . . . . . 6
3534oveq2d 6107 . . . . 5
36 neg1rr 10426 . . . . . . . . 9
37 neg1ne0 10427 . . . . . . . . 9
38 reexpclz 11885 . . . . . . . . 9
3936, 37, 38mp3an12 1304 . . . . . . . 8
4031, 39syl 16 . . . . . . 7
41 iseralt.2 . . . . . . . . 9
42 iseralt.6 . . . . . . . . . 10
4330sselda 3356 . . . . . . . . . . . 12
44 reexpclz 11885 . . . . . . . . . . . . 13
4536, 37, 44mp3an12 1304 . . . . . . . . . . . 12
4643, 45syl 16 . . . . . . . . . . 11
47 iseralt.3 . . . . . . . . . . . 12
4847ffvelrnda 5843 . . . . . . . . . . 11
4946, 48remulcld 9414 . . . . . . . . . 10
5042, 49eqeltrd 2517 . . . . . . . . 9
5127, 41, 50serfre 11835 . . . . . . . 8
5251ffvelrnda 5843 . . . . . . 7
5340, 52remulcld 9414 . . . . . 6
5453leidd 9906 . . . . 5
5535, 54eqbrtrd 4312 . . . 4
5647ad2antrr 725 . . . . . . . . . . 11
57 ax-1cn 9340 . . . . . . . . . . . . . . . 16
58572timesi 10442 . . . . . . . . . . . . . . 15
5958oveq2i 6102 . . . . . . . . . . . . . 14
60 simpr 461 . . . . . . . . . . . . . . . . . . 19
6160, 27syl6eleq 2533 . . . . . . . . . . . . . . . . . 18
6261adantr 465 . . . . . . . . . . . . . . . . 17
63 eluzelz 10870 . . . . . . . . . . . . . . . . 17
6462, 63syl 16 . . . . . . . . . . . . . . . 16
6564zcnd 10748 . . . . . . . . . . . . . . 15
66 2cn 10392 . . . . . . . . . . . . . . . 16
67 nn0cn 10589 . . . . . . . . . . . . . . . . 17
6867adantl 466 . . . . . . . . . . . . . . . 16
69 mulcl 9366 . . . . . . . . . . . . . . . 16
7066, 68, 69sylancr 663 . . . . . . . . . . . . . . 15
7166, 57mulcli 9391 . . . . . . . . . . . . . . . 16
7271a1i 11 . . . . . . . . . . . . . . 15
7365, 70, 72addassd 9408 . . . . . . . . . . . . . 14
7459, 73syl5eqr 2489 . . . . . . . . . . . . 13
75 2nn0 10596 . . . . . . . . . . . . . . . . . 18
76 simpr 461 . . . . . . . . . . . . . . . . . 18
77 nn0mulcl 10616 . . . . . . . . . . . . . . . . . 18
7875, 76, 77sylancr 663 . . . . . . . . . . . . . . . . 17
79 uzaddcl 10911 . . . . . . . . . . . . . . . . 17
8062, 78, 79syl2anc 661 . . . . . . . . . . . . . . . 16
8128, 80sseldi 3354 . . . . . . . . . . . . . . 15
8281zcnd 10748 . . . . . . . . . . . . . 14
8357a1i 11 . . . . . . . . . . . . . 14
8482, 83, 83addassd 9408 . . . . . . . . . . . . 13
85 2cnd 10394 . . . . . . . . . . . . . . 15
8685, 68, 83adddid 9410 . . . . . . . . . . . . . 14
8786oveq2d 6107 . . . . . . . . . . . . 13
8874, 84, 873eqtr4d 2485 . . . . . . . . . . . 12
89 peano2nn0 10620 . . . . . . . . . . . . . . . 16
9089adantl 466 . . . . . . . . . . . . . . 15
91 nn0mulcl 10616 . . . . . . . . . . . . . . 15
9275, 90, 91sylancr 663 . . . . . . . . . . . . . 14
93 uzaddcl 10911 . . . . . . . . . . . . . 14
9462, 92, 93syl2anc 661 . . . . . . . . . . . . 13
9594, 27syl6eleqr 2534 . . . . . . . . . . . 12
9688, 95eqeltrd 2517 . . . . . . . . . . 11
9756, 96ffvelrnd 5844 . . . . . . . . . 10
98 peano2uz 10908 . . . . . . . . . . . . 13
9980, 98syl 16 . . . . . . . . . . . 12
10099, 27syl6eleqr 2534 . . . . . . . . . . 11
10156, 100ffvelrnd 5844 . . . . . . . . . 10
10297, 101resubcld 9776 . . . . . . . . 9
103 0red 9387 . . . . . . . . 9
10440adantr 465 . . . . . . . . . 10
10551ad2antrr 725 . . . . . . . . . . 11
10680, 27syl6eleqr 2534 . . . . . . . . . . 11
107105, 106ffvelrnd 5844 . . . . . . . . . 10
108104, 107remulcld 9414 . . . . . . . . 9
109 iseralt.4 . . . . . . . . . . . . 13
110109ralrimiva 2799 . . . . . . . . . . . 12
111110ad2antrr 725 . . . . . . . . . . 11
112 oveq1 6098 . . . . . . . . . . . . . 14
113112fveq2d 5695 . . . . . . . . . . . . 13
114 fveq2 5691 . . . . . . . . . . . . 13
115113, 114breq12d 4305 . . . . . . . . . . . 12
116115rspcv 3069 . . . . . . . . . . 11
117100, 111, 116sylc 60 . . . . . . . . . 10
11897, 101suble0d 9930 . . . . . . . . . 10
119117, 118mpbird 232 . . . . . . . . 9
120102, 103, 108, 119leadd2dd 9954 . . . . . . . 8
121 seqp1 11821 . . . . . . . . . . . . 13
12299, 121syl 16 . . . . . . . . . . . 12
123 seqp1 11821 . . . . . . . . . . . . . 14
12480, 123syl 16 . . . . . . . . . . . . 13
125124oveq1d 6106 . . . . . . . . . . . 12
126122, 125eqtrd 2475 . . . . . . . . . . 11
12788fveq2d 5695 . . . . . . . . . . 11
128107recnd 9412 . . . . . . . . . . . 12
12942ralrimiva 2799 . . . . . . . . . . . . . . . . 17
130129ad2antrr 725 . . . . . . . . . . . . . . . 16
131 fveq2 5691 . . . . . . . . . . . . . . . . . 18
132 oveq2 6099 . . . . . . . . . . . . . . . . . . 19
133132, 114oveq12d 6109 . . . . . . . . . . . . . . . . . 18
134131, 133eqeq12d 2457 . . . . . . . . . . . . . . . . 17
135134rspcv 3069 . . . . . . . . . . . . . . . 16
136100, 130, 135sylc 60 . . . . . . . . . . . . . . 15
137 neg1cn 10425 . . . . . . . . . . . . . . . . . . 19
138137a1i 11 . . . . . . . . . . . . . . . . . 18
13937a1i 11 . . . . . . . . . . . . . . . . . 18
140138, 139, 81expp1zd 12017 . . . . . . . . . . . . . . . . 17
14136a1i 11 . . . . . . . . . . . . . . . . . . . 20
142141, 139, 81reexpclzd 12033 . . . . . . . . . . . . . . . . . . 19
143142recnd 9412 . . . . . . . . . . . . . . . . . 18
144 mulcom 9368 . . . . . . . . . . . . . . . . . 18
145143, 137, 144sylancl 662 . . . . . . . . . . . . . . . . 17
146143mulm1d 9796 . . . . . . . . . . . . . . . . 17
147140, 145, 1463eqtrd 2479 . . . . . . . . . . . . . . . 16
148147oveq1d 6106 . . . . . . . . . . . . . . 15
149101recnd 9412 . . . . . . . . . . . . . . . 16
150 mulneg12 9783 . . . . . . . . . . . . . . . 16
151143, 149, 150syl2anc 661 . . . . . . . . . . . . . . 15
152136, 148, 1513eqtrd 2479 . . . . . . . . . . . . . 14
153101renegcld 9775 . . . . . . . . . . . . . . 15
154142, 153remulcld 9414 . . . . . . . . . . . . . 14
155152, 154eqeltrd 2517 . . . . . . . . . . . . 13
156155recnd 9412 . . . . . . . . . . . 12
157 fveq2 5691 . . . . . . . . . . . . . . . . . 18
158 oveq2 6099 . . . . . . . . . . . . . . . . . . 19
159 fveq2 5691 . . . . . . . . . . . . . . . . . . 19
160158, 159oveq12d 6109 . . . . . . . . . . . . . . . . . 18
161157, 160eqeq12d 2457 . . . . . . . . . . . . . . . . 17
162161rspcv 3069 . . . . . . . . . . . . . . . 16
16396, 130, 162sylc 60 . . . . . . . . . . . . . . 15
16481peano2zd 10750 . . . . . . . . . . . . . . . . . 18
165138, 139, 164expp1zd 12017 . . . . . . . . . . . . . . . . 17
166147oveq1d 6106 . . . . . . . . . . . . . . . . 17
167 mul2neg 9784 . . . . . . . . . . . . . . . . . . 19
168143, 57, 167sylancl 662 . . . . . . . . . . . . . . . . . 18
169143mulid1d 9403 . . . . . . . . . . . . . . . . . 18
170168, 169eqtrd 2475 . . . . . . . . . . . . . . . . 17
171165, 166, 1703eqtrd 2479 . . . . . . . . . . . . . . . 16
172171oveq1d 6106 . . . . . . . . . . . . . . 15
173163, 172eqtrd 2475 . . . . . . . . . . . . . 14
174142, 97remulcld 9414 . . . . . . . . . . . . . 14
175173, 174eqeltrd 2517 . . . . . . . . . . . . 13
176175recnd 9412 . . . . . . . . . . . 12
177128, 156, 176addassd 9408 . . . . . . . . . . 11
178126, 127, 1773eqtr3d 2483 . . . . . . . . . 10
179178oveq2d 6107 . . . . . . . . 9
180104recnd 9412 . . . . . . . . . 10
181155, 175readdcld 9413 . . . . . . . . . . 11
182181recnd 9412 . . . . . . . . . 10
183180, 128, 182adddid 9410 . . . . . . . . 9
184180, 156, 176adddid 9410 . . . . . . . . . . 11
185152oveq2d 6107 . . . . . . . . . . . . . 14
186153recnd 9412 . . . . . . . . . . . . . . 15
187180, 143, 186mulassd 9409 . . . . . . . . . . . . . 14
188185, 187eqtr4d 2478 . . . . . . . . . . . . 13
18985, 65, 68adddid 9410 . . . . . . . . . . . . . . . . 17
190652timesd 10567 . . . . . . . . . . . . . . . . . 18
191190oveq1d 6106 . . . . . . . . . . . . . . . . 17
19265, 65, 70addassd 9408 . . . . . . . . . . . . . . . . 17
193189, 191, 1923eqtrrd 2480 . . . . . . . . . . . . . . . 16
194193oveq2d 6107 . . . . . . . . . . . . . . 15
195 expaddz 11908 . . . . . . . . . . . . . . . 16
196138, 139, 64, 81, 195syl22anc 1219 . . . . . . . . . . . . . . 15
197 2z 10678 . . . . . . . . . . . . . . . . . 18
198197a1i 11 . . . . . . . . . . . . . . . . 17
199 nn0z 10669 . . . . . . . . . . . . . . . . . 18
200 zaddcl 10685 . . . . . . . . . . . . . . . . . 18
20131, 199, 200syl2an 477 . . . . . . . . . . . . . . . . 17
202 expmulz 11910 . . . . . . . . . . . . . . . . 17
203138, 139, 198, 201, 202syl22anc 1219 . . . . . . . . . . . . . . . 16
204 neg1sqe1 11961 . . . . . . . . . . . . . . . . . 18
205204oveq1i 6101 . . . . . . . . . . . . . . . . 17
206 1exp 11893 . . . . . . . . . . . . . . . . . 18
207