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

Theorem iseraltlem2 13505
 Description: Lemma for iseralt 13507. 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 6304 . . . . . . . . . 10
2 2t0e0 10716 . . . . . . . . . 10
31, 2syl6eq 2514 . . . . . . . . 9
43oveq2d 6312 . . . . . . . 8
54fveq2d 5875 . . . . . . 7
65oveq2d 6312 . . . . . 6
76breq1d 4462 . . . . 5
87imbi2d 316 . . . 4
9 oveq2 6304 . . . . . . . . 9
109oveq2d 6312 . . . . . . . 8
1110fveq2d 5875 . . . . . . 7
1211oveq2d 6312 . . . . . 6
1312breq1d 4462 . . . . 5
1413imbi2d 316 . . . 4
15 oveq2 6304 . . . . . . . . 9
1615oveq2d 6312 . . . . . . . 8
1716fveq2d 5875 . . . . . . 7
1817oveq2d 6312 . . . . . 6
1918breq1d 4462 . . . . 5
2019imbi2d 316 . . . 4
21 oveq2 6304 . . . . . . . . 9
2221oveq2d 6312 . . . . . . . 8
2322fveq2d 5875 . . . . . . 7
2423oveq2d 6312 . . . . . 6
2524breq1d 4462 . . . . 5
2625imbi2d 316 . . . 4
27 iseralt.1 . . . . . . . . . . . 12
28 uzssz 11129 . . . . . . . . . . . 12
2927, 28eqsstri 3533 . . . . . . . . . . 11
3029a1i 11 . . . . . . . . . 10
3130sselda 3503 . . . . . . . . 9
3231zcnd 10995 . . . . . . . 8
3332addid1d 9801 . . . . . . 7
3433fveq2d 5875 . . . . . 6
3534oveq2d 6312 . . . . 5
36 neg1rr 10665 . . . . . . . . 9
37 neg1ne0 10666 . . . . . . . . 9
38 reexpclz 12186 . . . . . . . . 9
3936, 37, 38mp3an12 1314 . . . . . . . 8
4031, 39syl 16 . . . . . . 7
41 iseralt.2 . . . . . . . . 9
42 iseralt.6 . . . . . . . . . 10
4330sselda 3503 . . . . . . . . . . . 12
44 reexpclz 12186 . . . . . . . . . . . . 13
4536, 37, 44mp3an12 1314 . . . . . . . . . . . 12
4643, 45syl 16 . . . . . . . . . . 11
47 iseralt.3 . . . . . . . . . . . 12
4847ffvelrnda 6031 . . . . . . . . . . 11
4946, 48remulcld 9645 . . . . . . . . . 10
5042, 49eqeltrd 2545 . . . . . . . . 9
5127, 41, 50serfre 12136 . . . . . . . 8
5251ffvelrnda 6031 . . . . . . 7
5340, 52remulcld 9645 . . . . . 6
5453leidd 10144 . . . . 5
5535, 54eqbrtrd 4472 . . . 4
5647ad2antrr 725 . . . . . . . . . . 11
57 ax-1cn 9571 . . . . . . . . . . . . . . . 16
58572timesi 10681 . . . . . . . . . . . . . . 15
5958oveq2i 6307 . . . . . . . . . . . . . 14
60 simpr 461 . . . . . . . . . . . . . . . . . . 19
6160, 27syl6eleq 2555 . . . . . . . . . . . . . . . . . 18
6261adantr 465 . . . . . . . . . . . . . . . . 17
63 eluzelz 11119 . . . . . . . . . . . . . . . . 17
6462, 63syl 16 . . . . . . . . . . . . . . . 16
6564zcnd 10995 . . . . . . . . . . . . . . 15
66 2cn 10631 . . . . . . . . . . . . . . . 16
67 nn0cn 10830 . . . . . . . . . . . . . . . . 17
6867adantl 466 . . . . . . . . . . . . . . . 16
69 mulcl 9597 . . . . . . . . . . . . . . . 16
7066, 68, 69sylancr 663 . . . . . . . . . . . . . . 15
7166, 57mulcli 9622 . . . . . . . . . . . . . . . 16
7271a1i 11 . . . . . . . . . . . . . . 15
7365, 70, 72addassd 9639 . . . . . . . . . . . . . 14
7459, 73syl5eqr 2512 . . . . . . . . . . . . 13
75 2nn0 10837 . . . . . . . . . . . . . . . . . 18
76 simpr 461 . . . . . . . . . . . . . . . . . 18
77 nn0mulcl 10857 . . . . . . . . . . . . . . . . . 18
7875, 76, 77sylancr 663 . . . . . . . . . . . . . . . . 17
79 uzaddcl 11166 . . . . . . . . . . . . . . . . 17
8062, 78, 79syl2anc 661 . . . . . . . . . . . . . . . 16
8128, 80sseldi 3501 . . . . . . . . . . . . . . 15
8281zcnd 10995 . . . . . . . . . . . . . 14
83 1cnd 9633 . . . . . . . . . . . . . 14
8482, 83, 83addassd 9639 . . . . . . . . . . . . 13
85 2cnd 10633 . . . . . . . . . . . . . . 15
8685, 68, 83adddid 9641 . . . . . . . . . . . . . 14
8786oveq2d 6312 . . . . . . . . . . . . 13
8874, 84, 873eqtr4d 2508 . . . . . . . . . . . 12
89 peano2nn0 10861 . . . . . . . . . . . . . . . 16
9089adantl 466 . . . . . . . . . . . . . . 15
91 nn0mulcl 10857 . . . . . . . . . . . . . . 15
9275, 90, 91sylancr 663 . . . . . . . . . . . . . 14
93 uzaddcl 11166 . . . . . . . . . . . . . 14
9462, 92, 93syl2anc 661 . . . . . . . . . . . . 13
9594, 27syl6eleqr 2556 . . . . . . . . . . . 12
9688, 95eqeltrd 2545 . . . . . . . . . . 11
9756, 96ffvelrnd 6032 . . . . . . . . . 10
98 peano2uz 11163 . . . . . . . . . . . . 13
9980, 98syl 16 . . . . . . . . . . . 12
10099, 27syl6eleqr 2556 . . . . . . . . . . 11
10156, 100ffvelrnd 6032 . . . . . . . . . 10
10297, 101resubcld 10012 . . . . . . . . 9
103 0red 9618 . . . . . . . . 9
10440adantr 465 . . . . . . . . . 10
10551ad2antrr 725 . . . . . . . . . . 11
10680, 27syl6eleqr 2556 . . . . . . . . . . 11
107105, 106ffvelrnd 6032 . . . . . . . . . 10
108104, 107remulcld 9645 . . . . . . . . 9
109 iseralt.4 . . . . . . . . . . . . 13
110109ralrimiva 2871 . . . . . . . . . . . 12
111110ad2antrr 725 . . . . . . . . . . 11
112 oveq1 6303 . . . . . . . . . . . . . 14
113112fveq2d 5875 . . . . . . . . . . . . 13
114 fveq2 5871 . . . . . . . . . . . . 13
115113, 114breq12d 4465 . . . . . . . . . . . 12
116115rspcv 3206 . . . . . . . . . . 11
117100, 111, 116sylc 60 . . . . . . . . . 10
11897, 101suble0d 10168 . . . . . . . . . 10
119117, 118mpbird 232 . . . . . . . . 9
120102, 103, 108, 119leadd2dd 10192 . . . . . . . 8
121 seqp1 12122 . . . . . . . . . . . . 13
12299, 121syl 16 . . . . . . . . . . . 12
123 seqp1 12122 . . . . . . . . . . . . . 14
12480, 123syl 16 . . . . . . . . . . . . 13
125124oveq1d 6311 . . . . . . . . . . . 12
126122, 125eqtrd 2498 . . . . . . . . . . 11
12788fveq2d 5875 . . . . . . . . . . 11
128107recnd 9643 . . . . . . . . . . . 12
12942ralrimiva 2871 . . . . . . . . . . . . . . . . 17
130129ad2antrr 725 . . . . . . . . . . . . . . . 16
131 fveq2 5871 . . . . . . . . . . . . . . . . . 18
132 oveq2 6304 . . . . . . . . . . . . . . . . . . 19
133132, 114oveq12d 6314 . . . . . . . . . . . . . . . . . 18
134131, 133eqeq12d 2479 . . . . . . . . . . . . . . . . 17
135134rspcv 3206 . . . . . . . . . . . . . . . 16
136100, 130, 135sylc 60 . . . . . . . . . . . . . . 15
137 neg1cn 10664 . . . . . . . . . . . . . . . . . . 19
138137a1i 11 . . . . . . . . . . . . . . . . . 18
13937a1i 11 . . . . . . . . . . . . . . . . . 18
140138, 139, 81expp1zd 12319 . . . . . . . . . . . . . . . . 17
14136a1i 11 . . . . . . . . . . . . . . . . . . . 20
142141, 139, 81reexpclzd 12335 . . . . . . . . . . . . . . . . . . 19
143142recnd 9643 . . . . . . . . . . . . . . . . . 18
144 mulcom 9599 . . . . . . . . . . . . . . . . . 18
145143, 137, 144sylancl 662 . . . . . . . . . . . . . . . . 17
146143mulm1d 10033 . . . . . . . . . . . . . . . . 17
147140, 145, 1463eqtrd 2502 . . . . . . . . . . . . . . . 16
148147oveq1d 6311 . . . . . . . . . . . . . . 15
149101recnd 9643 . . . . . . . . . . . . . . . 16
150 mulneg12 10020 . . . . . . . . . . . . . . . 16
151143, 149, 150syl2anc 661 . . . . . . . . . . . . . . 15
152136, 148, 1513eqtrd 2502 . . . . . . . . . . . . . 14
153101renegcld 10011 . . . . . . . . . . . . . . 15
154142, 153remulcld 9645 . . . . . . . . . . . . . 14
155152, 154eqeltrd 2545 . . . . . . . . . . . . 13
156155recnd 9643 . . . . . . . . . . . 12
157 fveq2 5871 . . . . . . . . . . . . . . . . . 18
158 oveq2 6304 . . . . . . . . . . . . . . . . . . 19
159 fveq2 5871 . . . . . . . . . . . . . . . . . . 19
160158, 159oveq12d 6314 . . . . . . . . . . . . . . . . . 18
161157, 160eqeq12d 2479 . . . . . . . . . . . . . . . . 17
162161rspcv 3206 . . . . . . . . . . . . . . . 16
16396, 130, 162sylc 60 . . . . . . . . . . . . . . 15
16481peano2zd 10997 . . . . . . . . . . . . . . . . . 18
165138, 139, 164expp1zd 12319 . . . . . . . . . . . . . . . . 17
166147oveq1d 6311 . . . . . . . . . . . . . . . . 17
167 mul2neg 10021 . . . . . . . . . . . . . . . . . . 19
168143, 57, 167sylancl 662 . . . . . . . . . . . . . . . . . 18
169143mulid1d 9634 . . . . . . . . . . . . . . . . . 18
170168, 169eqtrd 2498 . . . . . . . . . . . . . . . . 17
171165, 166, 1703eqtrd 2502 . . . . . . . . . . . . . . . 16
172171oveq1d 6311 . . . . . . . . . . . . . . 15
173163, 172eqtrd 2498 . . . . . . . . . . . . . 14
174142, 97remulcld 9645 . . . . . . . . . . . . . 14
175173, 174eqeltrd 2545 . . . . . . . . . . . . 13
176175recnd 9643 . . . . . . . . . . . 12
177128, 156, 176addassd 9639 . . . . . . . . . . 11
178126, 127, 1773eqtr3d 2506 . . . . . . . . . 10
179178oveq2d 6312 . . . . . . . . 9
180104recnd 9643 . . . . . . . . . 10
181155, 175readdcld 9644 . . . . . . . . . . 11
182181recnd 9643 . . . . . . . . . 10
183180, 128, 182adddid 9641 . . . . . . . . 9
184180, 156, 176adddid 9641 . . . . . . . . . . 11
185152oveq2d 6312 . . . . . . . . . . . . . 14
186153recnd 9643 . . . . . . . . . . . . . . 15
187180, 143, 186mulassd 9640 . . . . . . . . . . . . . 14
188185, 187eqtr4d 2501 . . . . . . . . . . . . 13
18985, 65, 68adddid 9641 . . . . . . . . . . . . . . . . 17
190652timesd 10806 . . . . . . . . . . . . . . . . . 18
191190oveq1d 6311 . . . . . . . . . . . . . . . . 17
19265, 65, 70addassd 9639 . . . . . . . . . . . . . . . . 17
193189, 191, 1923eqtrrd 2503 . . . . . . . . . . . . . . . 16
194193oveq2d 6312 . . . . . . . . . . . . . . 15
195 expaddz 12210 . . . . . . . . . . . . . . . 16
196138, 139, 64, 81, 195syl22anc 1229 . . . . . . . . . . . . . . 15
197 2z 10921 . . . . . . . . . . . . . . . . . 18
198197a1i 11 . . . . . . . . . . . . . . . . 17
199 nn0z 10912 . . . . . . . . . . . . . . . . . 18
200 zaddcl 10929 . . . . . . . . . . . . . . . . . 18
20131, 199, 200syl2an 477 . . . . . . . . . . . . . . . . 17
202 expmulz 12212 . . . . . . . . . . . . . . . . 17
203138, 139, 198, 201, 202syl22anc 1229 . . . . . . . . . . . . . . . 16
204 neg1sqe1 12263 . . . . . . . . . . . . . . . . . 18
205204oveq1i 6306 . . . . . . . . . . . . . . . . 17
206 1exp 12195 . . . . . . . . . . . . . . . . . 18
207