Step | Hyp | Ref
| Expression |
1 | | nn0uz 12283 |
. . 3
⊢
ℕ0 = (ℤ≥‘0) |
2 | | 0zd 11996 |
. . 3
⊢ (𝜑 → 0 ∈
ℤ) |
3 | | geolim.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
4 | | geolim.2 |
. . . . . 6
⊢ (𝜑 → (abs‘𝐴) < 1) |
5 | 3, 4 | expcnv 15222 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ⇝ 0) |
6 | | ax-1cn 10598 |
. . . . . . 7
⊢ 1 ∈
ℂ |
7 | | subcl 10888 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 − 𝐴) ∈ ℂ) |
8 | 6, 3, 7 | sylancr 589 |
. . . . . 6
⊢ (𝜑 → (1 − 𝐴) ∈
ℂ) |
9 | | 1re 10644 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
10 | 9 | ltnri 10752 |
. . . . . . . . . . 11
⊢ ¬ 1
< 1 |
11 | | fveq2 6673 |
. . . . . . . . . . . . 13
⊢ (𝐴 = 1 → (abs‘𝐴) =
(abs‘1)) |
12 | | abs1 14660 |
. . . . . . . . . . . . 13
⊢
(abs‘1) = 1 |
13 | 11, 12 | syl6eq 2875 |
. . . . . . . . . . . 12
⊢ (𝐴 = 1 → (abs‘𝐴) = 1) |
14 | 13 | breq1d 5079 |
. . . . . . . . . . 11
⊢ (𝐴 = 1 → ((abs‘𝐴) < 1 ↔ 1 <
1)) |
15 | 10, 14 | mtbiri 329 |
. . . . . . . . . 10
⊢ (𝐴 = 1 → ¬
(abs‘𝐴) <
1) |
16 | 15 | necon2ai 3048 |
. . . . . . . . 9
⊢
((abs‘𝐴) <
1 → 𝐴 ≠
1) |
17 | 4, 16 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ≠ 1) |
18 | 17 | necomd 3074 |
. . . . . . 7
⊢ (𝜑 → 1 ≠ 𝐴) |
19 | | subeq0 10915 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) |
20 | 6, 3, 19 | sylancr 589 |
. . . . . . . 8
⊢ (𝜑 → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) |
21 | 20 | necon3bid 3063 |
. . . . . . 7
⊢ (𝜑 → ((1 − 𝐴) ≠ 0 ↔ 1 ≠ 𝐴)) |
22 | 18, 21 | mpbird 259 |
. . . . . 6
⊢ (𝜑 → (1 − 𝐴) ≠ 0) |
23 | 3, 8, 22 | divcld 11419 |
. . . . 5
⊢ (𝜑 → (𝐴 / (1 − 𝐴)) ∈ ℂ) |
24 | | nn0ex 11906 |
. . . . . . 7
⊢
ℕ0 ∈ V |
25 | 24 | mptex 6989 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) ∈ V |
26 | 25 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) ∈ V) |
27 | | oveq2 7167 |
. . . . . . . 8
⊢ (𝑛 = 𝑗 → (𝐴↑𝑛) = (𝐴↑𝑗)) |
28 | | eqid 2824 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ (𝐴↑𝑛)) = (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) |
29 | | ovex 7192 |
. . . . . . . 8
⊢ (𝐴↑𝑗) ∈ V |
30 | 27, 28, 29 | fvmpt 6771 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ (𝐴↑𝑛))‘𝑗) = (𝐴↑𝑗)) |
31 | 30 | adantl 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐴↑𝑛))‘𝑗) = (𝐴↑𝑗)) |
32 | | expcl 13450 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0)
→ (𝐴↑𝑗) ∈
ℂ) |
33 | 3, 32 | sylan 582 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐴↑𝑗) ∈ ℂ) |
34 | 31, 33 | eqeltrd 2916 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐴↑𝑛))‘𝑗) ∈ ℂ) |
35 | | expp1 13439 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0)
→ (𝐴↑(𝑗 + 1)) = ((𝐴↑𝑗) · 𝐴)) |
36 | 3, 35 | sylan 582 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐴↑(𝑗 + 1)) = ((𝐴↑𝑗) · 𝐴)) |
37 | 3 | adantr 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈
ℂ) |
38 | 33, 37 | mulcomd 10665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝐴↑𝑗) · 𝐴) = (𝐴 · (𝐴↑𝑗))) |
39 | 36, 38 | eqtrd 2859 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐴↑(𝑗 + 1)) = (𝐴 · (𝐴↑𝑗))) |
40 | 39 | oveq1d 7174 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)) = ((𝐴 · (𝐴↑𝑗)) / (1 − 𝐴))) |
41 | 8 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (1
− 𝐴) ∈
ℂ) |
42 | 22 | adantr 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (1
− 𝐴) ≠
0) |
43 | 37, 33, 41, 42 | div23d 11456 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝐴 · (𝐴↑𝑗)) / (1 − 𝐴)) = ((𝐴 / (1 − 𝐴)) · (𝐴↑𝑗))) |
44 | 40, 43 | eqtrd 2859 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)) = ((𝐴 / (1 − 𝐴)) · (𝐴↑𝑗))) |
45 | | oveq1 7166 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → (𝑛 + 1) = (𝑗 + 1)) |
46 | 45 | oveq2d 7175 |
. . . . . . . . 9
⊢ (𝑛 = 𝑗 → (𝐴↑(𝑛 + 1)) = (𝐴↑(𝑗 + 1))) |
47 | 46 | oveq1d 7174 |
. . . . . . . 8
⊢ (𝑛 = 𝑗 → ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)) = ((𝐴↑(𝑗 + 1)) / (1 − 𝐴))) |
48 | | eqid 2824 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) = (𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) |
49 | | ovex 7192 |
. . . . . . . 8
⊢ ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)) ∈ V |
50 | 47, 48, 49 | fvmpt 6771 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗) = ((𝐴↑(𝑗 + 1)) / (1 − 𝐴))) |
51 | 50 | adantl 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗) = ((𝐴↑(𝑗 + 1)) / (1 − 𝐴))) |
52 | 31 | oveq2d 7175 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝐴 / (1 − 𝐴)) · ((𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))‘𝑗)) = ((𝐴 / (1 − 𝐴)) · (𝐴↑𝑗))) |
53 | 44, 51, 52 | 3eqtr4d 2869 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗) = ((𝐴 / (1 − 𝐴)) · ((𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))‘𝑗))) |
54 | 1, 2, 5, 23, 26, 34, 53 | climmulc2 14996 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) ⇝ ((𝐴 / (1 − 𝐴)) · 0)) |
55 | 23 | mul01d 10842 |
. . . 4
⊢ (𝜑 → ((𝐴 / (1 − 𝐴)) · 0) = 0) |
56 | 54, 55 | breqtrd 5095 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) ⇝ 0) |
57 | 8, 22 | reccld 11412 |
. . 3
⊢ (𝜑 → (1 / (1 − 𝐴)) ∈
ℂ) |
58 | | seqex 13374 |
. . . 4
⊢ seq0( + ,
𝐹) ∈
V |
59 | 58 | a1i 11 |
. . 3
⊢ (𝜑 → seq0( + , 𝐹) ∈ V) |
60 | | peano2nn0 11940 |
. . . . . 6
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ0) |
61 | | expcl 13450 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ (𝑗 + 1) ∈
ℕ0) → (𝐴↑(𝑗 + 1)) ∈ ℂ) |
62 | 3, 60, 61 | syl2an 597 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐴↑(𝑗 + 1)) ∈ ℂ) |
63 | 62, 41, 42 | divcld 11419 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)) ∈ ℂ) |
64 | 51, 63 | eqeltrd 2916 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗) ∈ ℂ) |
65 | | nn0cn 11910 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0
→ 𝑗 ∈
ℂ) |
66 | 65 | adantl 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈
ℂ) |
67 | | pncan 10895 |
. . . . . . 7
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑗 + 1)
− 1) = 𝑗) |
68 | 66, 6, 67 | sylancl 588 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑗 + 1) − 1) = 𝑗) |
69 | 68 | oveq2d 7175 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(0...((𝑗 + 1) − 1)) =
(0...𝑗)) |
70 | 69 | sumeq1d 15061 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
Σ𝑘 ∈
(0...((𝑗 + 1) −
1))(𝐴↑𝑘) = Σ𝑘 ∈ (0...𝑗)(𝐴↑𝑘)) |
71 | 6 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 1 ∈
ℂ) |
72 | 71, 62, 41, 42 | divsubdird 11458 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((1
− (𝐴↑(𝑗 + 1))) / (1 − 𝐴)) = ((1 / (1 − 𝐴)) − ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)))) |
73 | 17 | adantr 483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ≠ 1) |
74 | 60 | adantl 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑗 + 1) ∈
ℕ0) |
75 | 37, 73, 74 | geoser 15225 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
Σ𝑘 ∈
(0...((𝑗 + 1) −
1))(𝐴↑𝑘) = ((1 − (𝐴↑(𝑗 + 1))) / (1 − 𝐴))) |
76 | 51 | oveq2d 7175 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((1 / (1
− 𝐴)) − ((𝑛 ∈ ℕ0
↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗)) = ((1 / (1 − 𝐴)) − ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)))) |
77 | 72, 75, 76 | 3eqtr4d 2869 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
Σ𝑘 ∈
(0...((𝑗 + 1) −
1))(𝐴↑𝑘) = ((1 / (1 − 𝐴)) − ((𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗))) |
78 | | simpll 765 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑗)) → 𝜑) |
79 | | elfznn0 13003 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑗) → 𝑘 ∈ ℕ0) |
80 | 79 | adantl 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑗)) → 𝑘 ∈ ℕ0) |
81 | | geolim.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = (𝐴↑𝑘)) |
82 | 78, 80, 81 | syl2anc 586 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑗)) → (𝐹‘𝑘) = (𝐴↑𝑘)) |
83 | | simpr 487 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈
ℕ0) |
84 | 83, 1 | eleqtrdi 2926 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈
(ℤ≥‘0)) |
85 | 78, 3 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑗)) → 𝐴 ∈ ℂ) |
86 | 85, 80 | expcld 13513 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑗)) → (𝐴↑𝑘) ∈ ℂ) |
87 | 82, 84, 86 | fsumser 15090 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
Σ𝑘 ∈ (0...𝑗)(𝐴↑𝑘) = (seq0( + , 𝐹)‘𝑗)) |
88 | 70, 77, 87 | 3eqtr3rd 2868 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (seq0( +
, 𝐹)‘𝑗) = ((1 / (1 − 𝐴)) − ((𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗))) |
89 | 1, 2, 56, 57, 59, 64, 88 | climsubc2 14998 |
. 2
⊢ (𝜑 → seq0( + , 𝐹) ⇝ ((1 / (1 − 𝐴)) − 0)) |
90 | 57 | subid1d 10989 |
. 2
⊢ (𝜑 → ((1 / (1 − 𝐴)) − 0) = (1 / (1 −
𝐴))) |
91 | 89, 90 | breqtrd 5095 |
1
⊢ (𝜑 → seq0( + , 𝐹) ⇝ (1 / (1 − 𝐴))) |