Metamath Proof Explorer


Theorem iseralt

Description: The alternating series test. If G ( k ) is a decreasing sequence that converges to 0 , then sum_ k e. Z ( -u 1 ^ k ) x. G ( k ) is a convergent series. (Note that the first term is positive if M is even, and negative if M is odd. If the parity of your series does not match up with this, you will need to post-compose the series with multiplication by -u 1 using isermulc2 .) (Contributed by Mario Carneiro, 7-Apr-2015) (Proof shortened by AV, 9-Jul-2022)

Ref Expression
Hypotheses iseralt.1 Z = M
iseralt.2 φ M
iseralt.3 φ G : Z
iseralt.4 φ k Z G k + 1 G k
iseralt.5 φ G 0
iseralt.6 φ k Z F k = 1 k G k
Assertion iseralt φ seq M + F dom

Proof

Step Hyp Ref Expression
1 iseralt.1 Z = M
2 iseralt.2 φ M
3 iseralt.3 φ G : Z
4 iseralt.4 φ k Z G k + 1 G k
5 iseralt.5 φ G 0
6 iseralt.6 φ k Z F k = 1 k G k
7 seqex seq M + F V
8 7 a1i φ seq M + F V
9 climrel Rel
10 9 brrelex1i G 0 G V
11 5 10 syl φ G V
12 eqidd φ n Z G n = G n
13 3 ffvelrnda φ n Z G n
14 13 recnd φ n Z G n
15 1 2 11 12 14 clim0c φ G 0 x + j Z n j G n < x
16 5 15 mpbid φ x + j Z n j G n < x
17 simpr φ x + j Z j Z
18 17 1 eleqtrdi φ x + j Z j M
19 eluzelz j M j
20 uzid j j j
21 18 19 20 3syl φ x + j Z j j
22 peano2uz j j j + 1 j
23 2fveq3 n = j + 1 G n = G j + 1
24 23 breq1d n = j + 1 G n < x G j + 1 < x
25 24 rspcv j + 1 j n j G n < x G j + 1 < x
26 21 22 25 3syl φ x + j Z n j G n < x G j + 1 < x
27 eluzelz n j n
28 27 ad2antll φ j Z n j n
29 28 zcnd φ j Z n j n
30 19 1 eleq2s j Z j
31 30 ad2antrl φ j Z n j j
32 31 zcnd φ j Z n j j
33 29 32 subcld φ j Z n j n j
34 2cnd φ j Z n j 2
35 2ne0 2 0
36 35 a1i φ j Z n j 2 0
37 33 34 36 divcan2d φ j Z n j 2 n j 2 = n j
38 37 oveq2d φ j Z n j j + 2 n j 2 = j + n - j
39 32 29 pncan3d φ j Z n j j + n - j = n
40 38 39 eqtr2d φ j Z n j n = j + 2 n j 2
41 40 adantr φ j Z n j n j 2 n = j + 2 n j 2
42 41 fveq2d φ j Z n j n j 2 seq M + F n = seq M + F j + 2 n j 2
43 42 fvoveq1d φ j Z n j n j 2 seq M + F n seq M + F j = seq M + F j + 2 n j 2 seq M + F j
44 simpll φ j Z n j n j 2 φ
45 simpl j Z n j j Z
46 45 ad2antlr φ j Z n j n j 2 j Z
47 simpr φ j Z n j n j 2 n j 2
48 28 31 zsubcld φ j Z n j n j
49 48 zred φ j Z n j n j
50 2rp 2 +
51 50 a1i φ j Z n j 2 +
52 eluzle n j j n
53 52 ad2antll φ j Z n j j n
54 28 zred φ j Z n j n
55 31 zred φ j Z n j j
56 54 55 subge0d φ j Z n j 0 n j j n
57 53 56 mpbird φ j Z n j 0 n j
58 49 51 57 divge0d φ j Z n j 0 n j 2
59 58 adantr φ j Z n j n j 2 0 n j 2
60 elnn0z n j 2 0 n j 2 0 n j 2
61 47 59 60 sylanbrc φ j Z n j n j 2 n j 2 0
62 1 2 3 4 5 6 iseraltlem3 φ j Z n j 2 0 seq M + F j + 2 n j 2 seq M + F j G j + 1 seq M + F j + 2 n j 2 + 1 seq M + F j G j + 1
63 62 simpld φ j Z n j 2 0 seq M + F j + 2 n j 2 seq M + F j G j + 1
64 44 46 61 63 syl3anc φ j Z n j n j 2 seq M + F j + 2 n j 2 seq M + F j G j + 1
65 43 64 eqbrtrd φ j Z n j n j 2 seq M + F n seq M + F j G j + 1
66 2div2e1 2 2 = 1
67 66 oveq2i n - j + 1 2 2 2 = n - j + 1 2 1
68 peano2cn n j n - j + 1
69 33 68 syl φ j Z n j n - j + 1
70 69 34 34 36 divsubdird φ j Z n j n j + 1 - 2 2 = n - j + 1 2 2 2
71 df-2 2 = 1 + 1
72 71 oveq2i n j + 1 - 2 = n j + 1 - 1 + 1
73 ax-1cn 1
74 73 a1i φ j Z n j 1
75 33 74 74 pnpcan2d φ j Z n j n j + 1 - 1 + 1 = n - j - 1
76 72 75 syl5eq φ j Z n j n j + 1 - 2 = n - j - 1
77 76 oveq1d φ j Z n j n j + 1 - 2 2 = n - j - 1 2
78 70 77 eqtr3d φ j Z n j n - j + 1 2 2 2 = n - j - 1 2
79 67 78 eqtr3id φ j Z n j n - j + 1 2 1 = n - j - 1 2
80 79 oveq2d φ j Z n j 2 n - j + 1 2 1 = 2 n - j - 1 2
81 subcl n j 1 n - j - 1
82 33 73 81 sylancl φ j Z n j n - j - 1
83 82 34 36 divcan2d φ j Z n j 2 n - j - 1 2 = n - j - 1
84 29 32 74 sub32d φ j Z n j n - j - 1 = n - 1 - j
85 80 83 84 3eqtrd φ j Z n j 2 n - j + 1 2 1 = n - 1 - j
86 85 oveq2d φ j Z n j j + 2 n - j + 1 2 1 = j + n 1 - j
87 subcl n 1 n 1
88 29 73 87 sylancl φ j Z n j n 1
89 32 88 pncan3d φ j Z n j j + n 1 - j = n 1
90 86 89 eqtrd φ j Z n j j + 2 n - j + 1 2 1 = n 1
91 90 oveq1d φ j Z n j j + 2 n - j + 1 2 1 + 1 = n - 1 + 1
92 npcan n 1 n - 1 + 1 = n
93 29 73 92 sylancl φ j Z n j n - 1 + 1 = n
94 91 93 eqtr2d φ j Z n j n = j + 2 n - j + 1 2 1 + 1
95 94 adantr φ j Z n j n - j + 1 2 n = j + 2 n - j + 1 2 1 + 1
96 95 fveq2d φ j Z n j n - j + 1 2 seq M + F n = seq M + F j + 2 n - j + 1 2 1 + 1
97 96 fvoveq1d φ j Z n j n - j + 1 2 seq M + F n seq M + F j = seq M + F j + 2 n - j + 1 2 1 + 1 seq M + F j
98 simpll φ j Z n j n - j + 1 2 φ
99 45 ad2antlr φ j Z n j n - j + 1 2 j Z
100 simpr φ j Z n j n - j + 1 2 n - j + 1 2
101 uznn0sub n j n j 0
102 101 ad2antll φ j Z n j n j 0
103 nn0p1nn n j 0 n - j + 1
104 102 103 syl φ j Z n j n - j + 1
105 104 nnrpd φ j Z n j n - j + 1 +
106 105 rphalfcld φ j Z n j n - j + 1 2 +
107 106 rpgt0d φ j Z n j 0 < n - j + 1 2
108 107 adantr φ j Z n j n - j + 1 2 0 < n - j + 1 2
109 elnnz n - j + 1 2 n - j + 1 2 0 < n - j + 1 2
110 100 108 109 sylanbrc φ j Z n j n - j + 1 2 n - j + 1 2
111 nnm1nn0 n - j + 1 2 n - j + 1 2 1 0
112 110 111 syl φ j Z n j n - j + 1 2 n - j + 1 2 1 0
113 1 2 3 4 5 6 iseraltlem3 φ j Z n - j + 1 2 1 0 seq M + F j + 2 n - j + 1 2 1 seq M + F j G j + 1 seq M + F j + 2 n - j + 1 2 1 + 1 seq M + F j G j + 1
114 113 simprd φ j Z n - j + 1 2 1 0 seq M + F j + 2 n - j + 1 2 1 + 1 seq M + F j G j + 1
115 98 99 112 114 syl3anc φ j Z n j n - j + 1 2 seq M + F j + 2 n - j + 1 2 1 + 1 seq M + F j G j + 1
116 97 115 eqbrtrd φ j Z n j n - j + 1 2 seq M + F n seq M + F j G j + 1
117 zeo n j n j 2 n - j + 1 2
118 48 117 syl φ j Z n j n j 2 n - j + 1 2
119 65 116 118 mpjaodan φ j Z n j seq M + F n seq M + F j G j + 1
120 1 peano2uzs j Z j + 1 Z
121 120 adantr j Z n j j + 1 Z
122 ffvelrn G : Z j + 1 Z G j + 1
123 3 121 122 syl2an φ j Z n j G j + 1
124 1 2 3 4 5 iseraltlem1 φ j + 1 Z 0 G j + 1
125 121 124 sylan2 φ j Z n j 0 G j + 1
126 123 125 absidd φ j Z n j G j + 1 = G j + 1
127 119 126 breqtrrd φ j Z n j seq M + F n seq M + F j G j + 1
128 127 adantlr φ x + j Z n j seq M + F n seq M + F j G j + 1
129 neg1rr 1
130 129 a1i φ k Z 1
131 neg1ne0 1 0
132 131 a1i φ k Z 1 0
133 eluzelz k M k
134 133 1 eleq2s k Z k
135 134 adantl φ k Z k
136 130 132 135 reexpclzd φ k Z 1 k
137 3 ffvelrnda φ k Z G k
138 136 137 remulcld φ k Z 1 k G k
139 6 138 eqeltrd φ k Z F k
140 1 2 139 serfre φ seq M + F : Z
141 1 uztrn2 j Z n j n Z
142 ffvelrn seq M + F : Z n Z seq M + F n
143 140 141 142 syl2an φ j Z n j seq M + F n
144 ffvelrn seq M + F : Z j Z seq M + F j
145 140 45 144 syl2an φ j Z n j seq M + F j
146 143 145 resubcld φ j Z n j seq M + F n seq M + F j
147 146 recnd φ j Z n j seq M + F n seq M + F j
148 147 abscld φ j Z n j seq M + F n seq M + F j
149 148 adantlr φ x + j Z n j seq M + F n seq M + F j
150 126 123 eqeltrd φ j Z n j G j + 1
151 150 adantlr φ x + j Z n j G j + 1
152 rpre x + x
153 152 ad2antlr φ x + j Z n j x
154 lelttr seq M + F n seq M + F j G j + 1 x seq M + F n seq M + F j G j + 1 G j + 1 < x seq M + F n seq M + F j < x
155 149 151 153 154 syl3anc φ x + j Z n j seq M + F n seq M + F j G j + 1 G j + 1 < x seq M + F n seq M + F j < x
156 128 155 mpand φ x + j Z n j G j + 1 < x seq M + F n seq M + F j < x
157 140 adantr φ x + seq M + F : Z
158 157 141 142 syl2an φ x + j Z n j seq M + F n
159 156 158 jctild φ x + j Z n j G j + 1 < x seq M + F n seq M + F n seq M + F j < x
160 159 anassrs φ x + j Z n j G j + 1 < x seq M + F n seq M + F n seq M + F j < x
161 160 ralrimdva φ x + j Z G j + 1 < x n j seq M + F n seq M + F n seq M + F j < x
162 26 161 syld φ x + j Z n j G n < x n j seq M + F n seq M + F n seq M + F j < x
163 162 reximdva φ x + j Z n j G n < x j Z n j seq M + F n seq M + F n seq M + F j < x
164 163 ralimdva φ x + j Z n j G n < x x + j Z n j seq M + F n seq M + F n seq M + F j < x
165 16 164 mpd φ x + j Z n j seq M + F n seq M + F n seq M + F j < x
166 1 8 165 caurcvg2 φ seq M + F dom