Proof of Theorem fsumvma2
Step | Hyp | Ref
| Expression |
1 | | fsumvma2.1 |
. 2
⊢ (𝑥 = (𝑝↑𝑘) → 𝐵 = 𝐶) |
2 | | fzfid 12772 |
. 2
⊢ (𝜑 → (1...(⌊‘𝐴)) ∈ Fin) |
3 | | elfznn 12370 |
. . . 4
⊢ (𝑥 ∈
(1...(⌊‘𝐴))
→ 𝑥 ∈
ℕ) |
4 | 3 | ssriv 3607 |
. . 3
⊢
(1...(⌊‘𝐴)) ⊆ ℕ |
5 | 4 | a1i 11 |
. 2
⊢ (𝜑 → (1...(⌊‘𝐴)) ⊆
ℕ) |
6 | | fsumvma2.2 |
. . 3
⊢ (𝜑 → 𝐴 ∈ ℝ) |
7 | | ppifi 24832 |
. . 3
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ)
∈ Fin) |
8 | 6, 7 | syl 17 |
. 2
⊢ (𝜑 → ((0[,]𝐴) ∩ ℙ) ∈
Fin) |
9 | | elin 3796 |
. . . . . 6
⊢ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ↔ (𝑝 ∈ (0[,]𝐴) ∧ 𝑝 ∈ ℙ)) |
10 | 9 | simprbi 480 |
. . . . 5
⊢ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) → 𝑝 ∈ ℙ) |
11 | | elfznn 12370 |
. . . . 5
⊢ (𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ) |
12 | 10, 11 | anim12i 590 |
. . . 4
⊢ ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) → (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) |
13 | 12 | pm4.71ri 665 |
. . 3
⊢ ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))))) |
14 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝐴 ∈ ℝ) |
15 | | prmnn 15388 |
. . . . . . . . 9
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
16 | 15 | ad2antrl 764 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑝 ∈ ℕ) |
17 | | nnnn0 11299 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℕ0) |
18 | 17 | ad2antll 765 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑘 ∈ ℕ0) |
19 | 16, 18 | nnexpcld 13030 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑𝑘) ∈ ℕ) |
20 | 19 | nnzd 11481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑𝑘) ∈ ℤ) |
21 | | flge 12606 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝑝↑𝑘) ∈ ℤ) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (𝑝↑𝑘) ≤ (⌊‘𝐴))) |
22 | 14, 20, 21 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (𝑝↑𝑘) ≤ (⌊‘𝐴))) |
23 | | simplrl 800 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑝 ∈ ℙ) |
24 | 23, 15 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑝 ∈ ℕ) |
25 | 24 | nnrpd 11870 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑝 ∈ ℝ+) |
26 | | simplrr 801 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑘 ∈ ℕ) |
27 | 26 | nnzd 11481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑘 ∈ ℤ) |
28 | | relogexp 24342 |
. . . . . . . . . . 11
⊢ ((𝑝 ∈ ℝ+
∧ 𝑘 ∈ ℤ)
→ (log‘(𝑝↑𝑘)) = (𝑘 · (log‘𝑝))) |
29 | 25, 27, 28 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (log‘(𝑝↑𝑘)) = (𝑘 · (log‘𝑝))) |
30 | 29 | breq1d 4663 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((log‘(𝑝↑𝑘)) ≤ (log‘𝐴) ↔ (𝑘 · (log‘𝑝)) ≤ (log‘𝐴))) |
31 | 26 | nnred 11035 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑘 ∈ ℝ) |
32 | 14 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝐴 ∈ ℝ) |
33 | | 0red 10041 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 0 ∈ ℝ) |
34 | 16 | nnred 11035 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑝 ∈ ℝ) |
35 | 34 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑝 ∈ ℝ) |
36 | 24 | nngt0d 11064 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 0 < 𝑝) |
37 | | 0red 10041 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 0 ∈
ℝ) |
38 | | nnnn0 11299 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ ℕ → 𝑝 ∈
ℕ0) |
39 | 16, 38 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑝 ∈ ℕ0) |
40 | 39 | nn0ge0d 11354 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 0 ≤ 𝑝) |
41 | | elicc2 12238 |
. . . . . . . . . . . . . . . . 17
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑝
∈ (0[,]𝐴) ↔
(𝑝 ∈ ℝ ∧ 0
≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) |
42 | | df-3an 1039 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑝 ∈ ℝ ∧ 0 ≤
𝑝 ∧ 𝑝 ≤ 𝐴) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ 𝐴)) |
43 | 41, 42 | syl6bb 276 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑝
∈ (0[,]𝐴) ↔
((𝑝 ∈ ℝ ∧ 0
≤ 𝑝) ∧ 𝑝 ≤ 𝐴))) |
44 | 43 | baibd 948 |
. . . . . . . . . . . . . . 15
⊢ (((0
∈ ℝ ∧ 𝐴
∈ ℝ) ∧ (𝑝
∈ ℝ ∧ 0 ≤ 𝑝)) → (𝑝 ∈ (0[,]𝐴) ↔ 𝑝 ≤ 𝐴)) |
45 | 37, 14, 34, 40, 44 | syl22anc 1327 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝 ∈ (0[,]𝐴) ↔ 𝑝 ≤ 𝐴)) |
46 | 45 | biimpa 501 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑝 ≤ 𝐴) |
47 | 33, 35, 32, 36, 46 | ltletrd 10197 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 0 < 𝐴) |
48 | 32, 47 | elrpd 11869 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝐴 ∈
ℝ+) |
49 | 48 | relogcld 24369 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (log‘𝐴) ∈ ℝ) |
50 | | prmuz2 15408 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) |
51 | | eluzelre 11698 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈
(ℤ≥‘2) → 𝑝 ∈ ℝ) |
52 | | eluz2b2 11761 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈
(ℤ≥‘2) ↔ (𝑝 ∈ ℕ ∧ 1 < 𝑝)) |
53 | 52 | simprbi 480 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈
(ℤ≥‘2) → 1 < 𝑝) |
54 | 51, 53 | rplogcld 24375 |
. . . . . . . . . . 11
⊢ (𝑝 ∈
(ℤ≥‘2) → (log‘𝑝) ∈
ℝ+) |
55 | 23, 50, 54 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (log‘𝑝) ∈
ℝ+) |
56 | 31, 49, 55 | lemuldivd 11921 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((𝑘 · (log‘𝑝)) ≤ (log‘𝐴) ↔ 𝑘 ≤ ((log‘𝐴) / (log‘𝑝)))) |
57 | 49, 55 | rerpdivcld 11903 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ) |
58 | | flge 12606 |
. . . . . . . . . 10
⊢
((((log‘𝐴) /
(log‘𝑝)) ∈
ℝ ∧ 𝑘 ∈
ℤ) → (𝑘 ≤
((log‘𝐴) /
(log‘𝑝)) ↔ 𝑘 ≤
(⌊‘((log‘𝐴) / (log‘𝑝))))) |
59 | 57, 27, 58 | syl2anc 693 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (𝑘 ≤ ((log‘𝐴) / (log‘𝑝)) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
60 | 30, 56, 59 | 3bitrd 294 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((log‘(𝑝↑𝑘)) ≤ (log‘𝐴) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
61 | 19 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (𝑝↑𝑘) ∈ ℕ) |
62 | 61 | nnrpd 11870 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (𝑝↑𝑘) ∈
ℝ+) |
63 | 62, 48 | logled 24373 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (log‘(𝑝↑𝑘)) ≤ (log‘𝐴))) |
64 | | simprr 796 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑘 ∈ ℕ) |
65 | | nnuz 11723 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
66 | 64, 65 | syl6eleq 2711 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑘 ∈
(ℤ≥‘1)) |
67 | 66 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → 𝑘 ∈
(ℤ≥‘1)) |
68 | 57 | flcld 12599 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈
ℤ) |
69 | | elfz5 12334 |
. . . . . . . . 9
⊢ ((𝑘 ∈
(ℤ≥‘1) ∧ (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℤ) →
(𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
70 | 67, 68, 69 | syl2anc 693 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → (𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ↔ 𝑘 ≤ (⌊‘((log‘𝐴) / (log‘𝑝))))) |
71 | 60, 63, 70 | 3bitr4d 300 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) ∧ 𝑝 ∈ (0[,]𝐴)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) |
72 | 71 | pm5.32da 673 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝 ∈ (0[,]𝐴) ∧ (𝑝↑𝑘) ≤ 𝐴) ↔ (𝑝 ∈ (0[,]𝐴) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))))) |
73 | 16 | nncnd 11036 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑝 ∈ ℂ) |
74 | 73 | exp1d 13003 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑1) = 𝑝) |
75 | 16 | nnge1d 11063 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 1 ≤ 𝑝) |
76 | 34, 75, 66 | leexp2ad 13041 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑1) ≤ (𝑝↑𝑘)) |
77 | 74, 76 | eqbrtrrd 4677 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → 𝑝 ≤ (𝑝↑𝑘)) |
78 | 19 | nnred 11035 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑𝑘) ∈ ℝ) |
79 | | letr 10131 |
. . . . . . . . . 10
⊢ ((𝑝 ∈ ℝ ∧ (𝑝↑𝑘) ∈ ℝ ∧ 𝐴 ∈ ℝ) → ((𝑝 ≤ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ≤ 𝐴) → 𝑝 ≤ 𝐴)) |
80 | 34, 78, 14, 79 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝 ≤ (𝑝↑𝑘) ∧ (𝑝↑𝑘) ≤ 𝐴) → 𝑝 ≤ 𝐴)) |
81 | 77, 80 | mpand 711 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝↑𝑘) ≤ 𝐴 → 𝑝 ≤ 𝐴)) |
82 | 81, 45 | sylibrd 249 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝↑𝑘) ≤ 𝐴 → 𝑝 ∈ (0[,]𝐴))) |
83 | 82 | pm4.71rd 667 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝↑𝑘) ≤ 𝐴 ↔ (𝑝 ∈ (0[,]𝐴) ∧ (𝑝↑𝑘) ≤ 𝐴))) |
84 | 9 | rbaib 947 |
. . . . . . . 8
⊢ (𝑝 ∈ ℙ → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ↔ 𝑝 ∈ (0[,]𝐴))) |
85 | 84 | ad2antrl 764 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ↔ 𝑝 ∈ (0[,]𝐴))) |
86 | 85 | anbi1d 741 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑝 ∈ (0[,]𝐴) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))))) |
87 | 72, 83, 86 | 3bitr4rd 301 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑝↑𝑘) ≤ 𝐴)) |
88 | 19, 65 | syl6eleq 2711 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (𝑝↑𝑘) ∈
(ℤ≥‘1)) |
89 | 14 | flcld 12599 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → (⌊‘𝐴) ∈
ℤ) |
90 | | elfz5 12334 |
. . . . . 6
⊢ (((𝑝↑𝑘) ∈ (ℤ≥‘1)
∧ (⌊‘𝐴)
∈ ℤ) → ((𝑝↑𝑘) ∈ (1...(⌊‘𝐴)) ↔ (𝑝↑𝑘) ≤ (⌊‘𝐴))) |
91 | 88, 89, 90 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝↑𝑘) ∈ (1...(⌊‘𝐴)) ↔ (𝑝↑𝑘) ≤ (⌊‘𝐴))) |
92 | 22, 87, 91 | 3bitr4d 300 |
. . . 4
⊢ ((𝜑 ∧ (𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ)) → ((𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) ↔ (𝑝↑𝑘) ∈ (1...(⌊‘𝐴)))) |
93 | 92 | pm5.32da 673 |
. . 3
⊢ (𝜑 → (((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝 ∈ ((0[,]𝐴) ∩ ℙ) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝)))))) ↔ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) ∧ (𝑝↑𝑘) ∈ (1...(⌊‘𝐴))))) |
94 | 13, 93 | syl5bb 272 |
. 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 24938 |
1
⊢ (𝜑 → Σ𝑥 ∈ (1...(⌊‘𝐴))𝐵 = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))𝐶) |