Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . 3
⊢
(ℤ≥‘𝑀) = (ℤ≥‘𝑀) |
2 | | geolim2.3 |
. . . 4
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
3 | 2 | nn0zd 12280 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℤ) |
4 | | geolim2.4 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐹‘𝑘) = (𝐴↑𝑘)) |
5 | | geolim.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℂ) |
6 | 5 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝐴 ∈ ℂ) |
7 | | eluznn0 12513 |
. . . . 5
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0) |
8 | 2, 7 | sylan 583 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0) |
9 | 6, 8 | expcld 13716 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → (𝐴↑𝑘) ∈ ℂ) |
10 | | oveq2 7221 |
. . . . . . . 8
⊢ (𝑛 = 𝑘 → (𝐴↑𝑛) = (𝐴↑𝑘)) |
11 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ (𝐴↑𝑛)) = (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) |
12 | | ovex 7246 |
. . . . . . . 8
⊢ (𝐴↑𝑘) ∈ V |
13 | 10, 11, 12 | fvmpt 6818 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ (𝐴↑𝑛))‘𝑘) = (𝐴↑𝑘)) |
14 | 8, 13 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))‘𝑘) = (𝐴↑𝑘)) |
15 | 14, 4 | eqtr4d 2780 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘𝑀)) → ((𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))‘𝑘) = (𝐹‘𝑘)) |
16 | 3, 15 | seqfeq 13601 |
. . . 4
⊢ (𝜑 → seq𝑀( + , (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))) = seq𝑀( + , 𝐹)) |
17 | | geolim.2 |
. . . . . . 7
⊢ (𝜑 → (abs‘𝐴) < 1) |
18 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑛 = 𝑗 → (𝐴↑𝑛) = (𝐴↑𝑗)) |
19 | | ovex 7246 |
. . . . . . . . 9
⊢ (𝐴↑𝑗) ∈ V |
20 | 18, 11, 19 | fvmpt 6818 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ (𝐴↑𝑛))‘𝑗) = (𝐴↑𝑗)) |
21 | 20 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐴↑𝑛))‘𝑗) = (𝐴↑𝑗)) |
22 | 5, 17, 21 | geolim 15434 |
. . . . . 6
⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0
↦ (𝐴↑𝑛))) ⇝ (1 / (1 −
𝐴))) |
23 | | seqex 13576 |
. . . . . . 7
⊢ seq0( + ,
(𝑛 ∈
ℕ0 ↦ (𝐴↑𝑛))) ∈ V |
24 | | ovex 7246 |
. . . . . . 7
⊢ (1 / (1
− 𝐴)) ∈
V |
25 | 23, 24 | breldm 5777 |
. . . . . 6
⊢ (seq0( +
, (𝑛 ∈
ℕ0 ↦ (𝐴↑𝑛))) ⇝ (1 / (1 − 𝐴)) → seq0( + , (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))) ∈ dom ⇝ ) |
26 | 22, 25 | syl 17 |
. . . . 5
⊢ (𝜑 → seq0( + , (𝑛 ∈ ℕ0
↦ (𝐴↑𝑛))) ∈ dom ⇝
) |
27 | | nn0uz 12476 |
. . . . . 6
⊢
ℕ0 = (ℤ≥‘0) |
28 | | expcl 13653 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0)
→ (𝐴↑𝑗) ∈
ℂ) |
29 | 5, 28 | sylan 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐴↑𝑗) ∈ ℂ) |
30 | 21, 29 | eqeltrd 2838 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐴↑𝑛))‘𝑗) ∈ ℂ) |
31 | 27, 2, 30 | iserex 15220 |
. . . . 5
⊢ (𝜑 → (seq0( + , (𝑛 ∈ ℕ0
↦ (𝐴↑𝑛))) ∈ dom ⇝ ↔
seq𝑀( + , (𝑛 ∈ ℕ0
↦ (𝐴↑𝑛))) ∈ dom ⇝
)) |
32 | 26, 31 | mpbid 235 |
. . . 4
⊢ (𝜑 → seq𝑀( + , (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))) ∈ dom ⇝ ) |
33 | 16, 32 | eqeltrrd 2839 |
. . 3
⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ ) |
34 | 1, 3, 4, 9, 33 | isumclim2 15322 |
. 2
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐴↑𝑘)) |
35 | 13 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐴↑𝑛))‘𝑘) = (𝐴↑𝑘)) |
36 | | expcl 13653 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℂ ∧ 𝑘 ∈ ℕ0)
→ (𝐴↑𝑘) ∈
ℂ) |
37 | 5, 36 | sylan 583 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐴↑𝑘) ∈ ℂ) |
38 | 27, 1, 2, 35, 37, 26 | isumsplit 15404 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ ℕ0 (𝐴↑𝑘) = (Σ𝑘 ∈ (0...(𝑀 − 1))(𝐴↑𝑘) + Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐴↑𝑘))) |
39 | | 0zd 12188 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℤ) |
40 | 27, 39, 35, 37, 22 | isumclim 15321 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ ℕ0 (𝐴↑𝑘) = (1 / (1 − 𝐴))) |
41 | 38, 40 | eqtr3d 2779 |
. . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ (0...(𝑀 − 1))(𝐴↑𝑘) + Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐴↑𝑘)) = (1 / (1 − 𝐴))) |
42 | | 1re 10833 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ |
43 | 42 | ltnri 10941 |
. . . . . . . . . 10
⊢ ¬ 1
< 1 |
44 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝐴 = 1 → (abs‘𝐴) =
(abs‘1)) |
45 | | abs1 14861 |
. . . . . . . . . . . 12
⊢
(abs‘1) = 1 |
46 | 44, 45 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢ (𝐴 = 1 → (abs‘𝐴) = 1) |
47 | 46 | breq1d 5063 |
. . . . . . . . . 10
⊢ (𝐴 = 1 → ((abs‘𝐴) < 1 ↔ 1 <
1)) |
48 | 43, 47 | mtbiri 330 |
. . . . . . . . 9
⊢ (𝐴 = 1 → ¬
(abs‘𝐴) <
1) |
49 | 48 | necon2ai 2970 |
. . . . . . . 8
⊢
((abs‘𝐴) <
1 → 𝐴 ≠
1) |
50 | 17, 49 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ≠ 1) |
51 | 5, 50, 2 | geoser 15431 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑀 − 1))(𝐴↑𝑘) = ((1 − (𝐴↑𝑀)) / (1 − 𝐴))) |
52 | 51 | oveq1d 7228 |
. . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ (0...(𝑀 − 1))(𝐴↑𝑘) + Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐴↑𝑘)) = (((1 − (𝐴↑𝑀)) / (1 − 𝐴)) + Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐴↑𝑘))) |
53 | 41, 52 | eqtr3d 2779 |
. . . 4
⊢ (𝜑 → (1 / (1 − 𝐴)) = (((1 − (𝐴↑𝑀)) / (1 − 𝐴)) + Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐴↑𝑘))) |
54 | 53 | oveq1d 7228 |
. . 3
⊢ (𝜑 → ((1 / (1 − 𝐴)) − ((1 − (𝐴↑𝑀)) / (1 − 𝐴))) = ((((1 − (𝐴↑𝑀)) / (1 − 𝐴)) + Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐴↑𝑘)) − ((1 − (𝐴↑𝑀)) / (1 − 𝐴)))) |
55 | | 1cnd 10828 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℂ) |
56 | | ax-1cn 10787 |
. . . . . 6
⊢ 1 ∈
ℂ |
57 | 5, 2 | expcld 13716 |
. . . . . 6
⊢ (𝜑 → (𝐴↑𝑀) ∈ ℂ) |
58 | | subcl 11077 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ (𝐴↑𝑀) ∈ ℂ) → (1 − (𝐴↑𝑀)) ∈ ℂ) |
59 | 56, 57, 58 | sylancr 590 |
. . . . 5
⊢ (𝜑 → (1 − (𝐴↑𝑀)) ∈ ℂ) |
60 | | subcl 11077 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 − 𝐴) ∈ ℂ) |
61 | 56, 5, 60 | sylancr 590 |
. . . . 5
⊢ (𝜑 → (1 − 𝐴) ∈
ℂ) |
62 | 50 | necomd 2996 |
. . . . . 6
⊢ (𝜑 → 1 ≠ 𝐴) |
63 | | subeq0 11104 |
. . . . . . . 8
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) |
64 | 56, 5, 63 | sylancr 590 |
. . . . . . 7
⊢ (𝜑 → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) |
65 | 64 | necon3bid 2985 |
. . . . . 6
⊢ (𝜑 → ((1 − 𝐴) ≠ 0 ↔ 1 ≠ 𝐴)) |
66 | 62, 65 | mpbird 260 |
. . . . 5
⊢ (𝜑 → (1 − 𝐴) ≠ 0) |
67 | 55, 59, 61, 66 | divsubdird 11647 |
. . . 4
⊢ (𝜑 → ((1 − (1 −
(𝐴↑𝑀))) / (1 − 𝐴)) = ((1 / (1 − 𝐴)) − ((1 − (𝐴↑𝑀)) / (1 − 𝐴)))) |
68 | | nncan 11107 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ (𝐴↑𝑀) ∈ ℂ) → (1 − (1
− (𝐴↑𝑀))) = (𝐴↑𝑀)) |
69 | 56, 57, 68 | sylancr 590 |
. . . . 5
⊢ (𝜑 → (1 − (1 −
(𝐴↑𝑀))) = (𝐴↑𝑀)) |
70 | 69 | oveq1d 7228 |
. . . 4
⊢ (𝜑 → ((1 − (1 −
(𝐴↑𝑀))) / (1 − 𝐴)) = ((𝐴↑𝑀) / (1 − 𝐴))) |
71 | 67, 70 | eqtr3d 2779 |
. . 3
⊢ (𝜑 → ((1 / (1 − 𝐴)) − ((1 − (𝐴↑𝑀)) / (1 − 𝐴))) = ((𝐴↑𝑀) / (1 − 𝐴))) |
72 | 59, 61, 66 | divcld 11608 |
. . . 4
⊢ (𝜑 → ((1 − (𝐴↑𝑀)) / (1 − 𝐴)) ∈ ℂ) |
73 | 1, 3, 14, 9, 32 | isumcl 15325 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐴↑𝑘) ∈ ℂ) |
74 | 72, 73 | pncan2d 11191 |
. . 3
⊢ (𝜑 → ((((1 − (𝐴↑𝑀)) / (1 − 𝐴)) + Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐴↑𝑘)) − ((1 − (𝐴↑𝑀)) / (1 − 𝐴))) = Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐴↑𝑘)) |
75 | 54, 71, 74 | 3eqtr3rd 2786 |
. 2
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘𝑀)(𝐴↑𝑘) = ((𝐴↑𝑀) / (1 − 𝐴))) |
76 | 34, 75 | breqtrd 5079 |
1
⊢ (𝜑 → seq𝑀( + , 𝐹) ⇝ ((𝐴↑𝑀) / (1 − 𝐴))) |