Proof of Theorem fsumvma2
Step | Hyp | Ref
| Expression |
1 | | fsumvma2.1 |
. 2
⊢ (𝑥 = (𝑝↑𝑘) → 𝐵 = 𝐶) |
2 | | fzfid 12634 |
. 2
⊢ (𝜑 → (1...(⌊‘𝐴)) ∈ Fin) |
3 | | elfznn 12241 |
. . . 4
⊢ (𝑥 ∈
(1...(⌊‘𝐴))
→ 𝑥 ∈
ℕ) |
4 | 3 | ssriv 3572 |
. . 3
⊢
(1...(⌊‘𝐴)) ⊆ ℕ |
5 | 4 | a1i 11 |
. 2
⊢ (𝜑 → (1...(⌊‘𝐴)) ⊆
ℕ) |
6 | | fsumvma2.2 |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) |
7 | | ppifi 24632 |
. . 3
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ)
∈ Fin) |
8 | 6, 7 | syl 17 |
. 2
⊢ (𝜑 → ((0[,]𝐴) ∩ ℙ) ∈
Fin) |
9 | | elin 3758 |
. . . . . 6
⊢ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ↔ (𝑝 ∈ (0[,]𝐴) ∧ 𝑝 ∈ ℙ)) |
10 | 9 | simprbi 479 |
. . . . 5
⊢ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 𝑝 ∈ ℙ) |
11 | | elfznn 12241 |
. . . . 5
⊢ (𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ) |
12 | 10, 11 | anim12i 588 |
. . . 4
⊢ ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) |
13 | 12 | pm4.71ri 663 |
. . 3
⊢ ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))))) |
14 | 6 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝐴 ∈ ℝ) |
15 | | prmnn 15226 |
. . . . . . . . 9
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
16 | 15 | ad2antrl 760 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑝 ∈ ℕ) |
17 | | nnnn0 11176 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
18 | 17 | ad2antll 761 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑘 ∈ ℕ0) |
19 | 16, 18 | nnexpcld 12892 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑𝑘) ∈ ℕ) |
20 | 19 | nnzd 11357 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑𝑘) ∈ ℤ) |
21 | | flge 12468 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝑝↑𝑘) ∈ ℤ) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (𝑝↑𝑘) ≤ (⌊‘𝐴))) |
22 | 14, 20, 21 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (𝑝↑𝑘) ≤ (⌊‘𝐴))) |
23 | | simplrl 796 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑝 ∈ ℙ) |
24 | 23, 15 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑝 ∈ ℕ) |
25 | 24 | nnrpd 11746 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑝 ∈ ℝ+) |
26 | | simplrr 797 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑘 ∈ ℕ) |
27 | 26 | nnzd 11357 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑘 ∈ ℤ) |
28 | | relogexp 24146 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ ℝ+
∧ 𝑘 ∈ ℤ)
→ (log‘(𝑝↑𝑘)) = (𝑘 · (log‘𝑝))) |
29 | 25, 27, 28 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (log‘(𝑝↑𝑘)) = (𝑘 · (log‘𝑝))) |
30 | 29 | breq1d 4593 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((log‘(𝑝↑𝑘)) ≤ (log‘𝐴) ↔ (𝑘 · (log‘𝑝)) ≤ (log‘𝐴))) |
31 | 26 | nnred 10912 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑘 ∈ ℝ) |
32 | 14 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝐴 ∈ ℝ) |
33 | | 0red 9920 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 0 ∈ ℝ) |
34 | 16 | nnred 10912 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑝 ∈ ℝ) |
35 | 34 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑝 ∈ ℝ) |
36 | 24 | nngt0d 10941 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 0 < 𝑝) |
37 | | 0red 9920 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 0 ∈
ℝ) |
38 | | nnnn0 11176 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ ℕ → 𝑝 ∈
ℕ0) |
39 | 16, 38 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑝 ∈ ℕ0) |
40 | 39 | nn0ge0d 11231 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 0 ≤ 𝑝) |
41 | | elicc2 12109 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑝
∈ (0[,]𝐴) ↔
(𝑝 ∈ ℝ ∧ 0
≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) |
42 | | df-3an 1033 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ ℝ ∧ 0 ≤
𝑝 ∧ 𝑝 ≤ 𝐴) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ 𝐴)) |
43 | 41, 42 | syl6bb 275 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑝
∈ (0[,]𝐴) ↔
((𝑝 ∈ ℝ ∧ 0
≤ 𝑝) ∧ 𝑝 ≤ 𝐴))) |
44 | 43 | baibd 946 |
. . . . . . . . . . . . . . 15
⊢ (((0
∈ ℝ ∧ 𝐴
∈ ℝ) ∧ (𝑝
∈ ℝ ∧ 0 ≤ 𝑝)) → (𝑝 ∈ (0[,]𝐴) ↔ 𝑝 ≤ 𝐴)) |
45 | 37, 14, 34, 40, 44 | syl22anc 1319 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝 ∈ (0[,]𝐴) ↔ 𝑝 ≤ 𝐴)) |
46 | 45 | biimpa 500 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑝 ≤ 𝐴) |
47 | 33, 35, 32, 36, 46 | ltletrd 10076 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 0 < 𝐴) |
48 | 32, 47 | elrpd 11745 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝐴 ∈
ℝ+) |
49 | 48 | relogcld 24173 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (log‘𝐴) ∈ ℝ) |
50 | | prmuz2 15246 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) |
51 | | eluzelre 11574 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈
(ℤ≥‘2) → 𝑝 ∈ ℝ) |
52 | | eluz2b2 11637 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈
(ℤ≥‘2) ↔ (𝑝 ∈ ℕ ∧ 1 < 𝑝)) |
53 | 52 | simprbi 479 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈
(ℤ≥‘2) → 1 < 𝑝) |
54 | 51, 53 | rplogcld 24179 |
. . . . . . . . . . 11
⊢ (𝑝 ∈
(ℤ≥‘2) → (log‘𝑝) ∈
ℝ+) |
55 | 23, 50, 54 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (log‘𝑝) ∈
ℝ+) |
56 | 31, 49, 55 | lemuldivd 11797 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((𝑘 · (log‘𝑝)) ≤ (log‘𝐴) ↔ 𝑘 ≤ ((log‘𝐴) / (log‘𝑝)))) |
57 | 49, 55 | rerpdivcld 11779 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ) |
58 | | flge 12468 |
. . . . . . . . . 10
⊢
((((log‘𝐴) /
(log‘𝑝)) ∈
ℝ ∧ 𝑘 ∈
ℤ) → (𝑘 ≤
((log‘𝐴) /
(log‘𝑝)) ↔ 𝑘 ≤
(⌊‘((log‘𝐴) / (log‘𝑝))))) |
59 | 57, 27, 58 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (𝑘 ≤ ((log‘𝐴) / (log‘𝑝)) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
60 | 30, 56, 59 | 3bitrd 293 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((log‘(𝑝↑𝑘)) ≤ (log‘𝐴) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
61 | 19 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (𝑝↑𝑘) ∈ ℕ) |
62 | 61 | nnrpd 11746 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (𝑝↑𝑘) ∈
ℝ+) |
63 | 62, 48 | logled 24177 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (log‘(𝑝↑𝑘)) ≤ (log‘𝐴))) |
64 | | simprr 792 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑘 ∈ ℕ) |
65 | | nnuz 11599 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
66 | 64, 65 | syl6eleq 2698 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑘 ∈
(ℤ≥‘1)) |
67 | 66 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑘 ∈
(ℤ≥‘1)) |
68 | 57 | flcld 12461 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈
ℤ) |
69 | | elfz5 12205 |
. . . . . . . . 9
⊢ ((𝑘 ∈
(ℤ≥‘1) ∧ (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ) →
(𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
70 | 67, 68, 69 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
71 | 60, 63, 70 | 3bitr4d 299 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) |
72 | 71 | pm5.32da 671 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝 ∈ (0[,]𝐴) ∧ (𝑝↑𝑘) ≤ 𝐴) ↔ (𝑝 ∈ (0[,]𝐴) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))))) |
73 | 16 | nncnd 10913 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑝 ∈ ℂ) |
74 | 73 | exp1d 12865 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑1) = 𝑝) |
75 | 16 | nnge1d 10940 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 1 ≤ 𝑝) |
76 | 34, 75, 66 | leexp2ad 12903 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑1) ≤ (𝑝↑𝑘)) |
77 | 74, 76 | eqbrtrrd 4607 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑝 ≤ (𝑝↑𝑘)) |
78 | 19 | nnred 10912 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑𝑘) ∈ ℝ) |
79 | | letr 10010 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℝ ∧ (𝑝↑𝑘) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝑝 ≤ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ≤ 𝐴) → 𝑝 ≤ 𝐴)) |
80 | 34, 78, 14, 79 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝 ≤ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ≤ 𝐴) → 𝑝 ≤ 𝐴)) |
81 | 77, 80 | mpand 707 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝↑𝑘) ≤ 𝐴 → 𝑝 ≤ 𝐴)) |
82 | 81, 45 | sylibrd 248 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝↑𝑘) ≤ 𝐴 → 𝑝 ∈ (0[,]𝐴))) |
83 | 82 | pm4.71rd 665 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (𝑝 ∈ (0[,]𝐴) ∧ (𝑝↑𝑘) ≤ 𝐴))) |
84 | 9 | rbaib 945 |
. . . . . . . 8
⊢ (𝑝 ∈ ℙ → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ↔ 𝑝 ∈ (0[,]𝐴))) |
85 | 84 | ad2antrl 760 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ↔ 𝑝 ∈ (0[,]𝐴))) |
86 | 85 | anbi1d 737 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑝 ∈ (0[,]𝐴) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))))) |
87 | 72, 83, 86 | 3bitr4rd 300 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑝↑𝑘) ≤ 𝐴)) |
88 | 19, 65 | syl6eleq 2698 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑𝑘) ∈
(ℤ≥‘1)) |
89 | 14 | flcld 12461 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (⌊‘𝐴) ∈
ℤ) |
90 | | elfz5 12205 |
. . . . . 6
⊢ (((𝑝↑𝑘) ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ ℤ) → ((𝑝↑𝑘) ∈ (1...(⌊‘𝐴)) ↔ (𝑝↑𝑘) ≤ (⌊‘𝐴))) |
91 | 88, 89, 90 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝↑𝑘) ∈ (1...(⌊‘𝐴)) ↔ (𝑝↑𝑘) ≤ (⌊‘𝐴))) |
92 | 22, 87, 91 | 3bitr4d 299 |
. . . 4
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑝↑𝑘) ∈ (1...(⌊‘𝐴)))) |
93 | 92 | pm5.32da 671 |
. . 3
⊢ (𝜑 → (((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) ↔ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝↑𝑘) ∈ (1...(⌊‘𝐴))))) |
94 | 13, 93 | syl5bb 271 |
. 2
⊢ (𝜑 → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝↑𝑘) ∈ (1...(⌊‘𝐴))))) |
95 | | fsumvma2.3 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (1...(⌊‘𝐴))) → 𝐵 ∈ ℂ) |
96 | | fsumvma2.4 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (1...(⌊‘𝐴)) ∧ (Λ‘𝑥) = 0)) → 𝐵 = 0) |
97 | 1, 2, 5, 8, 94, 95, 96 | fsumvma 24738 |
1
⊢ (𝜑 → Σ𝑥 ∈ (1...(⌊‘𝐴))𝐵 = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))𝐶) |