Proof of Theorem fsumvma2
| Step | Hyp | Ref
| Expression |
| 1 | | fsumvma2.1 |
. 2
⊢ (𝑥 = (𝑝↑𝑘) → 𝐵 = 𝐶) |
| 2 | | fzfid 14014 |
. 2
⊢ (𝜑 → (1...(⌊‘𝐴)) ∈ Fin) |
| 3 | | fz1ssnn 13595 |
. . 3
⊢
(1...(⌊‘𝐴)) ⊆ ℕ |
| 4 | 3 | a1i 11 |
. 2
⊢ (𝜑 → (1...(⌊‘𝐴)) ⊆
ℕ) |
| 5 | | fsumvma2.2 |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 6 | | ppifi 27149 |
. . 3
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ)
∈ Fin) |
| 7 | 5, 6 | syl 17 |
. 2
⊢ (𝜑 → ((0[,]𝐴) ∩ ℙ) ∈
Fin) |
| 8 | | elinel2 4202 |
. . . . 5
⊢ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 𝑝 ∈ ℙ) |
| 9 | | elfznn 13593 |
. . . . 5
⊢ (𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ) |
| 10 | 8, 9 | anim12i 613 |
. . . 4
⊢ ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) |
| 11 | 10 | pm4.71ri 560 |
. . 3
⊢ ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))))) |
| 12 | 5 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝐴 ∈ ℝ) |
| 13 | | prmnn 16711 |
. . . . . . . . 9
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
| 14 | 13 | ad2antrl 728 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑝 ∈ ℕ) |
| 15 | | nnnn0 12533 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
| 16 | 15 | ad2antll 729 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑘 ∈ ℕ0) |
| 17 | 14, 16 | nnexpcld 14284 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑𝑘) ∈ ℕ) |
| 18 | 17 | nnzd 12640 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑𝑘) ∈ ℤ) |
| 19 | | flge 13845 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝑝↑𝑘) ∈ ℤ) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (𝑝↑𝑘) ≤ (⌊‘𝐴))) |
| 20 | 12, 18, 19 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (𝑝↑𝑘) ≤ (⌊‘𝐴))) |
| 21 | | simplrl 777 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑝 ∈ ℙ) |
| 22 | 21, 13 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑝 ∈ ℕ) |
| 23 | 22 | nnrpd 13075 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑝 ∈ ℝ+) |
| 24 | | simplrr 778 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑘 ∈ ℕ) |
| 25 | 24 | nnzd 12640 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑘 ∈ ℤ) |
| 26 | | relogexp 26638 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ ℝ+
∧ 𝑘 ∈ ℤ)
→ (log‘(𝑝↑𝑘)) = (𝑘 · (log‘𝑝))) |
| 27 | 23, 25, 26 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (log‘(𝑝↑𝑘)) = (𝑘 · (log‘𝑝))) |
| 28 | 27 | breq1d 5153 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((log‘(𝑝↑𝑘)) ≤ (log‘𝐴) ↔ (𝑘 · (log‘𝑝)) ≤ (log‘𝐴))) |
| 29 | 24 | nnred 12281 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑘 ∈ ℝ) |
| 30 | 12 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝐴 ∈ ℝ) |
| 31 | | 0red 11264 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 0 ∈ ℝ) |
| 32 | 14 | nnred 12281 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑝 ∈ ℝ) |
| 33 | 32 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑝 ∈ ℝ) |
| 34 | 22 | nngt0d 12315 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 0 < 𝑝) |
| 35 | | 0red 11264 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 0 ∈
ℝ) |
| 36 | 14 | nnnn0d 12587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑝 ∈ ℕ0) |
| 37 | 36 | nn0ge0d 12590 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 0 ≤ 𝑝) |
| 38 | | elicc2 13452 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑝
∈ (0[,]𝐴) ↔
(𝑝 ∈ ℝ ∧ 0
≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) |
| 39 | | df-3an 1089 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ ℝ ∧ 0 ≤
𝑝 ∧ 𝑝 ≤ 𝐴) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ 𝐴)) |
| 40 | 38, 39 | bitrdi 287 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑝
∈ (0[,]𝐴) ↔
((𝑝 ∈ ℝ ∧ 0
≤ 𝑝) ∧ 𝑝 ≤ 𝐴))) |
| 41 | 40 | baibd 539 |
. . . . . . . . . . . . . . 15
⊢ (((0
∈ ℝ ∧ 𝐴
∈ ℝ) ∧ (𝑝
∈ ℝ ∧ 0 ≤ 𝑝)) → (𝑝 ∈ (0[,]𝐴) ↔ 𝑝 ≤ 𝐴)) |
| 42 | 35, 12, 32, 37, 41 | syl22anc 839 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝 ∈ (0[,]𝐴) ↔ 𝑝 ≤ 𝐴)) |
| 43 | 42 | biimpa 476 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑝 ≤ 𝐴) |
| 44 | 31, 33, 30, 34, 43 | ltletrd 11421 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 0 < 𝐴) |
| 45 | 30, 44 | elrpd 13074 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝐴 ∈
ℝ+) |
| 46 | 45 | relogcld 26665 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (log‘𝐴) ∈ ℝ) |
| 47 | | prmuz2 16733 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) |
| 48 | | eluzelre 12889 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈
(ℤ≥‘2) → 𝑝 ∈ ℝ) |
| 49 | | eluz2gt1 12962 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈
(ℤ≥‘2) → 1 < 𝑝) |
| 50 | 48, 49 | rplogcld 26671 |
. . . . . . . . . . 11
⊢ (𝑝 ∈
(ℤ≥‘2) → (log‘𝑝) ∈
ℝ+) |
| 51 | 21, 47, 50 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (log‘𝑝) ∈
ℝ+) |
| 52 | 29, 46, 51 | lemuldivd 13126 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((𝑘 · (log‘𝑝)) ≤ (log‘𝐴) ↔ 𝑘 ≤ ((log‘𝐴) / (log‘𝑝)))) |
| 53 | 46, 51 | rerpdivcld 13108 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ) |
| 54 | | flge 13845 |
. . . . . . . . . 10
⊢
((((log‘𝐴) /
(log‘𝑝)) ∈
ℝ ∧ 𝑘 ∈
ℤ) → (𝑘 ≤
((log‘𝐴) /
(log‘𝑝)) ↔ 𝑘 ≤
(⌊‘((log‘𝐴) / (log‘𝑝))))) |
| 55 | 53, 25, 54 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (𝑘 ≤ ((log‘𝐴) / (log‘𝑝)) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
| 56 | 28, 52, 55 | 3bitrd 305 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((log‘(𝑝↑𝑘)) ≤ (log‘𝐴) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
| 57 | 17 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (𝑝↑𝑘) ∈ ℕ) |
| 58 | 57 | nnrpd 13075 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (𝑝↑𝑘) ∈
ℝ+) |
| 59 | 58, 45 | logled 26669 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (log‘(𝑝↑𝑘)) ≤ (log‘𝐴))) |
| 60 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑘 ∈ ℕ) |
| 61 | | nnuz 12921 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
| 62 | 60, 61 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑘 ∈
(ℤ≥‘1)) |
| 63 | 62 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑘 ∈
(ℤ≥‘1)) |
| 64 | 53 | flcld 13838 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈
ℤ) |
| 65 | | elfz5 13556 |
. . . . . . . . 9
⊢ ((𝑘 ∈
(ℤ≥‘1) ∧ (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ) →
(𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
| 66 | 63, 64, 65 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
| 67 | 56, 59, 66 | 3bitr4d 311 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) |
| 68 | 67 | pm5.32da 579 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝 ∈ (0[,]𝐴) ∧ (𝑝↑𝑘) ≤ 𝐴) ↔ (𝑝 ∈ (0[,]𝐴) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))))) |
| 69 | 14 | nncnd 12282 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑝 ∈ ℂ) |
| 70 | 69 | exp1d 14181 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑1) = 𝑝) |
| 71 | 14 | nnge1d 12314 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 1 ≤ 𝑝) |
| 72 | 32, 71, 62 | leexp2ad 14293 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑1) ≤ (𝑝↑𝑘)) |
| 73 | 70, 72 | eqbrtrrd 5167 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑝 ≤ (𝑝↑𝑘)) |
| 74 | 17 | nnred 12281 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑𝑘) ∈ ℝ) |
| 75 | | letr 11355 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℝ ∧ (𝑝↑𝑘) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝑝 ≤ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ≤ 𝐴) → 𝑝 ≤ 𝐴)) |
| 76 | 32, 74, 12, 75 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝 ≤ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ≤ 𝐴) → 𝑝 ≤ 𝐴)) |
| 77 | 73, 76 | mpand 695 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝↑𝑘) ≤ 𝐴 → 𝑝 ≤ 𝐴)) |
| 78 | 77, 42 | sylibrd 259 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝↑𝑘) ≤ 𝐴 → 𝑝 ∈ (0[,]𝐴))) |
| 79 | 78 | pm4.71rd 562 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (𝑝 ∈ (0[,]𝐴) ∧ (𝑝↑𝑘) ≤ 𝐴))) |
| 80 | | elin 3967 |
. . . . . . . . 9
⊢ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ↔ (𝑝 ∈ (0[,]𝐴) ∧ 𝑝 ∈ ℙ)) |
| 81 | 80 | rbaib 538 |
. . . . . . . 8
⊢ (𝑝 ∈ ℙ → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ↔ 𝑝 ∈ (0[,]𝐴))) |
| 82 | 81 | ad2antrl 728 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ↔ 𝑝 ∈ (0[,]𝐴))) |
| 83 | 82 | anbi1d 631 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑝 ∈ (0[,]𝐴) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))))) |
| 84 | 68, 79, 83 | 3bitr4rd 312 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑝↑𝑘) ≤ 𝐴)) |
| 85 | 17, 61 | eleqtrdi 2851 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑𝑘) ∈
(ℤ≥‘1)) |
| 86 | 12 | flcld 13838 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (⌊‘𝐴) ∈
ℤ) |
| 87 | | elfz5 13556 |
. . . . . 6
⊢ (((𝑝↑𝑘) ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ ℤ) → ((𝑝↑𝑘) ∈ (1...(⌊‘𝐴)) ↔ (𝑝↑𝑘) ≤ (⌊‘𝐴))) |
| 88 | 85, 86, 87 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝↑𝑘) ∈ (1...(⌊‘𝐴)) ↔ (𝑝↑𝑘) ≤ (⌊‘𝐴))) |
| 89 | 20, 84, 88 | 3bitr4d 311 |
. . . 4
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑝↑𝑘) ∈ (1...(⌊‘𝐴)))) |
| 90 | 89 | pm5.32da 579 |
. . 3
⊢ (𝜑 → (((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) ↔ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝↑𝑘) ∈ (1...(⌊‘𝐴))))) |
| 91 | 11, 90 | bitrid 283 |
. 2
⊢ (𝜑 → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝↑𝑘) ∈ (1...(⌊‘𝐴))))) |
| 92 | | fsumvma2.3 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(⌊‘𝐴))) → 𝐵 ∈ ℂ) |
| 93 | | fsumvma2.4 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑥) = 0)) → 𝐵 = 0) |
| 94 | 1, 2, 4, 7, 91, 92, 93 | fsumvma 27257 |
1
⊢ (𝜑 → Σ𝑥 ∈ (1...(⌊‘𝐴))𝐵 = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))𝐶) |