Proof of Theorem cvgratnnlemsumlt
Step | Hyp | Ref
| Expression |
1 | | cvgratnn.m |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℕ) |
2 | 1 | nnzd 9392 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℤ) |
3 | | 1zzd 9298 |
. . . 4
⊢ (𝜑 → 1 ∈
ℤ) |
4 | | cvgratnn.n |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
5 | | eluzelz 9555 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑁 ∈ ℤ) |
6 | 4, 5 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℤ) |
7 | 6, 2 | zsubcld 9398 |
. . . 4
⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℤ) |
8 | | cvgratnn.3 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
9 | 8 | recnd 8004 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
10 | 9 | adantr 276 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 𝑀))) → 𝐴 ∈ ℂ) |
11 | | elfznn 10072 |
. . . . . . 7
⊢ (𝑘 ∈ (1...(𝑁 − 𝑀)) → 𝑘 ∈ ℕ) |
12 | 11 | adantl 277 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 𝑀))) → 𝑘 ∈ ℕ) |
13 | 12 | nnnn0d 9247 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 𝑀))) → 𝑘 ∈ ℕ0) |
14 | 10, 13 | expcld 10672 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (1...(𝑁 − 𝑀))) → (𝐴↑𝑘) ∈ ℂ) |
15 | | oveq2 5899 |
. . . 4
⊢ (𝑘 = (𝑖 − 𝑀) → (𝐴↑𝑘) = (𝐴↑(𝑖 − 𝑀))) |
16 | 2, 3, 7, 14, 15 | fsumshft 11470 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (1...(𝑁 − 𝑀))(𝐴↑𝑘) = Σ𝑖 ∈ ((1 + 𝑀)...((𝑁 − 𝑀) + 𝑀))(𝐴↑(𝑖 − 𝑀))) |
17 | | 1cnd 7991 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℂ) |
18 | 1 | nncnd 8951 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ ℂ) |
19 | 17, 18 | addcomd 8126 |
. . . . 5
⊢ (𝜑 → (1 + 𝑀) = (𝑀 + 1)) |
20 | 6 | zcnd 9394 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℂ) |
21 | 20, 18 | npcand 8290 |
. . . . 5
⊢ (𝜑 → ((𝑁 − 𝑀) + 𝑀) = 𝑁) |
22 | 19, 21 | oveq12d 5909 |
. . . 4
⊢ (𝜑 → ((1 + 𝑀)...((𝑁 − 𝑀) + 𝑀)) = ((𝑀 + 1)...𝑁)) |
23 | 22 | sumeq1d 11392 |
. . 3
⊢ (𝜑 → Σ𝑖 ∈ ((1 + 𝑀)...((𝑁 − 𝑀) + 𝑀))(𝐴↑(𝑖 − 𝑀)) = Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐴↑(𝑖 − 𝑀))) |
24 | 16, 23 | eqtrd 2222 |
. 2
⊢ (𝜑 → Σ𝑘 ∈ (1...(𝑁 − 𝑀))(𝐴↑𝑘) = Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐴↑(𝑖 − 𝑀))) |
25 | | fzval3 10222 |
. . . . 5
⊢ ((𝑁 − 𝑀) ∈ ℤ → (1...(𝑁 − 𝑀)) = (1..^((𝑁 − 𝑀) + 1))) |
26 | 25 | sumeq1d 11392 |
. . . 4
⊢ ((𝑁 − 𝑀) ∈ ℤ → Σ𝑘 ∈ (1...(𝑁 − 𝑀))(𝐴↑𝑘) = Σ𝑘 ∈ (1..^((𝑁 − 𝑀) + 1))(𝐴↑𝑘)) |
27 | 7, 26 | syl 14 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (1...(𝑁 − 𝑀))(𝐴↑𝑘) = Σ𝑘 ∈ (1..^((𝑁 − 𝑀) + 1))(𝐴↑𝑘)) |
28 | | 1red 7990 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
29 | | cvgratnn.4 |
. . . . . 6
⊢ (𝜑 → 𝐴 < 1) |
30 | 8, 28, 29 | ltapd 8613 |
. . . . 5
⊢ (𝜑 → 𝐴 # 1) |
31 | | 1nn0 9210 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
32 | 31 | a1i 9 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℕ0) |
33 | 7 | peano2zd 9396 |
. . . . . 6
⊢ (𝜑 → ((𝑁 − 𝑀) + 1) ∈ ℤ) |
34 | | eluzle 9558 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑁) |
35 | 4, 34 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ≤ 𝑁) |
36 | 6 | zred 9393 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℝ) |
37 | 1 | nnred 8950 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℝ) |
38 | 36, 37 | subge0d 8510 |
. . . . . . . 8
⊢ (𝜑 → (0 ≤ (𝑁 − 𝑀) ↔ 𝑀 ≤ 𝑁)) |
39 | 35, 38 | mpbird 167 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (𝑁 − 𝑀)) |
40 | 7 | zred 9393 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 − 𝑀) ∈ ℝ) |
41 | 28, 40 | addge02d 8509 |
. . . . . . 7
⊢ (𝜑 → (0 ≤ (𝑁 − 𝑀) ↔ 1 ≤ ((𝑁 − 𝑀) + 1))) |
42 | 39, 41 | mpbid 147 |
. . . . . 6
⊢ (𝜑 → 1 ≤ ((𝑁 − 𝑀) + 1)) |
43 | | eluz2 9552 |
. . . . . 6
⊢ (((𝑁 − 𝑀) + 1) ∈
(ℤ≥‘1) ↔ (1 ∈ ℤ ∧ ((𝑁 − 𝑀) + 1) ∈ ℤ ∧ 1 ≤ ((𝑁 − 𝑀) + 1))) |
44 | 3, 33, 42, 43 | syl3anbrc 1183 |
. . . . 5
⊢ (𝜑 → ((𝑁 − 𝑀) + 1) ∈
(ℤ≥‘1)) |
45 | 9, 30, 32, 44 | geosergap 11532 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (1..^((𝑁 − 𝑀) + 1))(𝐴↑𝑘) = (((𝐴↑1) − (𝐴↑((𝑁 − 𝑀) + 1))) / (1 − 𝐴))) |
46 | 9 | exp1d 10667 |
. . . . . . 7
⊢ (𝜑 → (𝐴↑1) = 𝐴) |
47 | 46, 8 | eqeltrd 2266 |
. . . . . 6
⊢ (𝜑 → (𝐴↑1) ∈ ℝ) |
48 | | cvgratnn.gt0 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 𝐴) |
49 | 8, 48 | elrpd 9711 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
50 | 49, 33 | rpexpcld 10696 |
. . . . . . 7
⊢ (𝜑 → (𝐴↑((𝑁 − 𝑀) + 1)) ∈
ℝ+) |
51 | 50 | rpred 9714 |
. . . . . 6
⊢ (𝜑 → (𝐴↑((𝑁 − 𝑀) + 1)) ∈ ℝ) |
52 | 47, 51 | resubcld 8356 |
. . . . 5
⊢ (𝜑 → ((𝐴↑1) − (𝐴↑((𝑁 − 𝑀) + 1))) ∈ ℝ) |
53 | 28, 8 | resubcld 8356 |
. . . . . 6
⊢ (𝜑 → (1 − 𝐴) ∈
ℝ) |
54 | 8, 28 | posdifd 8507 |
. . . . . . 7
⊢ (𝜑 → (𝐴 < 1 ↔ 0 < (1 − 𝐴))) |
55 | 29, 54 | mpbid 147 |
. . . . . 6
⊢ (𝜑 → 0 < (1 − 𝐴)) |
56 | 53, 55 | elrpd 9711 |
. . . . 5
⊢ (𝜑 → (1 − 𝐴) ∈
ℝ+) |
57 | 46 | oveq1d 5906 |
. . . . . 6
⊢ (𝜑 → ((𝐴↑1) − (𝐴↑((𝑁 − 𝑀) + 1))) = (𝐴 − (𝐴↑((𝑁 − 𝑀) + 1)))) |
58 | 8, 50 | ltsubrpd 9747 |
. . . . . 6
⊢ (𝜑 → (𝐴 − (𝐴↑((𝑁 − 𝑀) + 1))) < 𝐴) |
59 | 57, 58 | eqbrtrd 4040 |
. . . . 5
⊢ (𝜑 → ((𝐴↑1) − (𝐴↑((𝑁 − 𝑀) + 1))) < 𝐴) |
60 | 52, 8, 56, 59 | ltdiv1dd 9772 |
. . . 4
⊢ (𝜑 → (((𝐴↑1) − (𝐴↑((𝑁 − 𝑀) + 1))) / (1 − 𝐴)) < (𝐴 / (1 − 𝐴))) |
61 | 45, 60 | eqbrtrd 4040 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (1..^((𝑁 − 𝑀) + 1))(𝐴↑𝑘) < (𝐴 / (1 − 𝐴))) |
62 | 27, 61 | eqbrtrd 4040 |
. 2
⊢ (𝜑 → Σ𝑘 ∈ (1...(𝑁 − 𝑀))(𝐴↑𝑘) < (𝐴 / (1 − 𝐴))) |
63 | 24, 62 | eqbrtrrd 4042 |
1
⊢ (𝜑 → Σ𝑖 ∈ ((𝑀 + 1)...𝑁)(𝐴↑(𝑖 − 𝑀)) < (𝐴 / (1 − 𝐴))) |