Step | Hyp | Ref
| Expression |
1 | | nn0uz 12620 |
. . 3
⊢
ℕ0 = (ℤ≥‘0) |
2 | | 0zd 12331 |
. . 3
⊢ (𝜑 → 0 ∈
ℤ) |
3 | | geolim.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
4 | | geolim.2 |
. . . . . 6
⊢ (𝜑 → (abs‘𝐴) < 1) |
5 | 3, 4 | expcnv 15576 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) ⇝ 0) |
6 | | ax-1cn 10929 |
. . . . . . 7
⊢ 1 ∈
ℂ |
7 | | subcl 11220 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 − 𝐴) ∈ ℂ) |
8 | 6, 3, 7 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → (1 − 𝐴) ∈
ℂ) |
9 | | 1re 10975 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
10 | 9 | ltnri 11084 |
. . . . . . . . . . 11
⊢ ¬ 1
< 1 |
11 | | fveq2 6774 |
. . . . . . . . . . . . 13
⊢ (𝐴 = 1 → (abs‘𝐴) =
(abs‘1)) |
12 | | abs1 15009 |
. . . . . . . . . . . . 13
⊢
(abs‘1) = 1 |
13 | 11, 12 | eqtrdi 2794 |
. . . . . . . . . . . 12
⊢ (𝐴 = 1 → (abs‘𝐴) = 1) |
14 | 13 | breq1d 5084 |
. . . . . . . . . . 11
⊢ (𝐴 = 1 → ((abs‘𝐴) < 1 ↔ 1 <
1)) |
15 | 10, 14 | mtbiri 327 |
. . . . . . . . . 10
⊢ (𝐴 = 1 → ¬
(abs‘𝐴) <
1) |
16 | 15 | necon2ai 2973 |
. . . . . . . . 9
⊢
((abs‘𝐴) <
1 → 𝐴 ≠
1) |
17 | 4, 16 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ≠ 1) |
18 | 17 | necomd 2999 |
. . . . . . 7
⊢ (𝜑 → 1 ≠ 𝐴) |
19 | | subeq0 11247 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) |
20 | 6, 3, 19 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) |
21 | 20 | necon3bid 2988 |
. . . . . . 7
⊢ (𝜑 → ((1 − 𝐴) ≠ 0 ↔ 1 ≠ 𝐴)) |
22 | 18, 21 | mpbird 256 |
. . . . . 6
⊢ (𝜑 → (1 − 𝐴) ≠ 0) |
23 | 3, 8, 22 | divcld 11751 |
. . . . 5
⊢ (𝜑 → (𝐴 / (1 − 𝐴)) ∈ ℂ) |
24 | | nn0ex 12239 |
. . . . . . 7
⊢
ℕ0 ∈ V |
25 | 24 | mptex 7099 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) ∈ V |
26 | 25 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) ∈ V) |
27 | | oveq2 7283 |
. . . . . . . 8
⊢ (𝑛 = 𝑗 → (𝐴↑𝑛) = (𝐴↑𝑗)) |
28 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ (𝐴↑𝑛)) = (𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛)) |
29 | | ovex 7308 |
. . . . . . . 8
⊢ (𝐴↑𝑗) ∈ V |
30 | 27, 28, 29 | fvmpt 6875 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ (𝐴↑𝑛))‘𝑗) = (𝐴↑𝑗)) |
31 | 30 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐴↑𝑛))‘𝑗) = (𝐴↑𝑗)) |
32 | | expcl 13800 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0)
→ (𝐴↑𝑗) ∈
ℂ) |
33 | 3, 32 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐴↑𝑗) ∈ ℂ) |
34 | 31, 33 | eqeltrd 2839 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ (𝐴↑𝑛))‘𝑗) ∈ ℂ) |
35 | | expp1 13789 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑗 ∈ ℕ0)
→ (𝐴↑(𝑗 + 1)) = ((𝐴↑𝑗) · 𝐴)) |
36 | 3, 35 | sylan 580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐴↑(𝑗 + 1)) = ((𝐴↑𝑗) · 𝐴)) |
37 | 3 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ∈
ℂ) |
38 | 33, 37 | mulcomd 10996 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝐴↑𝑗) · 𝐴) = (𝐴 · (𝐴↑𝑗))) |
39 | 36, 38 | eqtrd 2778 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐴↑(𝑗 + 1)) = (𝐴 · (𝐴↑𝑗))) |
40 | 39 | oveq1d 7290 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)) = ((𝐴 · (𝐴↑𝑗)) / (1 − 𝐴))) |
41 | 8 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (1
− 𝐴) ∈
ℂ) |
42 | 22 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (1
− 𝐴) ≠
0) |
43 | 37, 33, 41, 42 | div23d 11788 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝐴 · (𝐴↑𝑗)) / (1 − 𝐴)) = ((𝐴 / (1 − 𝐴)) · (𝐴↑𝑗))) |
44 | 40, 43 | eqtrd 2778 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)) = ((𝐴 / (1 − 𝐴)) · (𝐴↑𝑗))) |
45 | | oveq1 7282 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑗 → (𝑛 + 1) = (𝑗 + 1)) |
46 | 45 | oveq2d 7291 |
. . . . . . . . 9
⊢ (𝑛 = 𝑗 → (𝐴↑(𝑛 + 1)) = (𝐴↑(𝑗 + 1))) |
47 | 46 | oveq1d 7290 |
. . . . . . . 8
⊢ (𝑛 = 𝑗 → ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)) = ((𝐴↑(𝑗 + 1)) / (1 − 𝐴))) |
48 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) = (𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) |
49 | | ovex 7308 |
. . . . . . . 8
⊢ ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)) ∈ V |
50 | 47, 48, 49 | fvmpt 6875 |
. . . . . . 7
⊢ (𝑗 ∈ ℕ0
→ ((𝑛 ∈
ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗) = ((𝐴↑(𝑗 + 1)) / (1 − 𝐴))) |
51 | 50 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗) = ((𝐴↑(𝑗 + 1)) / (1 − 𝐴))) |
52 | 31 | oveq2d 7291 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝐴 / (1 − 𝐴)) · ((𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))‘𝑗)) = ((𝐴 / (1 − 𝐴)) · (𝐴↑𝑗))) |
53 | 44, 51, 52 | 3eqtr4d 2788 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗) = ((𝐴 / (1 − 𝐴)) · ((𝑛 ∈ ℕ0 ↦ (𝐴↑𝑛))‘𝑗))) |
54 | 1, 2, 5, 23, 26, 34, 53 | climmulc2 15346 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) ⇝ ((𝐴 / (1 − 𝐴)) · 0)) |
55 | 23 | mul01d 11174 |
. . . 4
⊢ (𝜑 → ((𝐴 / (1 − 𝐴)) · 0) = 0) |
56 | 54, 55 | breqtrd 5100 |
. . 3
⊢ (𝜑 → (𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴))) ⇝ 0) |
57 | 8, 22 | reccld 11744 |
. . 3
⊢ (𝜑 → (1 / (1 − 𝐴)) ∈
ℂ) |
58 | | seqex 13723 |
. . . 4
⊢ seq0( + ,
𝐹) ∈
V |
59 | 58 | a1i 11 |
. . 3
⊢ (𝜑 → seq0( + , 𝐹) ∈ V) |
60 | | peano2nn0 12273 |
. . . . . 6
⊢ (𝑗 ∈ ℕ0
→ (𝑗 + 1) ∈
ℕ0) |
61 | | expcl 13800 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ (𝑗 + 1) ∈
ℕ0) → (𝐴↑(𝑗 + 1)) ∈ ℂ) |
62 | 3, 60, 61 | syl2an 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝐴↑(𝑗 + 1)) ∈ ℂ) |
63 | 62, 41, 42 | divcld 11751 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)) ∈ ℂ) |
64 | 51, 63 | eqeltrd 2839 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑛 ∈ ℕ0
↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗) ∈ ℂ) |
65 | | nn0cn 12243 |
. . . . . . . 8
⊢ (𝑗 ∈ ℕ0
→ 𝑗 ∈
ℂ) |
66 | 65 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈
ℂ) |
67 | | pncan 11227 |
. . . . . . 7
⊢ ((𝑗 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑗 + 1)
− 1) = 𝑗) |
68 | 66, 6, 67 | sylancl 586 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((𝑗 + 1) − 1) = 𝑗) |
69 | 68 | oveq2d 7291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
(0...((𝑗 + 1) − 1)) =
(0...𝑗)) |
70 | 69 | sumeq1d 15413 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
Σ𝑘 ∈
(0...((𝑗 + 1) −
1))(𝐴↑𝑘) = Σ𝑘 ∈ (0...𝑗)(𝐴↑𝑘)) |
71 | 6 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 1 ∈
ℂ) |
72 | 71, 62, 41, 42 | divsubdird 11790 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((1
− (𝐴↑(𝑗 + 1))) / (1 − 𝐴)) = ((1 / (1 − 𝐴)) − ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)))) |
73 | 17 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝐴 ≠ 1) |
74 | 60 | adantl 482 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (𝑗 + 1) ∈
ℕ0) |
75 | 37, 73, 74 | geoser 15579 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
Σ𝑘 ∈
(0...((𝑗 + 1) −
1))(𝐴↑𝑘) = ((1 − (𝐴↑(𝑗 + 1))) / (1 − 𝐴))) |
76 | 51 | oveq2d 7291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → ((1 / (1
− 𝐴)) − ((𝑛 ∈ ℕ0
↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗)) = ((1 / (1 − 𝐴)) − ((𝐴↑(𝑗 + 1)) / (1 − 𝐴)))) |
77 | 72, 75, 76 | 3eqtr4d 2788 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
Σ𝑘 ∈
(0...((𝑗 + 1) −
1))(𝐴↑𝑘) = ((1 / (1 − 𝐴)) − ((𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗))) |
78 | | simpll 764 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑗)) → 𝜑) |
79 | | elfznn0 13349 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑗) → 𝑘 ∈ ℕ0) |
80 | 79 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑗)) → 𝑘 ∈ ℕ0) |
81 | | geolim.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ0) → (𝐹‘𝑘) = (𝐴↑𝑘)) |
82 | 78, 80, 81 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑗)) → (𝐹‘𝑘) = (𝐴↑𝑘)) |
83 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈
ℕ0) |
84 | 83, 1 | eleqtrdi 2849 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → 𝑗 ∈
(ℤ≥‘0)) |
85 | 78, 3 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑗)) → 𝐴 ∈ ℂ) |
86 | 85, 80 | expcld 13864 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ ℕ0) ∧ 𝑘 ∈ (0...𝑗)) → (𝐴↑𝑘) ∈ ℂ) |
87 | 82, 84, 86 | fsumser 15442 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) →
Σ𝑘 ∈ (0...𝑗)(𝐴↑𝑘) = (seq0( + , 𝐹)‘𝑗)) |
88 | 70, 77, 87 | 3eqtr3rd 2787 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ ℕ0) → (seq0( +
, 𝐹)‘𝑗) = ((1 / (1 − 𝐴)) − ((𝑛 ∈ ℕ0 ↦ ((𝐴↑(𝑛 + 1)) / (1 − 𝐴)))‘𝑗))) |
89 | 1, 2, 56, 57, 59, 64, 88 | climsubc2 15348 |
. 2
⊢ (𝜑 → seq0( + , 𝐹) ⇝ ((1 / (1 − 𝐴)) − 0)) |
90 | 57 | subid1d 11321 |
. 2
⊢ (𝜑 → ((1 / (1 − 𝐴)) − 0) = (1 / (1 −
𝐴))) |
91 | 89, 90 | breqtrd 5100 |
1
⊢ (𝜑 → seq0( + , 𝐹) ⇝ (1 / (1 − 𝐴))) |