Mathbox for Jim Kingdon < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  cvgcmp2nlemabs GIF version

Theorem cvgcmp2nlemabs 13385
 Description: Lemma for cvgcmp2n 13386. The partial sums get closer to each other as we go further out. The proof proceeds by rewriting (seq1( + , 𝐺)‘𝑁) as the sum of (seq1( + , 𝐺)‘𝑀) and a term which gets smaller as 𝑀 gets large. (Contributed by Jim Kingdon, 25-Aug-2023.)
Hypotheses
Ref Expression
cvgcmp2n.cl ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
cvgcmp2n.ge0 ((𝜑𝑘 ∈ ℕ) → 0 ≤ (𝐺𝑘))
cvgcmp2n.lt ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ≤ (1 / (2↑𝑘)))
cvgcmp2nlemabs.m (𝜑𝑀 ∈ ℕ)
cvgcmp2nlemabs.n (𝜑𝑁 ∈ (ℤ𝑀))
Assertion
Ref Expression
cvgcmp2nlemabs (𝜑 → (abs‘((seq1( + , 𝐺)‘𝑁) − (seq1( + , 𝐺)‘𝑀))) < (2 / 𝑀))
Distinct variable groups:   𝑘,𝐺   𝑘,𝑀   𝑘,𝑁   𝜑,𝑘

Proof of Theorem cvgcmp2nlemabs
StepHypRef Expression
1 eqidd 2141 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ‘1)) → (𝐺𝑘) = (𝐺𝑘))
2 cvgcmp2nlemabs.m . . . . . . . . . 10 (𝜑𝑀 ∈ ℕ)
3 cvgcmp2nlemabs.n . . . . . . . . . 10 (𝜑𝑁 ∈ (ℤ𝑀))
4 eluznn 9417 . . . . . . . . . 10 ((𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ𝑀)) → 𝑁 ∈ ℕ)
52, 3, 4syl2anc 409 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
6 elnnuz 9382 . . . . . . . . 9 (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ‘1))
75, 6sylib 121 . . . . . . . 8 (𝜑𝑁 ∈ (ℤ‘1))
8 elnnuz 9382 . . . . . . . . 9 (𝑘 ∈ ℕ ↔ 𝑘 ∈ (ℤ‘1))
9 cvgcmp2n.cl . . . . . . . . . 10 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℝ)
109recnd 7814 . . . . . . . . 9 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ∈ ℂ)
118, 10sylan2br 286 . . . . . . . 8 ((𝜑𝑘 ∈ (ℤ‘1)) → (𝐺𝑘) ∈ ℂ)
121, 7, 11fsum3ser 11194 . . . . . . 7 (𝜑 → Σ𝑘 ∈ (1...𝑁)(𝐺𝑘) = (seq1( + , 𝐺)‘𝑁))
13 nnuz 9381 . . . . . . . . 9 ℕ = (ℤ‘1)
142, 13eleqtrdi 2233 . . . . . . . 8 (𝜑𝑀 ∈ (ℤ‘1))
151, 14, 11fsum3ser 11194 . . . . . . 7 (𝜑 → Σ𝑘 ∈ (1...𝑀)(𝐺𝑘) = (seq1( + , 𝐺)‘𝑀))
1612, 15oveq12d 5796 . . . . . 6 (𝜑 → (Σ𝑘 ∈ (1...𝑁)(𝐺𝑘) − Σ𝑘 ∈ (1...𝑀)(𝐺𝑘)) = ((seq1( + , 𝐺)‘𝑁) − (seq1( + , 𝐺)‘𝑀)))
172nnred 8753 . . . . . . . . . . 11 (𝜑𝑀 ∈ ℝ)
1817ltp1d 8708 . . . . . . . . . 10 (𝜑𝑀 < (𝑀 + 1))
19 fzdisj 9859 . . . . . . . . . 10 (𝑀 < (𝑀 + 1) → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
2018, 19syl 14 . . . . . . . . 9 (𝜑 → ((1...𝑀) ∩ ((𝑀 + 1)...𝑁)) = ∅)
21 eluzle 9358 . . . . . . . . . . . 12 (𝑁 ∈ (ℤ𝑀) → 𝑀𝑁)
223, 21syl 14 . . . . . . . . . . 11 (𝜑𝑀𝑁)
23 elfz1b 9897 . . . . . . . . . . 11 (𝑀 ∈ (1...𝑁) ↔ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀𝑁))
242, 5, 22, 23syl3anbrc 1166 . . . . . . . . . 10 (𝜑𝑀 ∈ (1...𝑁))
25 fzsplit 9858 . . . . . . . . . 10 (𝑀 ∈ (1...𝑁) → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
2624, 25syl 14 . . . . . . . . 9 (𝜑 → (1...𝑁) = ((1...𝑀) ∪ ((𝑀 + 1)...𝑁)))
27 1zzd 9101 . . . . . . . . . 10 (𝜑 → 1 ∈ ℤ)
285nnzd 9192 . . . . . . . . . 10 (𝜑𝑁 ∈ ℤ)
2927, 28fzfigd 10231 . . . . . . . . 9 (𝜑 → (1...𝑁) ∈ Fin)
30 elfznn 9861 . . . . . . . . . 10 (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ)
3130, 10sylan2 284 . . . . . . . . 9 ((𝜑𝑘 ∈ (1...𝑁)) → (𝐺𝑘) ∈ ℂ)
3220, 26, 29, 31fsumsplit 11204 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ (1...𝑁)(𝐺𝑘) = (Σ𝑘 ∈ (1...𝑀)(𝐺𝑘) + Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐺𝑘)))
3332eqcomd 2146 . . . . . . 7 (𝜑 → (Σ𝑘 ∈ (1...𝑀)(𝐺𝑘) + Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐺𝑘)) = Σ𝑘 ∈ (1...𝑁)(𝐺𝑘))
3429, 31fsumcl 11197 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ (1...𝑁)(𝐺𝑘) ∈ ℂ)
352nnzd 9192 . . . . . . . . . 10 (𝜑𝑀 ∈ ℤ)
3627, 35fzfigd 10231 . . . . . . . . 9 (𝜑 → (1...𝑀) ∈ Fin)
37 elfznn 9861 . . . . . . . . . 10 (𝑘 ∈ (1...𝑀) → 𝑘 ∈ ℕ)
3837, 10sylan2 284 . . . . . . . . 9 ((𝜑𝑘 ∈ (1...𝑀)) → (𝐺𝑘) ∈ ℂ)
3936, 38fsumcl 11197 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ (1...𝑀)(𝐺𝑘) ∈ ℂ)
4035peano2zd 9196 . . . . . . . . . 10 (𝜑 → (𝑀 + 1) ∈ ℤ)
4140, 28fzfigd 10231 . . . . . . . . 9 (𝜑 → ((𝑀 + 1)...𝑁) ∈ Fin)
422peano2nnd 8755 . . . . . . . . . . 11 (𝜑 → (𝑀 + 1) ∈ ℕ)
43 elfzuz 9829 . . . . . . . . . . 11 (𝑘 ∈ ((𝑀 + 1)...𝑁) → 𝑘 ∈ (ℤ‘(𝑀 + 1)))
44 eluznn 9417 . . . . . . . . . . 11 (((𝑀 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ‘(𝑀 + 1))) → 𝑘 ∈ ℕ)
4542, 43, 44syl2an 287 . . . . . . . . . 10 ((𝜑𝑘 ∈ ((𝑀 + 1)...𝑁)) → 𝑘 ∈ ℕ)
4645, 10syldan 280 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)...𝑁)) → (𝐺𝑘) ∈ ℂ)
4741, 46fsumcl 11197 . . . . . . . 8 (𝜑 → Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐺𝑘) ∈ ℂ)
4834, 39, 47subaddd 8111 . . . . . . 7 (𝜑 → ((Σ𝑘 ∈ (1...𝑁)(𝐺𝑘) − Σ𝑘 ∈ (1...𝑀)(𝐺𝑘)) = Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐺𝑘) ↔ (Σ𝑘 ∈ (1...𝑀)(𝐺𝑘) + Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐺𝑘)) = Σ𝑘 ∈ (1...𝑁)(𝐺𝑘)))
4933, 48mpbird 166 . . . . . 6 (𝜑 → (Σ𝑘 ∈ (1...𝑁)(𝐺𝑘) − Σ𝑘 ∈ (1...𝑀)(𝐺𝑘)) = Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐺𝑘))
5016, 49eqtr3d 2175 . . . . 5 (𝜑 → ((seq1( + , 𝐺)‘𝑁) − (seq1( + , 𝐺)‘𝑀)) = Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐺𝑘))
5145, 9syldan 280 . . . . . 6 ((𝜑𝑘 ∈ ((𝑀 + 1)...𝑁)) → (𝐺𝑘) ∈ ℝ)
5241, 51fsumrecl 11198 . . . . 5 (𝜑 → Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐺𝑘) ∈ ℝ)
5350, 52eqeltrd 2217 . . . 4 (𝜑 → ((seq1( + , 𝐺)‘𝑁) − (seq1( + , 𝐺)‘𝑀)) ∈ ℝ)
5442nnzd 9192 . . . . . . 7 (𝜑 → (𝑀 + 1) ∈ ℤ)
5554, 28fzfigd 10231 . . . . . 6 (𝜑 → ((𝑀 + 1)...𝑁) ∈ Fin)
56 cvgcmp2n.ge0 . . . . . . 7 ((𝜑𝑘 ∈ ℕ) → 0 ≤ (𝐺𝑘))
5745, 56syldan 280 . . . . . 6 ((𝜑𝑘 ∈ ((𝑀 + 1)...𝑁)) → 0 ≤ (𝐺𝑘))
5855, 51, 57fsumge0 11256 . . . . 5 (𝜑 → 0 ≤ Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐺𝑘))
5958, 50breqtrrd 3960 . . . 4 (𝜑 → 0 ≤ ((seq1( + , 𝐺)‘𝑁) − (seq1( + , 𝐺)‘𝑀)))
6053, 59absidd 10967 . . 3 (𝜑 → (abs‘((seq1( + , 𝐺)‘𝑁) − (seq1( + , 𝐺)‘𝑀))) = ((seq1( + , 𝐺)‘𝑁) − (seq1( + , 𝐺)‘𝑀)))
6160, 50eqtrd 2173 . 2 (𝜑 → (abs‘((seq1( + , 𝐺)‘𝑁) − (seq1( + , 𝐺)‘𝑀))) = Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐺𝑘))
62 halfre 8953 . . . . . . 7 (1 / 2) ∈ ℝ
6362a1i 9 . . . . . 6 (𝜑 → (1 / 2) ∈ ℝ)
6442nnnn0d 9050 . . . . . 6 (𝜑 → (𝑀 + 1) ∈ ℕ0)
6563, 64reexpcld 10468 . . . . 5 (𝜑 → ((1 / 2)↑(𝑀 + 1)) ∈ ℝ)
665peano2nnd 8755 . . . . . . 7 (𝜑 → (𝑁 + 1) ∈ ℕ)
6766nnnn0d 9050 . . . . . 6 (𝜑 → (𝑁 + 1) ∈ ℕ0)
6863, 67reexpcld 10468 . . . . 5 (𝜑 → ((1 / 2)↑(𝑁 + 1)) ∈ ℝ)
6965, 68resubcld 8163 . . . 4 (𝜑 → (((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) ∈ ℝ)
70 1mhlfehlf 8958 . . . . . 6 (1 − (1 / 2)) = (1 / 2)
71 2rp 9471 . . . . . . 7 2 ∈ ℝ+
72 rpreccl 9493 . . . . . . 7 (2 ∈ ℝ+ → (1 / 2) ∈ ℝ+)
7371, 72ax-mp 5 . . . . . 6 (1 / 2) ∈ ℝ+
7470, 73eqeltri 2213 . . . . 5 (1 − (1 / 2)) ∈ ℝ+
7574a1i 9 . . . 4 (𝜑 → (1 − (1 / 2)) ∈ ℝ+)
7669, 75rerpdivcld 9541 . . 3 (𝜑 → ((((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) / (1 − (1 / 2))) ∈ ℝ)
7771a1i 9 . . . . 5 (𝜑 → 2 ∈ ℝ+)
782nnrpd 9507 . . . . 5 (𝜑𝑀 ∈ ℝ+)
7977, 78rpdivcld 9527 . . . 4 (𝜑 → (2 / 𝑀) ∈ ℝ+)
8079rpred 9509 . . 3 (𝜑 → (2 / 𝑀) ∈ ℝ)
8171a1i 9 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)...𝑁)) → 2 ∈ ℝ+)
8245nnzd 9192 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)...𝑁)) → 𝑘 ∈ ℤ)
8381, 82rpexpcld 10475 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝑀 + 1)...𝑁)) → (2↑𝑘) ∈ ℝ+)
8483rprecred 9521 . . . . . . 7 ((𝜑𝑘 ∈ ((𝑀 + 1)...𝑁)) → (1 / (2↑𝑘)) ∈ ℝ)
85 cvgcmp2n.lt . . . . . . . 8 ((𝜑𝑘 ∈ ℕ) → (𝐺𝑘) ≤ (1 / (2↑𝑘)))
8645, 85syldan 280 . . . . . . 7 ((𝜑𝑘 ∈ ((𝑀 + 1)...𝑁)) → (𝐺𝑘) ≤ (1 / (2↑𝑘)))
8741, 51, 84, 86fsumle 11260 . . . . . 6 (𝜑 → Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐺𝑘) ≤ Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(1 / (2↑𝑘)))
88 2cnd 8813 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)...𝑁)) → 2 ∈ ℂ)
8981rpap0d 9515 . . . . . . . . 9 ((𝜑𝑘 ∈ ((𝑀 + 1)...𝑁)) → 2 # 0)
9088, 89, 82exprecapd 10459 . . . . . . . 8 ((𝜑𝑘 ∈ ((𝑀 + 1)...𝑁)) → ((1 / 2)↑𝑘) = (1 / (2↑𝑘)))
9190eqcomd 2146 . . . . . . 7 ((𝜑𝑘 ∈ ((𝑀 + 1)...𝑁)) → (1 / (2↑𝑘)) = ((1 / 2)↑𝑘))
9291sumeq2dv 11165 . . . . . 6 (𝜑 → Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(1 / (2↑𝑘)) = Σ𝑘 ∈ ((𝑀 + 1)...𝑁)((1 / 2)↑𝑘))
9387, 92breqtrd 3958 . . . . 5 (𝜑 → Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐺𝑘) ≤ Σ𝑘 ∈ ((𝑀 + 1)...𝑁)((1 / 2)↑𝑘))
94 fzval3 10008 . . . . . . 7 (𝑁 ∈ ℤ → ((𝑀 + 1)...𝑁) = ((𝑀 + 1)..^(𝑁 + 1)))
9528, 94syl 14 . . . . . 6 (𝜑 → ((𝑀 + 1)...𝑁) = ((𝑀 + 1)..^(𝑁 + 1)))
9695sumeq1d 11163 . . . . 5 (𝜑 → Σ𝑘 ∈ ((𝑀 + 1)...𝑁)((1 / 2)↑𝑘) = Σ𝑘 ∈ ((𝑀 + 1)..^(𝑁 + 1))((1 / 2)↑𝑘))
9793, 96breqtrd 3958 . . . 4 (𝜑 → Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐺𝑘) ≤ Σ𝑘 ∈ ((𝑀 + 1)..^(𝑁 + 1))((1 / 2)↑𝑘))
98 halfcn 8954 . . . . . 6 (1 / 2) ∈ ℂ
9998a1i 9 . . . . 5 (𝜑 → (1 / 2) ∈ ℂ)
100 1re 7785 . . . . . . 7 1 ∈ ℝ
101 halflt1 8957 . . . . . . 7 (1 / 2) < 1
10262, 100, 101ltapii 8417 . . . . . 6 (1 / 2) # 1
103102a1i 9 . . . . 5 (𝜑 → (1 / 2) # 1)
104 eluzp1p1 9371 . . . . . 6 (𝑁 ∈ (ℤ𝑀) → (𝑁 + 1) ∈ (ℤ‘(𝑀 + 1)))
1053, 104syl 14 . . . . 5 (𝜑 → (𝑁 + 1) ∈ (ℤ‘(𝑀 + 1)))
10699, 103, 64, 105geosergap 11303 . . . 4 (𝜑 → Σ𝑘 ∈ ((𝑀 + 1)..^(𝑁 + 1))((1 / 2)↑𝑘) = ((((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) / (1 − (1 / 2))))
10797, 106breqtrd 3958 . . 3 (𝜑 → Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐺𝑘) ≤ ((((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) / (1 − (1 / 2))))
10873a1i 9 . . . . . . . 8 (𝜑 → (1 / 2) ∈ ℝ+)
10928peano2zd 9196 . . . . . . . 8 (𝜑 → (𝑁 + 1) ∈ ℤ)
110108, 109rpexpcld 10475 . . . . . . 7 (𝜑 → ((1 / 2)↑(𝑁 + 1)) ∈ ℝ+)
111110rpred 9509 . . . . . 6 (𝜑 → ((1 / 2)↑(𝑁 + 1)) ∈ ℝ)
11265, 111resubcld 8163 . . . . 5 (𝜑 → (((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) ∈ ℝ)
1132nnrecred 8787 . . . . 5 (𝜑 → (1 / 𝑀) ∈ ℝ)
11465, 110ltsubrpd 9542 . . . . . 6 (𝜑 → (((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) < ((1 / 2)↑(𝑀 + 1)))
115 2cnd 8813 . . . . . . . 8 (𝜑 → 2 ∈ ℂ)
11677rpap0d 9515 . . . . . . . 8 (𝜑 → 2 # 0)
117115, 116, 40exprecapd 10459 . . . . . . 7 (𝜑 → ((1 / 2)↑(𝑀 + 1)) = (1 / (2↑(𝑀 + 1))))
11842nnred 8753 . . . . . . . . 9 (𝜑 → (𝑀 + 1) ∈ ℝ)
11977, 40rpexpcld 10475 . . . . . . . . . 10 (𝜑 → (2↑(𝑀 + 1)) ∈ ℝ+)
120119rpred 9509 . . . . . . . . 9 (𝜑 → (2↑(𝑀 + 1)) ∈ ℝ)
121 2z 9102 . . . . . . . . . . . 12 2 ∈ ℤ
122 uzid 9360 . . . . . . . . . . . 12 (2 ∈ ℤ → 2 ∈ (ℤ‘2))
123121, 122ax-mp 5 . . . . . . . . . . 11 2 ∈ (ℤ‘2)
124123a1i 9 . . . . . . . . . 10 (𝜑 → 2 ∈ (ℤ‘2))
125 bernneq3 10441 . . . . . . . . . 10 ((2 ∈ (ℤ‘2) ∧ (𝑀 + 1) ∈ ℕ0) → (𝑀 + 1) < (2↑(𝑀 + 1)))
126124, 64, 125syl2anc 409 . . . . . . . . 9 (𝜑 → (𝑀 + 1) < (2↑(𝑀 + 1)))
12717, 118, 120, 18, 126lttrd 7908 . . . . . . . 8 (𝜑𝑀 < (2↑(𝑀 + 1)))
12878, 119ltrecd 9528 . . . . . . . 8 (𝜑 → (𝑀 < (2↑(𝑀 + 1)) ↔ (1 / (2↑(𝑀 + 1))) < (1 / 𝑀)))
129127, 128mpbid 146 . . . . . . 7 (𝜑 → (1 / (2↑(𝑀 + 1))) < (1 / 𝑀))
130117, 129eqbrtrd 3954 . . . . . 6 (𝜑 → ((1 / 2)↑(𝑀 + 1)) < (1 / 𝑀))
131112, 65, 113, 114, 130lttrd 7908 . . . . 5 (𝜑 → (((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) < (1 / 𝑀))
132112, 113, 77, 131ltmul1dd 9565 . . . 4 (𝜑 → ((((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) · 2) < ((1 / 𝑀) · 2))
13370oveq2i 5789 . . . . . 6 ((((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) / (1 − (1 / 2))) = ((((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) / (1 / 2))
134112recnd 7814 . . . . . . 7 (𝜑 → (((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) ∈ ℂ)
135 1cnd 7802 . . . . . . 7 (𝜑 → 1 ∈ ℂ)
136 1ap0 8372 . . . . . . . 8 1 # 0
137136a1i 9 . . . . . . 7 (𝜑 → 1 # 0)
138134, 135, 115, 137, 116divdivap2d 8603 . . . . . 6 (𝜑 → ((((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) / (1 / 2)) = (((((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) · 2) / 1))
139133, 138syl5eq 2185 . . . . 5 (𝜑 → ((((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) / (1 − (1 / 2))) = (((((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) · 2) / 1))
140134, 115mulcld 7806 . . . . . 6 (𝜑 → ((((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) · 2) ∈ ℂ)
141140div1d 8560 . . . . 5 (𝜑 → (((((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) · 2) / 1) = ((((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) · 2))
142139, 141eqtrd 2173 . . . 4 (𝜑 → ((((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) / (1 − (1 / 2))) = ((((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) · 2))
14317recnd 7814 . . . . 5 (𝜑𝑀 ∈ ℂ)
1442nnap0d 8786 . . . . 5 (𝜑𝑀 # 0)
145115, 143, 144divrecap2d 8574 . . . 4 (𝜑 → (2 / 𝑀) = ((1 / 𝑀) · 2))
146132, 142, 1453brtr4d 3964 . . 3 (𝜑 → ((((1 / 2)↑(𝑀 + 1)) − ((1 / 2)↑(𝑁 + 1))) / (1 − (1 / 2))) < (2 / 𝑀))
14752, 76, 80, 107, 146lelttrd 7907 . 2 (𝜑 → Σ𝑘 ∈ ((𝑀 + 1)...𝑁)(𝐺𝑘) < (2 / 𝑀))
14861, 147eqbrtrd 3954 1 (𝜑 → (abs‘((seq1( + , 𝐺)‘𝑁) − (seq1( + , 𝐺)‘𝑀))) < (2 / 𝑀))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1332   ∈ wcel 1481   ∪ cun 3070   ∩ cin 3071  ∅c0 3364   class class class wbr 3933  ‘cfv 5127  (class class class)co 5778  ℂcc 7638  ℝcr 7639  0cc0 7640  1c1 7641   + caddc 7643   · cmul 7645   < clt 7820   ≤ cle 7821   − cmin 7953   # cap 8363   / cdiv 8452  ℕcn 8740  2c2 8791  ℕ0cn0 8997  ℤcz 9074  ℤ≥cuz 9346  ℝ+crp 9466  ...cfz 9817  ..^cfzo 9946  seqcseq 10245  ↑cexp 10319  abscabs 10797  Σcsu 11150 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4047  ax-sep 4050  ax-nul 4058  ax-pow 4102  ax-pr 4135  ax-un 4359  ax-setind 4456  ax-iinf 4506  ax-cnex 7731  ax-resscn 7732  ax-1cn 7733  ax-1re 7734  ax-icn 7735  ax-addcl 7736  ax-addrcl 7737  ax-mulcl 7738  ax-mulrcl 7739  ax-addcom 7740  ax-mulcom 7741  ax-addass 7742  ax-mulass 7743  ax-distr 7744  ax-i2m1 7745  ax-0lt1 7746  ax-1rid 7747  ax-0id 7748  ax-rnegex 7749  ax-precex 7750  ax-cnre 7751  ax-pre-ltirr 7752  ax-pre-ltwlin 7753  ax-pre-lttrn 7754  ax-pre-apti 7755  ax-pre-ltadd 7756  ax-pre-mulgt0 7757  ax-pre-mulext 7758  ax-arch 7759  ax-caucvg 7760 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rmo 2425  df-rab 2426  df-v 2689  df-sbc 2911  df-csb 3005  df-dif 3074  df-un 3076  df-in 3078  df-ss 3085  df-nul 3365  df-if 3476  df-pw 3513  df-sn 3534  df-pr 3535  df-op 3537  df-uni 3741  df-int 3776  df-iun 3819  df-br 3934  df-opab 3994  df-mpt 3995  df-tr 4031  df-id 4219  df-po 4222  df-iso 4223  df-iord 4292  df-on 4294  df-ilim 4295  df-suc 4297  df-iom 4509  df-xp 4549  df-rel 4550  df-cnv 4551  df-co 4552  df-dm 4553  df-rn 4554  df-res 4555  df-ima 4556  df-iota 5092  df-fun 5129  df-fn 5130  df-f 5131  df-f1 5132  df-fo 5133  df-f1o 5134  df-fv 5135  df-isom 5136  df-riota 5734  df-ov 5781  df-oprab 5782  df-mpo 5783  df-1st 6042  df-2nd 6043  df-recs 6206  df-irdg 6271  df-frec 6292  df-1o 6317  df-oadd 6321  df-er 6433  df-en 6639  df-dom 6640  df-fin 6641  df-pnf 7822  df-mnf 7823  df-xr 7824  df-ltxr 7825  df-le 7826  df-sub 7955  df-neg 7956  df-reap 8357  df-ap 8364  df-div 8453  df-inn 8741  df-2 8799  df-3 8800  df-4 8801  df-n0 8998  df-z 9075  df-uz 9347  df-q 9435  df-rp 9467  df-ico 9703  df-fz 9818  df-fzo 9947  df-seqfrec 10246  df-exp 10320  df-ihash 10550  df-cj 10642  df-re 10643  df-im 10644  df-rsqrt 10798  df-abs 10799  df-clim 11076  df-sumdc 11151 This theorem is referenced by:  cvgcmp2n  13386
 Copyright terms: Public domain W3C validator