Step | Hyp | Ref
| Expression |
1 | | nnuz 9493 |
. . . . . . 7
⊢ ℕ =
(ℤ≥‘1) |
2 | | 1zzd 9210 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) |
3 | | cvgratnn.6 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) |
4 | 1, 2, 3 | serf 10400 |
. . . . . 6
⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ) |
5 | | cvgratnnlemrate.m |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℕ) |
6 | | cvgratnnlemrate.n |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
7 | | eluznn 9530 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ ∧ 𝑁 ∈
(ℤ≥‘𝑀)) → 𝑁 ∈ ℕ) |
8 | 5, 6, 7 | syl2anc 409 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
9 | 4, 8 | ffvelrnd 5616 |
. . . . 5
⊢ (𝜑 → (seq1( + , 𝐹)‘𝑁) ∈ ℂ) |
10 | 4, 5 | ffvelrnd 5616 |
. . . . 5
⊢ (𝜑 → (seq1( + , 𝐹)‘𝑀) ∈ ℂ) |
11 | 9, 10 | subcld 8201 |
. . . 4
⊢ (𝜑 → ((seq1( + , 𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀)) ∈ ℂ) |
12 | 11 | abscld 11113 |
. . 3
⊢ (𝜑 → (abs‘((seq1( + ,
𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀))) ∈ ℝ) |
13 | | fveq2 5481 |
. . . . . . 7
⊢ (𝑘 = 𝑀 → (𝐹‘𝑘) = (𝐹‘𝑀)) |
14 | 13 | eleq1d 2233 |
. . . . . 6
⊢ (𝑘 = 𝑀 → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘𝑀) ∈ ℂ)) |
15 | 3 | ralrimiva 2537 |
. . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝐹‘𝑘) ∈ ℂ) |
16 | 14, 15, 5 | rspcdva 2831 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑀) ∈ ℂ) |
17 | 16 | abscld 11113 |
. . . 4
⊢ (𝜑 → (abs‘(𝐹‘𝑀)) ∈ ℝ) |
18 | 5 | nnzd 9304 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ ℤ) |
19 | 18 | peano2zd 9308 |
. . . . . 6
⊢ (𝜑 → (𝑀 + 1) ∈ ℤ) |
20 | | eluzelz 9467 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
21 | 6, 20 | syl 14 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
22 | 19, 21 | fzfigd 10357 |
. . . . 5
⊢ (𝜑 → ((𝑀 + 1)...𝑁) ∈ Fin) |
23 | | cvgratnn.3 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
24 | 23 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝐴 ∈ ℝ) |
25 | 5 | nnred 8862 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℝ) |
26 | 25 | adantr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 ∈ ℝ) |
27 | | peano2re 8026 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℝ → (𝑀 + 1) ∈
ℝ) |
28 | 26, 27 | syl 14 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 + 1) ∈ ℝ) |
29 | | elfzelz 9952 |
. . . . . . . . . 10
⊢ (𝑖 ∈ ((𝑀 + 1)...𝑁) → 𝑖 ∈ ℤ) |
30 | 29 | adantl 275 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ ℤ) |
31 | 30 | zred 9305 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑖 ∈ ℝ) |
32 | 26 | lep1d 8818 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 ≤ (𝑀 + 1)) |
33 | | elfzle1 9953 |
. . . . . . . . 9
⊢ (𝑖 ∈ ((𝑀 + 1)...𝑁) → (𝑀 + 1) ≤ 𝑖) |
34 | 33 | adantl 275 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 + 1) ≤ 𝑖) |
35 | 26, 28, 31, 32, 34 | letrd 8014 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝑀 ≤ 𝑖) |
36 | | znn0sub 9248 |
. . . . . . . 8
⊢ ((𝑀 ∈ ℤ ∧ 𝑖 ∈ ℤ) → (𝑀 ≤ 𝑖 ↔ (𝑖 − 𝑀) ∈
ℕ0)) |
37 | 18, 29, 36 | syl2an 287 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑀 ≤ 𝑖 ↔ (𝑖 − 𝑀) ∈
ℕ0)) |
38 | 35, 37 | mpbid 146 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑖 − 𝑀) ∈
ℕ0) |
39 | 24, 38 | reexpcld 10595 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝐴↑(𝑖 − 𝑀)) ∈ ℝ) |
40 | 22, 39 | fsumrecl 11332 |
. . . 4
⊢ (𝜑 → Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐴↑(𝑖 − 𝑀)) ∈ ℝ) |
41 | 17, 40 | remulcld 7921 |
. . 3
⊢ (𝜑 → ((abs‘(𝐹‘𝑀)) · Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐴↑(𝑖 − 𝑀))) ∈ ℝ) |
42 | | cvgratnn.4 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 < 1) |
43 | | cvgratnn.gt0 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < 𝐴) |
44 | 23, 43 | elrpd 9621 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
45 | 44 | reclt1d 9638 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 < 1 ↔ 1 < (1 / 𝐴))) |
46 | 42, 45 | mpbid 146 |
. . . . . . . . . 10
⊢ (𝜑 → 1 < (1 / 𝐴)) |
47 | | 1re 7890 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
48 | 44 | rprecred 9636 |
. . . . . . . . . . 11
⊢ (𝜑 → (1 / 𝐴) ∈ ℝ) |
49 | | difrp 9620 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ (1 / 𝐴) ∈ ℝ) → (1 < (1 / 𝐴) ↔ ((1 / 𝐴) − 1) ∈
ℝ+)) |
50 | 47, 48, 49 | sylancr 411 |
. . . . . . . . . 10
⊢ (𝜑 → (1 < (1 / 𝐴) ↔ ((1 / 𝐴) − 1) ∈
ℝ+)) |
51 | 46, 50 | mpbid 146 |
. . . . . . . . 9
⊢ (𝜑 → ((1 / 𝐴) − 1) ∈
ℝ+) |
52 | 51 | rpreccld 9635 |
. . . . . . . 8
⊢ (𝜑 → (1 / ((1 / 𝐴) − 1)) ∈
ℝ+) |
53 | 52, 44 | rpdivcld 9642 |
. . . . . . 7
⊢ (𝜑 → ((1 / ((1 / 𝐴) − 1)) / 𝐴) ∈
ℝ+) |
54 | | fveq2 5481 |
. . . . . . . . . . 11
⊢ (𝑘 = 1 → (𝐹‘𝑘) = (𝐹‘1)) |
55 | 54 | eleq1d 2233 |
. . . . . . . . . 10
⊢ (𝑘 = 1 → ((𝐹‘𝑘) ∈ ℂ ↔ (𝐹‘1) ∈ ℂ)) |
56 | | 1nn 8860 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
57 | 56 | a1i 9 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ∈
ℕ) |
58 | 55, 15, 57 | rspcdva 2831 |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘1) ∈ ℂ) |
59 | 58 | abscld 11113 |
. . . . . . . 8
⊢ (𝜑 → (abs‘(𝐹‘1)) ∈
ℝ) |
60 | 58 | absge0d 11116 |
. . . . . . . 8
⊢ (𝜑 → 0 ≤ (abs‘(𝐹‘1))) |
61 | 59, 60 | ge0p1rpd 9655 |
. . . . . . 7
⊢ (𝜑 → ((abs‘(𝐹‘1)) + 1) ∈
ℝ+) |
62 | 53, 61 | rpmulcld 9641 |
. . . . . 6
⊢ (𝜑 → (((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) ∈
ℝ+) |
63 | 62 | rpred 9624 |
. . . . 5
⊢ (𝜑 → (((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) ∈
ℝ) |
64 | 63, 5 | nndivred 8899 |
. . . 4
⊢ (𝜑 → ((((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) / 𝑀) ∈
ℝ) |
65 | | 1red 7906 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℝ) |
66 | 65, 23 | resubcld 8271 |
. . . . . . 7
⊢ (𝜑 → (1 − 𝐴) ∈
ℝ) |
67 | 23, 65 | posdifd 8422 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 < 1 ↔ 0 < (1 − 𝐴))) |
68 | 42, 67 | mpbid 146 |
. . . . . . 7
⊢ (𝜑 → 0 < (1 − 𝐴)) |
69 | 66, 68 | elrpd 9621 |
. . . . . 6
⊢ (𝜑 → (1 − 𝐴) ∈
ℝ+) |
70 | 44, 69 | rpdivcld 9642 |
. . . . 5
⊢ (𝜑 → (𝐴 / (1 − 𝐴)) ∈
ℝ+) |
71 | 70 | rpred 9624 |
. . . 4
⊢ (𝜑 → (𝐴 / (1 − 𝐴)) ∈ ℝ) |
72 | 64, 71 | remulcld 7921 |
. . 3
⊢ (𝜑 → (((((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) / 𝑀) · (𝐴 / (1 − 𝐴))) ∈ ℝ) |
73 | | cvgratnn.7 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (abs‘(𝐹‘(𝑘 + 1))) ≤ (𝐴 · (abs‘(𝐹‘𝑘)))) |
74 | 23, 42, 43, 3, 73, 5, 6 | cvgratnnlemseq 11457 |
. . . . 5
⊢ (𝜑 → ((seq1( + , 𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀)) = Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐹‘𝑖)) |
75 | 74 | fveq2d 5485 |
. . . 4
⊢ (𝜑 → (abs‘((seq1( + ,
𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀))) = (abs‘Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐹‘𝑖))) |
76 | 23, 42, 43, 3, 73, 5, 6 | cvgratnnlemabsle 11458 |
. . . 4
⊢ (𝜑 → (abs‘Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐹‘𝑖)) ≤ ((abs‘(𝐹‘𝑀)) · Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐴↑(𝑖 − 𝑀)))) |
77 | 75, 76 | eqbrtrd 3999 |
. . 3
⊢ (𝜑 → (abs‘((seq1( + ,
𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀))) ≤ ((abs‘(𝐹‘𝑀)) · Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐴↑(𝑖 − 𝑀)))) |
78 | 16 | absge0d 11116 |
. . . 4
⊢ (𝜑 → 0 ≤ (abs‘(𝐹‘𝑀))) |
79 | 23, 42, 43, 3, 73, 5 | cvgratnnlemfm 11460 |
. . . 4
⊢ (𝜑 → (abs‘(𝐹‘𝑀)) < ((((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) / 𝑀)) |
80 | 44 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 𝐴 ∈
ℝ+) |
81 | 38 | nn0zd 9303 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝑖 − 𝑀) ∈ ℤ) |
82 | 80, 81 | rpexpcld 10602 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → (𝐴↑(𝑖 − 𝑀)) ∈
ℝ+) |
83 | 82 | rpge0d 9628 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ((𝑀 + 1)...𝑁)) → 0 ≤ (𝐴↑(𝑖 − 𝑀))) |
84 | 22, 39, 83 | fsumge0 11390 |
. . . 4
⊢ (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐴↑(𝑖 − 𝑀))) |
85 | 23, 42, 43, 3, 73, 5, 6 | cvgratnnlemsumlt 11459 |
. . . 4
⊢ (𝜑 → Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐴↑(𝑖 − 𝑀)) < (𝐴 / (1 − 𝐴))) |
86 | 17, 64, 40, 71, 78, 79, 84, 85 | ltmul12ad 8828 |
. . 3
⊢ (𝜑 → ((abs‘(𝐹‘𝑀)) · Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐴↑(𝑖 − 𝑀))) < (((((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) / 𝑀) · (𝐴 / (1 − 𝐴)))) |
87 | 12, 41, 72, 77, 86 | lelttrd 8015 |
. 2
⊢ (𝜑 → (abs‘((seq1( + ,
𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀))) < (((((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) / 𝑀) · (𝐴 / (1 − 𝐴)))) |
88 | 63 | recnd 7919 |
. . 3
⊢ (𝜑 → (((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) ∈
ℂ) |
89 | 71 | recnd 7919 |
. . 3
⊢ (𝜑 → (𝐴 / (1 − 𝐴)) ∈ ℂ) |
90 | 5 | nncnd 8863 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℂ) |
91 | 5 | nnap0d 8895 |
. . 3
⊢ (𝜑 → 𝑀 # 0) |
92 | 88, 89, 90, 91 | div23apd 8716 |
. 2
⊢ (𝜑 → (((((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) · (𝐴 / (1 − 𝐴))) / 𝑀) = (((((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) / 𝑀) · (𝐴 / (1 − 𝐴)))) |
93 | 87, 92 | breqtrrd 4005 |
1
⊢ (𝜑 → (abs‘((seq1( + ,
𝐹)‘𝑁) − (seq1( + , 𝐹)‘𝑀))) < (((((1 / ((1 / 𝐴) − 1)) / 𝐴) · ((abs‘(𝐹‘1)) + 1)) · (𝐴 / (1 − 𝐴))) / 𝑀)) |