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

Theorem iseraltlem2 13318
Description: Lemma for iseralt 13320. 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 6230 . . . . . . . . . 10
2 2t0e0 10615 . . . . . . . . . 10
31, 2syl6eq 2511 . . . . . . . . 9
43oveq2d 6238 . . . . . . . 8
54fveq2d 5817 . . . . . . 7
65oveq2d 6238 . . . . . 6
76breq1d 4419 . . . . 5
87imbi2d 316 . . . 4
9 oveq2 6230 . . . . . . . . 9
109oveq2d 6238 . . . . . . . 8
1110fveq2d 5817 . . . . . . 7
1211oveq2d 6238 . . . . . 6
1312breq1d 4419 . . . . 5
1413imbi2d 316 . . . 4
15 oveq2 6230 . . . . . . . . 9
1615oveq2d 6238 . . . . . . . 8
1716fveq2d 5817 . . . . . . 7
1817oveq2d 6238 . . . . . 6
1918breq1d 4419 . . . . 5
2019imbi2d 316 . . . 4
21 oveq2 6230 . . . . . . . . 9
2221oveq2d 6238 . . . . . . . 8
2322fveq2d 5817 . . . . . . 7
2423oveq2d 6238 . . . . . 6
2524breq1d 4419 . . . . 5
2625imbi2d 316 . . . 4
27 iseralt.1 . . . . . . . . . . . 12
28 uzssz 11019 . . . . . . . . . . . 12
2927, 28eqsstri 3500 . . . . . . . . . . 11
3029a1i 11 . . . . . . . . . 10
3130sselda 3470 . . . . . . . . 9
3231zcnd 10886 . . . . . . . 8
3332addid1d 9706 . . . . . . 7
3433fveq2d 5817 . . . . . 6
3534oveq2d 6238 . . . . 5
36 neg1rr 10564 . . . . . . . . 9
37 neg1ne0 10565 . . . . . . . . 9
38 reexpclz 12042 . . . . . . . . 9
3936, 37, 38mp3an12 1305 . . . . . . . 8
4031, 39syl 16 . . . . . . 7
41 iseralt.2 . . . . . . . . 9
42 iseralt.6 . . . . . . . . . 10
4330sselda 3470 . . . . . . . . . . . 12
44 reexpclz 12042 . . . . . . . . . . . . 13
4536, 37, 44mp3an12 1305 . . . . . . . . . . . 12
4643, 45syl 16 . . . . . . . . . . 11
47 iseralt.3 . . . . . . . . . . . 12
4847ffvelrnda 5966 . . . . . . . . . . 11
4946, 48remulcld 9551 . . . . . . . . . 10
5042, 49eqeltrd 2542 . . . . . . . . 9
5127, 41, 50serfre 11992 . . . . . . . 8
5251ffvelrnda 5966 . . . . . . 7
5340, 52remulcld 9551 . . . . . 6
5453leidd 10043 . . . . 5
5535, 54eqbrtrd 4429 . . . 4
5647ad2antrr 725 . . . . . . . . . . 11
57 ax-1cn 9477 . . . . . . . . . . . . . . . 16
58572timesi 10580 . . . . . . . . . . . . . . 15
5958oveq2i 6233 . . . . . . . . . . . . . 14
60 simpr 461 . . . . . . . . . . . . . . . . . . 19
6160, 27syl6eleq 2552 . . . . . . . . . . . . . . . . . 18
6261adantr 465 . . . . . . . . . . . . . . . . 17
63 eluzelz 11009 . . . . . . . . . . . . . . . . 17
6462, 63syl 16 . . . . . . . . . . . . . . . 16
6564zcnd 10886 . . . . . . . . . . . . . . 15
66 2cn 10530 . . . . . . . . . . . . . . . 16
67 nn0cn 10727 . . . . . . . . . . . . . . . . 17
6867adantl 466 . . . . . . . . . . . . . . . 16
69 mulcl 9503 . . . . . . . . . . . . . . . 16
7066, 68, 69sylancr 663 . . . . . . . . . . . . . . 15
7166, 57mulcli 9528 . . . . . . . . . . . . . . . 16
7271a1i 11 . . . . . . . . . . . . . . 15
7365, 70, 72addassd 9545 . . . . . . . . . . . . . 14
7459, 73syl5eqr 2509 . . . . . . . . . . . . 13
75 2nn0 10734 . . . . . . . . . . . . . . . . . 18
76 simpr 461 . . . . . . . . . . . . . . . . . 18
77 nn0mulcl 10754 . . . . . . . . . . . . . . . . . 18
7875, 76, 77sylancr 663 . . . . . . . . . . . . . . . . 17
79 uzaddcl 11050 . . . . . . . . . . . . . . . . 17
8062, 78, 79syl2anc 661 . . . . . . . . . . . . . . . 16
8128, 80sseldi 3468 . . . . . . . . . . . . . . 15
8281zcnd 10886 . . . . . . . . . . . . . 14
8357a1i 11 . . . . . . . . . . . . . 14
8482, 83, 83addassd 9545 . . . . . . . . . . . . 13
85 2cnd 10532 . . . . . . . . . . . . . . 15
8685, 68, 83adddid 9547 . . . . . . . . . . . . . 14
8786oveq2d 6238 . . . . . . . . . . . . 13
8874, 84, 873eqtr4d 2505 . . . . . . . . . . . 12
89 peano2nn0 10758 . . . . . . . . . . . . . . . 16
9089adantl 466 . . . . . . . . . . . . . . 15
91 nn0mulcl 10754 . . . . . . . . . . . . . . 15
9275, 90, 91sylancr 663 . . . . . . . . . . . . . 14
93 uzaddcl 11050 . . . . . . . . . . . . . 14
9462, 92, 93syl2anc 661 . . . . . . . . . . . . 13
9594, 27syl6eleqr 2553 . . . . . . . . . . . 12
9688, 95eqeltrd 2542 . . . . . . . . . . 11
9756, 96ffvelrnd 5967 . . . . . . . . . 10
98 peano2uz 11047 . . . . . . . . . . . . 13
9980, 98syl 16 . . . . . . . . . . . 12
10099, 27syl6eleqr 2553 . . . . . . . . . . 11
10156, 100ffvelrnd 5967 . . . . . . . . . 10
10297, 101resubcld 9913 . . . . . . . . 9
103 0red 9524 . . . . . . . . 9
10440adantr 465 . . . . . . . . . 10
10551ad2antrr 725 . . . . . . . . . . 11
10680, 27syl6eleqr 2553 . . . . . . . . . . 11
107105, 106ffvelrnd 5967 . . . . . . . . . 10
108104, 107remulcld 9551 . . . . . . . . 9
109 iseralt.4 . . . . . . . . . . . . 13
110109ralrimiva 2831 . . . . . . . . . . . 12
111110ad2antrr 725 . . . . . . . . . . 11
112 oveq1 6229 . . . . . . . . . . . . . 14
113112fveq2d 5817 . . . . . . . . . . . . 13
114 fveq2 5813 . . . . . . . . . . . . 13
115113, 114breq12d 4422 . . . . . . . . . . . 12
116115rspcv 3178 . . . . . . . . . . 11
117100, 111, 116sylc 60 . . . . . . . . . 10
11897, 101suble0d 10067 . . . . . . . . . 10
119117, 118mpbird 232 . . . . . . . . 9
120102, 103, 108, 119leadd2dd 10091 . . . . . . . 8
121 seqp1 11978 . . . . . . . . . . . . 13
12299, 121syl 16 . . . . . . . . . . . 12
123 seqp1 11978 . . . . . . . . . . . . . 14
12480, 123syl 16 . . . . . . . . . . . . 13
125124oveq1d 6237 . . . . . . . . . . . 12
126122, 125eqtrd 2495 . . . . . . . . . . 11
12788fveq2d 5817 . . . . . . . . . . 11
128107recnd 9549 . . . . . . . . . . . 12
12942ralrimiva 2831 . . . . . . . . . . . . . . . . 17
130129ad2antrr 725 . . . . . . . . . . . . . . . 16
131 fveq2 5813 . . . . . . . . . . . . . . . . . 18
132 oveq2 6230 . . . . . . . . . . . . . . . . . . 19
133132, 114oveq12d 6240 . . . . . . . . . . . . . . . . . 18
134131, 133eqeq12d 2476 . . . . . . . . . . . . . . . . 17
135134rspcv 3178 . . . . . . . . . . . . . . . 16
136100, 130, 135sylc 60 . . . . . . . . . . . . . . 15
137 neg1cn 10563 . . . . . . . . . . . . . . . . . . 19
138137a1i 11 . . . . . . . . . . . . . . . . . 18
13937a1i 11 . . . . . . . . . . . . . . . . . 18
140138, 139, 81expp1zd 12174 . . . . . . . . . . . . . . . . 17
14136a1i 11 . . . . . . . . . . . . . . . . . . . 20
142141, 139, 81reexpclzd 12190 . . . . . . . . . . . . . . . . . . 19
143142recnd 9549 . . . . . . . . . . . . . . . . . 18
144 mulcom 9505 . . . . . . . . . . . . . . . . . 18
145143, 137, 144sylancl 662 . . . . . . . . . . . . . . . . 17
146143mulm1d 9933 . . . . . . . . . . . . . . . . 17
147140, 145, 1463eqtrd 2499 . . . . . . . . . . . . . . . 16
148147oveq1d 6237 . . . . . . . . . . . . . . 15
149101recnd 9549 . . . . . . . . . . . . . . . 16
150 mulneg12 9920 . . . . . . . . . . . . . . . 16
151143, 149, 150syl2anc 661 . . . . . . . . . . . . . . 15
152136, 148, 1513eqtrd 2499 . . . . . . . . . . . . . 14
153101renegcld 9912 . . . . . . . . . . . . . . 15
154142, 153remulcld 9551 . . . . . . . . . . . . . 14
155152, 154eqeltrd 2542 . . . . . . . . . . . . 13
156155recnd 9549 . . . . . . . . . . . 12
157 fveq2 5813 . . . . . . . . . . . . . . . . . 18
158 oveq2 6230 . . . . . . . . . . . . . . . . . . 19
159 fveq2 5813 . . . . . . . . . . . . . . . . . . 19
160158, 159oveq12d 6240 . . . . . . . . . . . . . . . . . 18
161157, 160eqeq12d 2476 . . . . . . . . . . . . . . . . 17
162161rspcv 3178 . . . . . . . . . . . . . . . 16
16396, 130, 162sylc 60 . . . . . . . . . . . . . . 15
16481peano2zd 10888 . . . . . . . . . . . . . . . . . 18
165138, 139, 164expp1zd 12174 . . . . . . . . . . . . . . . . 17
166147oveq1d 6237 . . . . . . . . . . . . . . . . 17
167 mul2neg 9921 . . . . . . . . . . . . . . . . . . 19
168143, 57, 167sylancl 662 . . . . . . . . . . . . . . . . . 18
169143mulid1d 9540 . . . . . . . . . . . . . . . . . 18
170168, 169eqtrd 2495 . . . . . . . . . . . . . . . . 17
171165, 166, 1703eqtrd 2499 . . . . . . . . . . . . . . . 16
172171oveq1d 6237 . . . . . . . . . . . . . . 15
173163, 172eqtrd 2495 . . . . . . . . . . . . . 14
174142, 97remulcld 9551 . . . . . . . . . . . . . 14
175173, 174eqeltrd 2542 . . . . . . . . . . . . 13
176175recnd 9549 . . . . . . . . . . . 12
177128, 156, 176addassd 9545 . . . . . . . . . . 11
178126, 127, 1773eqtr3d 2503 . . . . . . . . . 10
179178oveq2d 6238 . . . . . . . . 9
180104recnd 9549 . . . . . . . . . 10
181155, 175readdcld 9550 . . . . . . . . . . 11
182181recnd 9549 . . . . . . . . . 10
183180, 128, 182adddid 9547 . . . . . . . . 9
184180, 156, 176adddid 9547 . . . . . . . . . . 11
185152oveq2d 6238 . . . . . . . . . . . . . 14
186153recnd 9549 . . . . . . . . . . . . . . 15
187180, 143, 186mulassd 9546 . . . . . . . . . . . . . 14
188185, 187eqtr4d 2498 . . . . . . . . . . . . 13
18985, 65, 68adddid 9547 . . . . . . . . . . . . . . . . 17
190652timesd 10705 . . . . . . . . . . . . . . . . . 18
191190oveq1d 6237 . . . . . . . . . . . . . . . . 17
19265, 65, 70addassd 9545 . . . . . . . . . . . . . . . . 17
193189, 191, 1923eqtrrd 2500 . . . . . . . . . . . . . . . 16
194193oveq2d 6238 . . . . . . . . . . . . . . 15
195 expaddz 12065 . . . . . . . . . . . . . . . 16
196138, 139, 64, 81, 195syl22anc 1220 . . . . . . . . . . . . . . 15
197 2z 10816 . . . . . . . . . . . . . . . . . 18
198197a1i 11 . . . . . . . . . . . . . . . . 17
199 nn0z 10807 . . . . . . . . . . . . . . . . . 18
200 zaddcl 10823 . . . . . . . . . . . . . . . . . 18
20131, 199, 200syl2an 477 . . . . . . . . . . . . . . . . 17
202 expmulz 12067 . . . . . . . . . . . . . . . . 17
203138, 139, 198, 201, 202syl22anc 1220 . . . . . . . . . . . . . . . 16
204 neg1sqe1 12118 . . . . . . . . . . . . . . . . . 18
205204oveq1i 6232 . . . . . . . . . . . . . . . . 17
206 1exp 12050 . . . . . . . . . . . . . . . . . 18
207