Proof of Theorem pwm1geoser
Step | Hyp | Ref
| Expression |
1 | | 1m1e0 10966 |
. . . 4
⊢ (1
− 1) = 0 |
2 | | pwm1geoser.3 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
3 | 2 | nn0zd 11356 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
4 | | 1exp 12751 |
. . . . . 6
⊢ (𝑁 ∈ ℤ →
(1↑𝑁) =
1) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → (1↑𝑁) = 1) |
6 | 5 | oveq1d 6564 |
. . . 4
⊢ (𝜑 → ((1↑𝑁) − 1) = (1 −
1)) |
7 | | fzfid 12634 |
. . . . . 6
⊢ (𝜑 → (0...(𝑁 − 1)) ∈ Fin) |
8 | | 1cnd 9935 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 1 ∈
ℂ) |
9 | | elfznn0 12302 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0) |
10 | 9 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ0) |
11 | 8, 10 | expcld 12870 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (1↑𝑘) ∈
ℂ) |
12 | 7, 11 | fsumcl 14311 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))(1↑𝑘) ∈ ℂ) |
13 | 12 | mul02d 10113 |
. . . 4
⊢ (𝜑 → (0 · Σ𝑘 ∈ (0...(𝑁 − 1))(1↑𝑘)) = 0) |
14 | 1, 6, 13 | 3eqtr4a 2670 |
. . 3
⊢ (𝜑 → ((1↑𝑁) − 1) = (0 · Σ𝑘 ∈ (0...(𝑁 − 1))(1↑𝑘))) |
15 | | oveq1 6556 |
. . . . 5
⊢ (𝐴 = 1 → (𝐴↑𝑁) = (1↑𝑁)) |
16 | 15 | oveq1d 6564 |
. . . 4
⊢ (𝐴 = 1 → ((𝐴↑𝑁) − 1) = ((1↑𝑁) − 1)) |
17 | | oveq1 6556 |
. . . . . 6
⊢ (𝐴 = 1 → (𝐴 − 1) = (1 −
1)) |
18 | 17, 1 | syl6eq 2660 |
. . . . 5
⊢ (𝐴 = 1 → (𝐴 − 1) = 0) |
19 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝐴 = 1 → (𝐴↑𝑘) = (1↑𝑘)) |
20 | 19 | adantr 480 |
. . . . . . 7
⊢ ((𝐴 = 1 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑𝑘) = (1↑𝑘)) |
21 | 20 | ralrimiva 2949 |
. . . . . 6
⊢ (𝐴 = 1 → ∀𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) = (1↑𝑘)) |
22 | 21 | sumeq2d 14280 |
. . . . 5
⊢ (𝐴 = 1 → Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) = Σ𝑘 ∈ (0...(𝑁 − 1))(1↑𝑘)) |
23 | 18, 22 | oveq12d 6567 |
. . . 4
⊢ (𝐴 = 1 → ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)) = (0 · Σ𝑘 ∈ (0...(𝑁 − 1))(1↑𝑘))) |
24 | 16, 23 | eqeq12d 2625 |
. . 3
⊢ (𝐴 = 1 → (((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)) ↔ ((1↑𝑁) − 1) = (0 · Σ𝑘 ∈ (0...(𝑁 − 1))(1↑𝑘)))) |
25 | 14, 24 | syl5ibr 235 |
. 2
⊢ (𝐴 = 1 → (𝜑 → ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)))) |
26 | | pwm1geoser.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
27 | 26 | adantl 481 |
. . . . 5
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → 𝐴 ∈ ℂ) |
28 | | neqne 2790 |
. . . . . 6
⊢ (¬
𝐴 = 1 → 𝐴 ≠ 1) |
29 | 28 | adantr 480 |
. . . . 5
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → 𝐴 ≠ 1) |
30 | 2 | adantl 481 |
. . . . 5
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → 𝑁 ∈
ℕ0) |
31 | 27, 29, 30 | geoser 14438 |
. . . 4
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) = ((1 − (𝐴↑𝑁)) / (1 − 𝐴))) |
32 | | eqcom 2617 |
. . . . 5
⊢
(Σ𝑘 ∈
(0...(𝑁 − 1))(𝐴↑𝑘) = ((1 − (𝐴↑𝑁)) / (1 − 𝐴)) ↔ ((1 − (𝐴↑𝑁)) / (1 − 𝐴)) = Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)) |
33 | | 1cnd 9935 |
. . . . . . . 8
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → 1 ∈ ℂ) |
34 | 26, 2 | expcld 12870 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴↑𝑁) ∈ ℂ) |
35 | 34 | adantl 481 |
. . . . . . . 8
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → (𝐴↑𝑁) ∈ ℂ) |
36 | | nesym 2838 |
. . . . . . . . . 10
⊢ (1 ≠
𝐴 ↔ ¬ 𝐴 = 1) |
37 | 36 | biimpri 217 |
. . . . . . . . 9
⊢ (¬
𝐴 = 1 → 1 ≠ 𝐴) |
38 | 37 | adantr 480 |
. . . . . . . 8
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → 1 ≠ 𝐴) |
39 | 33, 35, 33, 27, 38 | div2subd 10730 |
. . . . . . 7
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → ((1 − (𝐴↑𝑁)) / (1 − 𝐴)) = (((𝐴↑𝑁) − 1) / (𝐴 − 1))) |
40 | 39 | eqeq1d 2612 |
. . . . . 6
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → (((1 − (𝐴↑𝑁)) / (1 − 𝐴)) = Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) ↔ (((𝐴↑𝑁) − 1) / (𝐴 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘))) |
41 | | peano2cnm 10226 |
. . . . . . . . 9
⊢ ((𝐴↑𝑁) ∈ ℂ → ((𝐴↑𝑁) − 1) ∈
ℂ) |
42 | 34, 41 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴↑𝑁) − 1) ∈
ℂ) |
43 | 42 | adantl 481 |
. . . . . . 7
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → ((𝐴↑𝑁) − 1) ∈
ℂ) |
44 | | fzfid 12634 |
. . . . . . . 8
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → (0...(𝑁 − 1)) ∈ Fin) |
45 | 27 | adantr 480 |
. . . . . . . . 9
⊢ (((¬
𝐴 = 1 ∧ 𝜑) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝐴 ∈ ℂ) |
46 | 9 | adantl 481 |
. . . . . . . . 9
⊢ (((¬
𝐴 = 1 ∧ 𝜑) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ0) |
47 | 45, 46 | expcld 12870 |
. . . . . . . 8
⊢ (((¬
𝐴 = 1 ∧ 𝜑) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑𝑘) ∈ ℂ) |
48 | 44, 47 | fsumcl 14311 |
. . . . . . 7
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) ∈ ℂ) |
49 | | peano2cnm 10226 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (𝐴 − 1) ∈
ℂ) |
50 | 49 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝐴 = 1) → (𝐴 − 1) ∈
ℂ) |
51 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝐴 = 1) → 𝐴 ∈
ℂ) |
52 | | 1cnd 9935 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝐴 = 1) → 1 ∈
ℂ) |
53 | 28 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝐴 = 1) → 𝐴 ≠ 1) |
54 | 51, 52, 53 | subne0d 10280 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝐴 = 1) → (𝐴 − 1) ≠
0) |
55 | 50, 54 | jca 553 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝐴 = 1) → ((𝐴 − 1) ∈ ℂ ∧
(𝐴 − 1) ≠
0)) |
56 | 55 | ex 449 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (¬
𝐴 = 1 → ((𝐴 − 1) ∈ ℂ ∧
(𝐴 − 1) ≠
0))) |
57 | 26, 56 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (¬ 𝐴 = 1 → ((𝐴 − 1) ∈ ℂ ∧ (𝐴 − 1) ≠
0))) |
58 | 57 | impcom 445 |
. . . . . . 7
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → ((𝐴 − 1) ∈ ℂ ∧ (𝐴 − 1) ≠
0)) |
59 | | divmul2 10568 |
. . . . . . 7
⊢ ((((𝐴↑𝑁) − 1) ∈ ℂ ∧
Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) ∈ ℂ ∧ ((𝐴 − 1) ∈ ℂ ∧ (𝐴 − 1) ≠ 0)) →
((((𝐴↑𝑁) − 1) / (𝐴 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) ↔ ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)))) |
60 | 43, 48, 58, 59 | syl3anc 1318 |
. . . . . 6
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → ((((𝐴↑𝑁) − 1) / (𝐴 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) ↔ ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)))) |
61 | 40, 60 | bitrd 267 |
. . . . 5
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → (((1 − (𝐴↑𝑁)) / (1 − 𝐴)) = Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) ↔ ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)))) |
62 | 32, 61 | syl5bb 271 |
. . . 4
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → (Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) = ((1 − (𝐴↑𝑁)) / (1 − 𝐴)) ↔ ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)))) |
63 | 31, 62 | mpbid 221 |
. . 3
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘))) |
64 | 63 | ex 449 |
. 2
⊢ (¬
𝐴 = 1 → (𝜑 → ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)))) |
65 | 25, 64 | pm2.61i 175 |
1
⊢ (𝜑 → ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘))) |