Proof of Theorem pwm1geoserOLD
Step | Hyp | Ref
| Expression |
1 | | 1m1e0 11710 |
. . . 4
⊢ (1
− 1) = 0 |
2 | | pwm1geoserOLD.3 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
3 | 2 | nn0zd 12086 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
4 | | 1exp 13459 |
. . . . . 6
⊢ (𝑁 ∈ ℤ →
(1↑𝑁) =
1) |
5 | 3, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → (1↑𝑁) = 1) |
6 | 5 | oveq1d 7171 |
. . . 4
⊢ (𝜑 → ((1↑𝑁) − 1) = (1 −
1)) |
7 | | fzfid 13342 |
. . . . . 6
⊢ (𝜑 → (0...(𝑁 − 1)) ∈ Fin) |
8 | | 1cnd 10636 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 1 ∈
ℂ) |
9 | | elfznn0 13001 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...(𝑁 − 1)) → 𝑘 ∈ ℕ0) |
10 | 9 | adantl 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ0) |
11 | 8, 10 | expcld 13511 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (1↑𝑘) ∈
ℂ) |
12 | 7, 11 | fsumcl 15090 |
. . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 − 1))(1↑𝑘) ∈ ℂ) |
13 | 12 | mul02d 10838 |
. . . 4
⊢ (𝜑 → (0 · Σ𝑘 ∈ (0...(𝑁 − 1))(1↑𝑘)) = 0) |
14 | 1, 6, 13 | 3eqtr4a 2882 |
. . 3
⊢ (𝜑 → ((1↑𝑁) − 1) = (0 · Σ𝑘 ∈ (0...(𝑁 − 1))(1↑𝑘))) |
15 | | oveq1 7163 |
. . . . 5
⊢ (𝐴 = 1 → (𝐴↑𝑁) = (1↑𝑁)) |
16 | 15 | oveq1d 7171 |
. . . 4
⊢ (𝐴 = 1 → ((𝐴↑𝑁) − 1) = ((1↑𝑁) − 1)) |
17 | | oveq1 7163 |
. . . . . 6
⊢ (𝐴 = 1 → (𝐴 − 1) = (1 −
1)) |
18 | 17, 1 | syl6eq 2872 |
. . . . 5
⊢ (𝐴 = 1 → (𝐴 − 1) = 0) |
19 | | oveq1 7163 |
. . . . . 6
⊢ (𝐴 = 1 → (𝐴↑𝑘) = (1↑𝑘)) |
20 | 19 | sumeq2sdv 15061 |
. . . . 5
⊢ (𝐴 = 1 → Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) = Σ𝑘 ∈ (0...(𝑁 − 1))(1↑𝑘)) |
21 | 18, 20 | oveq12d 7174 |
. . . 4
⊢ (𝐴 = 1 → ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)) = (0 · Σ𝑘 ∈ (0...(𝑁 − 1))(1↑𝑘))) |
22 | 16, 21 | eqeq12d 2837 |
. . 3
⊢ (𝐴 = 1 → (((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)) ↔ ((1↑𝑁) − 1) = (0 · Σ𝑘 ∈ (0...(𝑁 − 1))(1↑𝑘)))) |
23 | 14, 22 | syl5ibr 248 |
. 2
⊢ (𝐴 = 1 → (𝜑 → ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)))) |
24 | | pwm1geoserOLD.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℂ) |
25 | 24 | adantl 484 |
. . . . 5
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → 𝐴 ∈ ℂ) |
26 | | neqne 3024 |
. . . . . 6
⊢ (¬
𝐴 = 1 → 𝐴 ≠ 1) |
27 | 26 | adantr 483 |
. . . . 5
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → 𝐴 ≠ 1) |
28 | 2 | adantl 484 |
. . . . 5
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → 𝑁 ∈
ℕ0) |
29 | 25, 27, 28 | geoser 15222 |
. . . 4
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) = ((1 − (𝐴↑𝑁)) / (1 − 𝐴))) |
30 | | eqcom 2828 |
. . . . 5
⊢
(Σ𝑘 ∈
(0...(𝑁 − 1))(𝐴↑𝑘) = ((1 − (𝐴↑𝑁)) / (1 − 𝐴)) ↔ ((1 − (𝐴↑𝑁)) / (1 − 𝐴)) = Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)) |
31 | | 1cnd 10636 |
. . . . . . . 8
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → 1 ∈ ℂ) |
32 | 24, 2 | expcld 13511 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴↑𝑁) ∈ ℂ) |
33 | 32 | adantl 484 |
. . . . . . . 8
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → (𝐴↑𝑁) ∈ ℂ) |
34 | | nesym 3072 |
. . . . . . . . . 10
⊢ (1 ≠
𝐴 ↔ ¬ 𝐴 = 1) |
35 | 34 | biimpri 230 |
. . . . . . . . 9
⊢ (¬
𝐴 = 1 → 1 ≠ 𝐴) |
36 | 35 | adantr 483 |
. . . . . . . 8
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → 1 ≠ 𝐴) |
37 | 31, 33, 31, 25, 36 | div2subd 11466 |
. . . . . . 7
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → ((1 − (𝐴↑𝑁)) / (1 − 𝐴)) = (((𝐴↑𝑁) − 1) / (𝐴 − 1))) |
38 | 37 | eqeq1d 2823 |
. . . . . 6
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → (((1 − (𝐴↑𝑁)) / (1 − 𝐴)) = Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) ↔ (((𝐴↑𝑁) − 1) / (𝐴 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘))) |
39 | | peano2cnm 10952 |
. . . . . . . . 9
⊢ ((𝐴↑𝑁) ∈ ℂ → ((𝐴↑𝑁) − 1) ∈
ℂ) |
40 | 32, 39 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴↑𝑁) − 1) ∈
ℂ) |
41 | 40 | adantl 484 |
. . . . . . 7
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → ((𝐴↑𝑁) − 1) ∈
ℂ) |
42 | | fzfid 13342 |
. . . . . . . 8
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → (0...(𝑁 − 1)) ∈ Fin) |
43 | 25 | adantr 483 |
. . . . . . . . 9
⊢ (((¬
𝐴 = 1 ∧ 𝜑) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝐴 ∈ ℂ) |
44 | 9 | adantl 484 |
. . . . . . . . 9
⊢ (((¬
𝐴 = 1 ∧ 𝜑) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → 𝑘 ∈ ℕ0) |
45 | 43, 44 | expcld 13511 |
. . . . . . . 8
⊢ (((¬
𝐴 = 1 ∧ 𝜑) ∧ 𝑘 ∈ (0...(𝑁 − 1))) → (𝐴↑𝑘) ∈ ℂ) |
46 | 42, 45 | fsumcl 15090 |
. . . . . . 7
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) ∈ ℂ) |
47 | | peano2cnm 10952 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ ℂ → (𝐴 − 1) ∈
ℂ) |
48 | 47 | adantr 483 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝐴 = 1) → (𝐴 − 1) ∈
ℂ) |
49 | | simpl 485 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝐴 = 1) → 𝐴 ∈
ℂ) |
50 | | 1cnd 10636 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝐴 = 1) → 1 ∈
ℂ) |
51 | 26 | adantl 484 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝐴 = 1) → 𝐴 ≠ 1) |
52 | 49, 50, 51 | subne0d 11006 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝐴 = 1) → (𝐴 − 1) ≠
0) |
53 | 48, 52 | jca 514 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ ¬
𝐴 = 1) → ((𝐴 − 1) ∈ ℂ ∧
(𝐴 − 1) ≠
0)) |
54 | 53 | ex 415 |
. . . . . . . . 9
⊢ (𝐴 ∈ ℂ → (¬
𝐴 = 1 → ((𝐴 − 1) ∈ ℂ ∧
(𝐴 − 1) ≠
0))) |
55 | 24, 54 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (¬ 𝐴 = 1 → ((𝐴 − 1) ∈ ℂ ∧ (𝐴 − 1) ≠
0))) |
56 | 55 | impcom 410 |
. . . . . . 7
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → ((𝐴 − 1) ∈ ℂ ∧ (𝐴 − 1) ≠
0)) |
57 | | divmul2 11302 |
. . . . . . 7
⊢ ((((𝐴↑𝑁) − 1) ∈ ℂ ∧
Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) ∈ ℂ ∧ ((𝐴 − 1) ∈ ℂ ∧ (𝐴 − 1) ≠ 0)) →
((((𝐴↑𝑁) − 1) / (𝐴 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) ↔ ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)))) |
58 | 41, 46, 56, 57 | syl3anc 1367 |
. . . . . 6
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → ((((𝐴↑𝑁) − 1) / (𝐴 − 1)) = Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) ↔ ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)))) |
59 | 38, 58 | bitrd 281 |
. . . . 5
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → (((1 − (𝐴↑𝑁)) / (1 − 𝐴)) = Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) ↔ ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)))) |
60 | 30, 59 | syl5bb 285 |
. . . 4
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → (Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘) = ((1 − (𝐴↑𝑁)) / (1 − 𝐴)) ↔ ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)))) |
61 | 29, 60 | mpbid 234 |
. . 3
⊢ ((¬
𝐴 = 1 ∧ 𝜑) → ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘))) |
62 | 61 | ex 415 |
. 2
⊢ (¬
𝐴 = 1 → (𝜑 → ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘)))) |
63 | 23, 62 | pm2.61i 184 |
1
⊢ (𝜑 → ((𝐴↑𝑁) − 1) = ((𝐴 − 1) · Σ𝑘 ∈ (0...(𝑁 − 1))(𝐴↑𝑘))) |