Step | Hyp | Ref
| Expression |
1 | | fzofi 12635 |
. . . . . 6
⊢ (𝑀..^𝑁) ∈ Fin |
2 | 1 | a1i 11 |
. . . . 5
⊢ (𝜑 → (𝑀..^𝑁) ∈ Fin) |
3 | | ax-1cn 9873 |
. . . . . 6
⊢ 1 ∈
ℂ |
4 | | geoserg.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
5 | | subcl 10159 |
. . . . . 6
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 − 𝐴) ∈ ℂ) |
6 | 3, 4, 5 | sylancr 694 |
. . . . 5
⊢ (𝜑 → (1 − 𝐴) ∈
ℂ) |
7 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝐴 ∈ ℂ) |
8 | | geoserg.3 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈
ℕ0) |
9 | | elfzouz 12343 |
. . . . . . 7
⊢ (𝑘 ∈ (𝑀..^𝑁) → 𝑘 ∈ (ℤ≥‘𝑀)) |
10 | | eluznn0 11633 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑘 ∈
(ℤ≥‘𝑀)) → 𝑘 ∈ ℕ0) |
11 | 8, 9, 10 | syl2an 493 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 𝑘 ∈ ℕ0) |
12 | 7, 11 | expcld 12870 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐴↑𝑘) ∈ ℂ) |
13 | 2, 6, 12 | fsummulc1 14359 |
. . . 4
⊢ (𝜑 → (Σ𝑘 ∈ (𝑀..^𝑁)(𝐴↑𝑘) · (1 − 𝐴)) = Σ𝑘 ∈ (𝑀..^𝑁)((𝐴↑𝑘) · (1 − 𝐴))) |
14 | 3 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → 1 ∈ ℂ) |
15 | 12, 14, 7 | subdid 10365 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝐴↑𝑘) · (1 − 𝐴)) = (((𝐴↑𝑘) · 1) − ((𝐴↑𝑘) · 𝐴))) |
16 | 12 | mulid1d 9936 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝐴↑𝑘) · 1) = (𝐴↑𝑘)) |
17 | 7, 11 | expp1d 12871 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (𝐴↑(𝑘 + 1)) = ((𝐴↑𝑘) · 𝐴)) |
18 | 17 | eqcomd 2616 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝐴↑𝑘) · 𝐴) = (𝐴↑(𝑘 + 1))) |
19 | 16, 18 | oveq12d 6567 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → (((𝐴↑𝑘) · 1) − ((𝐴↑𝑘) · 𝐴)) = ((𝐴↑𝑘) − (𝐴↑(𝑘 + 1)))) |
20 | 15, 19 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀..^𝑁)) → ((𝐴↑𝑘) · (1 − 𝐴)) = ((𝐴↑𝑘) − (𝐴↑(𝑘 + 1)))) |
21 | 20 | sumeq2dv 14281 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)((𝐴↑𝑘) · (1 − 𝐴)) = Σ𝑘 ∈ (𝑀..^𝑁)((𝐴↑𝑘) − (𝐴↑(𝑘 + 1)))) |
22 | | oveq2 6557 |
. . . . 5
⊢ (𝑗 = 𝑘 → (𝐴↑𝑗) = (𝐴↑𝑘)) |
23 | | oveq2 6557 |
. . . . 5
⊢ (𝑗 = (𝑘 + 1) → (𝐴↑𝑗) = (𝐴↑(𝑘 + 1))) |
24 | | oveq2 6557 |
. . . . 5
⊢ (𝑗 = 𝑀 → (𝐴↑𝑗) = (𝐴↑𝑀)) |
25 | | oveq2 6557 |
. . . . 5
⊢ (𝑗 = 𝑁 → (𝐴↑𝑗) = (𝐴↑𝑁)) |
26 | | geoserg.4 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) |
27 | 4 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ ℂ) |
28 | | elfzuz 12209 |
. . . . . . 7
⊢ (𝑗 ∈ (𝑀...𝑁) → 𝑗 ∈ (ℤ≥‘𝑀)) |
29 | | eluznn0 11633 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑗 ∈
(ℤ≥‘𝑀)) → 𝑗 ∈ ℕ0) |
30 | 8, 28, 29 | syl2an 493 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝑗 ∈ ℕ0) |
31 | 27, 30 | expcld 12870 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → (𝐴↑𝑗) ∈ ℂ) |
32 | 22, 23, 24, 25, 26, 31 | telfsumo 14375 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)((𝐴↑𝑘) − (𝐴↑(𝑘 + 1))) = ((𝐴↑𝑀) − (𝐴↑𝑁))) |
33 | 13, 21, 32 | 3eqtrrd 2649 |
. . 3
⊢ (𝜑 → ((𝐴↑𝑀) − (𝐴↑𝑁)) = (Σ𝑘 ∈ (𝑀..^𝑁)(𝐴↑𝑘) · (1 − 𝐴))) |
34 | 4, 8 | expcld 12870 |
. . . . 5
⊢ (𝜑 → (𝐴↑𝑀) ∈ ℂ) |
35 | | eluznn0 11633 |
. . . . . . 7
⊢ ((𝑀 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘𝑀)) → 𝑁 ∈
ℕ0) |
36 | 8, 26, 35 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
37 | 4, 36 | expcld 12870 |
. . . . 5
⊢ (𝜑 → (𝐴↑𝑁) ∈ ℂ) |
38 | 34, 37 | subcld 10271 |
. . . 4
⊢ (𝜑 → ((𝐴↑𝑀) − (𝐴↑𝑁)) ∈ ℂ) |
39 | 2, 12 | fsumcl 14311 |
. . . 4
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(𝐴↑𝑘) ∈ ℂ) |
40 | | geoserg.2 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ 1) |
41 | 40 | necomd 2837 |
. . . . 5
⊢ (𝜑 → 1 ≠ 𝐴) |
42 | | subeq0 10186 |
. . . . . . 7
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) |
43 | 3, 4, 42 | sylancr 694 |
. . . . . 6
⊢ (𝜑 → ((1 − 𝐴) = 0 ↔ 1 = 𝐴)) |
44 | 43 | necon3bid 2826 |
. . . . 5
⊢ (𝜑 → ((1 − 𝐴) ≠ 0 ↔ 1 ≠ 𝐴)) |
45 | 41, 44 | mpbird 246 |
. . . 4
⊢ (𝜑 → (1 − 𝐴) ≠ 0) |
46 | 38, 39, 6, 45 | divmul3d 10714 |
. . 3
⊢ (𝜑 → ((((𝐴↑𝑀) − (𝐴↑𝑁)) / (1 − 𝐴)) = Σ𝑘 ∈ (𝑀..^𝑁)(𝐴↑𝑘) ↔ ((𝐴↑𝑀) − (𝐴↑𝑁)) = (Σ𝑘 ∈ (𝑀..^𝑁)(𝐴↑𝑘) · (1 − 𝐴)))) |
47 | 33, 46 | mpbird 246 |
. 2
⊢ (𝜑 → (((𝐴↑𝑀) − (𝐴↑𝑁)) / (1 − 𝐴)) = Σ𝑘 ∈ (𝑀..^𝑁)(𝐴↑𝑘)) |
48 | 47 | eqcomd 2616 |
1
⊢ (𝜑 → Σ𝑘 ∈ (𝑀..^𝑁)(𝐴↑𝑘) = (((𝐴↑𝑀) − (𝐴↑𝑁)) / (1 − 𝐴))) |