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

Theorem iseraltlem3 13506
 Description: Lemma for iseralt 13507. From iseraltlem2 13505, we have (-u1 ) S( 2 ) (-u1 ) S( ) and (-u1 ) S( 1) (-u1 ) S( 2 1), and we also have (-u1 ) S( 1)= (-u1 ) S( ) ( 1) for each by the definition of the partial sum , so combining the inequalities we get (-u1 ) S( ) ( 1)= (-u1 ) S( 1) (-u1 ) S( 2 1)= (-u1 ) S( 2 ) ( 2 1) (-u1 ) S( 2 ) (-u1 ) S( ) (-u1 ) S( ) ( 1), so |(-u1 ) S( 2 1) (-u1 ) S( )|= |S( 2 1) S( )| ( 1) and |(-u1 ) S( 2 ) (-u1 ) S( )|= |S( 2 ) S( )| ( 1). Thus, both even and odd partial sums are Cauchy if converges to . (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
iseraltlem3
Distinct variable groups:   ,   ,   ,M   ,   ,   ,N   ,

Proof of Theorem iseraltlem3
StepHypRef Expression
1 neg1rr 10665 . . . . . . . . . 10
21a1i 11 . . . . . . . . 9
3 neg1ne0 10666 . . . . . . . . . 10
43a1i 11 . . . . . . . . 9
5 iseralt.1 . . . . . . . . . . 11
6 uzssz 11129 . . . . . . . . . . 11
75, 6eqsstri 3533 . . . . . . . . . 10
8 simp2 997 . . . . . . . . . 10
97, 8sseldi 3501 . . . . . . . . 9
102, 4, 9reexpclzd 12335 . . . . . . . 8
1110recnd 9643 . . . . . . 7
12 iseralt.2 . . . . . . . . . . 11
13 iseralt.6 . . . . . . . . . . . 12
141a1i 11 . . . . . . . . . . . . . 14
153a1i 11 . . . . . . . . . . . . . 14
16 simpr 461 . . . . . . . . . . . . . . 15
177, 16sseldi 3501 . . . . . . . . . . . . . 14
1814, 15, 17reexpclzd 12335 . . . . . . . . . . . . 13
19 iseralt.3 . . . . . . . . . . . . . 14
2019ffvelrnda 6031 . . . . . . . . . . . . 13
2118, 20remulcld 9645 . . . . . . . . . . . 12
2213, 21eqeltrd 2545 . . . . . . . . . . 11
235, 12, 22serfre 12136 . . . . . . . . . 10
24233ad2ant1 1017 . . . . . . . . 9
258, 5syl6eleq 2555 . . . . . . . . . . 11
26 2nn0 10837 . . . . . . . . . . . 12
27 simp3 998 . . . . . . . . . . . 12
28 nn0mulcl 10857 . . . . . . . . . . . 12
2926, 27, 28sylancr 663 . . . . . . . . . . 11
30 uzaddcl 11166 . . . . . . . . . . 11
3125, 29, 30syl2anc 661 . . . . . . . . . 10
3231, 5syl6eleqr 2556 . . . . . . . . 9
3324, 32ffvelrnd 6032 . . . . . . . 8
3433recnd 9643 . . . . . . 7
3524, 8ffvelrnd 6032 . . . . . . . 8
3635recnd 9643 . . . . . . 7
3711, 34, 36subdid 10037 . . . . . 6
3837fveq2d 5875 . . . . 5
3933, 35resubcld 10012 . . . . . . 7
4039recnd 9643 . . . . . 6
4111, 40absmuld 13285 . . . . 5
4238, 41eqtr3d 2500 . . . 4
432recnd 9643 . . . . . . 7
44 absexpz 13138 . . . . . . 7
4543, 4, 9, 44syl3anc 1228 . . . . . 6
46 ax-1cn 9571 . . . . . . . . . 10
4746absnegi 13232 . . . . . . . . 9
48 abs1 13130 . . . . . . . . 9
4947, 48eqtri 2486 . . . . . . . 8
5049oveq1i 6306 . . . . . . 7
51 1exp 12195 . . . . . . . 8
529, 51syl 16 . . . . . . 7
5350, 52syl5eq 2510 . . . . . 6
5445, 53eqtrd 2498 . . . . 5
5554oveq1d 6311 . . . 4
5640abscld 13267 . . . . . 6
5756recnd 9643 . . . . 5
5857mulid2d 9635 . . . 4
5942, 55, 583eqtrd 2502 . . 3
6010, 35remulcld 9645 . . . . . 6
61193ad2ant1 1017 . . . . . . 7
625peano2uzs 11164 . . . . . . . 8
63623ad2ant2 1018 . . . . . . 7
6461, 63ffvelrnd 6032 . . . . . 6
6560, 64resubcld 10012 . . . . 5
665peano2uzs 11164 . . . . . . . 8
6732, 66syl 16 . . . . . . 7
6824, 67ffvelrnd 6032 . . . . . 6
6910, 68remulcld 9645 . . . . 5
7010, 33remulcld 9645 . . . . 5
71 seqp1 12122 . . . . . . . . . . 11
7225, 71syl 16 . . . . . . . . . 10
7313ralrimiva 2871 . . . . . . . . . . . . 13
74733ad2ant1 1017 . . . . . . . . . . . 12
75 fveq2 5871 . . . . . . . . . . . . . 14
76 oveq2 6304 . . . . . . . . . . . . . . 15
77 fveq2 5871 . . . . . . . . . . . . . . 15
7876, 77oveq12d 6314 . . . . . . . . . . . . . 14
7975, 78eqeq12d 2479 . . . . . . . . . . . . 13
8079rspcv 3206 . . . . . . . . . . . 12
8163, 74, 80sylc 60 . . . . . . . . . . 11
8281oveq2d 6312 . . . . . . . . . 10
8343, 4, 9expp1zd 12319 . . . . . . . . . . . . . 14
84 neg1cn 10664 . . . . . . . . . . . . . . 15
85 mulcom 9599 . . . . . . . . . . . . . . 15
8611, 84, 85sylancl 662 . . . . . . . . . . . . . 14
8711mulm1d 10033 . . . . . . . . . . . . . 14
8883, 86, 873eqtrd 2502 . . . . . . . . . . . . 13
8988oveq1d 6311 . . . . . . . . . . . 12
9064recnd 9643 . . . . . . . . . . . . 13
9111, 90mulneg1d 10034 . . . . . . . . . . . 12
9289, 91eqtrd 2498 . . . . . . . . . . 11
9392oveq2d 6312 . . . . . . . . . 10
9472, 82, 933eqtrd 2502 . . . . . . . . 9
9510, 64remulcld 9645 . . . . . . . . . . 11
9695recnd 9643 . . . . . . . . . 10
9736, 96negsubd 9960 . . . . . . . . 9
9894, 97eqtrd 2498 . . . . . . . 8
9998oveq2d 6312 . . . . . . 7
10011, 36, 96subdid 10037 . . . . . . 7
1019zcnd 10995 . . . . . . . . . . . . . . 15
1021012timesd 10806 . . . . . . . . . . . . . 14
103102oveq2d 6312 . . . . . . . . . . . . 13
104 2z 10921 . . . . . . . . . . . . . . 15
105104a1i 11 . . . . . . . . . . . . . 14
106 expmulz 12212 . . . . . . . . . . . . . 14
10743, 4, 105, 9, 106syl22anc 1229 . . . . . . . . . . . . 13
108103, 107eqtr3d 2500 . . . . . . . . . . . 12
109 neg1sqe1 12263 . . . . . . . . . . . . 13
110109oveq1i 6306 . . . . . . . . . . . 12
111108, 110syl6eq 2514 . . . . . . . . . . 11
112 expaddz 12210 . . . . . . . . . . . 12
11343, 4, 9, 9, 112syl22anc 1229 . . . . . . . . . . 11
114111, 113, 523eqtr3d 2506 . . . . . . . . . 10
115114oveq1d 6311 . . . . . . . . 9
11611, 11, 90mulassd 9640 . . . . . . . . 9
11790mulid2d 9635 . . . . . . . . 9
118115, 116, 1173eqtr3d 2506 . . . . . . . 8
119118oveq2d 6312 . . . . . . 7
12099, 100, 1193eqtrd 2502 . . . . . 6
121 iseralt.4 . . . . . . . . . . 11
122 iseralt.5 . . . . . . . . . . 11
1235, 12, 19, 121, 122, 13iseraltlem2 13505 . . . . . . . . . 10
12462, 123syl3an2 1262 . . . . . . . . 9
125 1cnd 9633 . . . . . . . . . . . 12
12629nn0cnd 10879 . . . . . . . . . . . 12
127101, 125, 126add32d 9825 . . . . . . . . . . 11
128127fveq2d 5875 . . . . . . . . . 10
12988, 128oveq12d 6314 . . . . . . . . 9
13088oveq1d 6311 . . . . . . . . 9
131124, 129, 1303brtr3d 4481 . . . . . . . 8
13268recnd 9643 . . . . . . . . 9
13311, 132mulneg1d 10034 . . . . . . . 8
13424, 63ffvelrnd 6032 . . . . . . . . . 10
135134recnd 9643 . . . . . . . . 9
13611, 135mulneg1d 10034 . . . . . . . 8
137131, 133, 1363brtr3d 4481 . . . . . . 7
13810, 134remulcld 9645 . . . . . . . 8
139138, 69lenegd 10156 . . . . . . 7
140137, 139mpbird 232 . . . . . 6
141120, 140eqbrtrrd 4474 . . . . 5
142 seqp1 12122 . . . . . . . . . 10
14331, 142syl 16 . . . . . . . . 9
144 fveq2 5871 . . . . . . . . . . . . . 14
145 oveq2 6304 . . . . . . . . . . . . . . 15
146 fveq2 5871 . . . . . . . . . . . . . . 15
147145, 146oveq12d 6314 . . . . . . . . . . . . . 14
148144, 147eqeq12d 2479 . . . . . . . . . . . . 13
149148rspcv 3206 . . . . . . . . . . . 12
15067, 74, 149sylc 60 . . . . . . . . . . 11
1517, 63sseldi 3501 . . . . . . . . . . . . . . 15
15229nn0zd 10992 . . . . . . . . . . . . . . 15
153 expaddz 12210 . . . . . . . . . . . . . . 15
15443, 4, 151, 152, 153syl22anc 1229 . . . . . . . . . . . . . 14
15527nn0zd 10992 . . . . . . . . . . . . . . . . 17
156 expmulz 12212 . . . . . . . . . . . . . . . . 17
15743, 4, 105, 155, 156syl22anc 1229 . . . . . . . . . . . . . . . 16
158109oveq1i 6306 . . . . . . . . . . . . . . . . 17
159 1exp 12195 . . . . . . . . . . . . . . . . . 18
160155, 159syl 16 . . . . . . . . . . . . . . . . 17
161158, 160syl5eq 2510 . . . . . . . . . . . . . . . 16
162157, 161eqtrd 2498 . . . . . . . . . . . . . . 15
16388, 162oveq12d 6314 . . . . . . . . . . . . . 14
164154, 163eqtrd 2498 . . . . . . . . . . . . 13
165127oveq2d 6312 . . . . . . . . . . . . 13
16611negcld 9941 . . . . . . . . . . . . . 14
167166mulid1d 9634 . . . . . . . . . . . . 13
168164, 165, 1673eqtr3d 2506 . . . . . . . . . . . 12
169168oveq1d 6311 . . . . . . . . . . 11
17061, 67ffvelrnd 6032 . . . . . . . . . . . . 13
171170recnd 9643 . . . . . . . . . . . 12
17211, 171mulneg1d 10034 . . . . . . . . . . 11
173150, 169, 1723eqtrd 2502 . . . . . . . . . 10
174173oveq2d 6312 . . . . . . . . 9
17510, 170remulcld 9645 . . . . . . . . . . 11
176175recnd 9643 . . . . . . . . . 10
17734, 176negsubd 9960 . . . . . . . . 9
178143, 174, 1773eqtrd 2502 . . . . . . . 8
179178oveq2d 6312 . . . . . . 7
18011, 34, 176subdid 10037 . . . . . . 7
181114oveq1d 6311 . . . . . . . . 9
18211, 11, 171mulassd 9640 . . . . . . . . 9
183171mulid2d 9635 . . . . . . . . 9
184181, 182, 1833eqtr3d 2506 . . . . . . . 8
185184oveq2d 6312 . . . . . . 7