Step | Hyp | Ref
| Expression |
1 | | chpval 24848 |
. 2
⊢ (𝐴 ∈ ℝ →
(ψ‘𝐴) =
Σ𝑛 ∈
(1...(⌊‘𝐴))(Λ‘𝑛)) |
2 | | fveq2 6191 |
. . 3
⊢ (𝑛 = (𝑝↑𝑘) → (Λ‘𝑛) = (Λ‘(𝑝↑𝑘))) |
3 | | id 22 |
. . 3
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ) |
4 | | elfznn 12370 |
. . . . . 6
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) |
5 | 4 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝑛 ∈
ℕ) |
6 | | vmacl 24844 |
. . . . 5
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (Λ‘𝑛)
∈ ℝ) |
8 | 7 | recnd 10068 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (Λ‘𝑛)
∈ ℂ) |
9 | | simprr 796 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → (Λ‘𝑛) = 0) |
10 | 2, 3, 8, 9 | fsumvma2 24939 |
. 2
⊢ (𝐴 ∈ ℝ →
Σ𝑛 ∈
(1...(⌊‘𝐴))(Λ‘𝑛) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(Λ‘(𝑝↑𝑘))) |
11 | | inss2 3834 |
. . . . . . 7
⊢
((0[,]𝐴) ∩
ℙ) ⊆ ℙ |
12 | | simpr 477 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) |
13 | 11, 12 | sseldi 3601 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ) |
14 | | elfznn 12370 |
. . . . . 6
⊢ (𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ) |
15 | | vmappw 24842 |
. . . . . 6
⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) →
(Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
16 | 13, 14, 15 | syl2an 494 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) →
(Λ‘(𝑝↑𝑘)) = (log‘𝑝)) |
17 | 16 | sumeq2dv 14433 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(Λ‘(𝑝↑𝑘)) = Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝)) |
18 | | fzfid 12772 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin) |
19 | | prmuz2 15408 |
. . . . . . . 8
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) |
20 | | eluzelre 11698 |
. . . . . . . . 9
⊢ (𝑝 ∈
(ℤ≥‘2) → 𝑝 ∈ ℝ) |
21 | | eluz2b2 11761 |
. . . . . . . . . 10
⊢ (𝑝 ∈
(ℤ≥‘2) ↔ (𝑝 ∈ ℕ ∧ 1 < 𝑝)) |
22 | 21 | simprbi 480 |
. . . . . . . . 9
⊢ (𝑝 ∈
(ℤ≥‘2) → 1 < 𝑝) |
23 | 20, 22 | rplogcld 24375 |
. . . . . . . 8
⊢ (𝑝 ∈
(ℤ≥‘2) → (log‘𝑝) ∈
ℝ+) |
24 | 13, 19, 23 | 3syl 18 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℝ+) |
25 | 24 | rpcnd 11874 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℂ) |
26 | | fsumconst 14522 |
. . . . . 6
⊢
(((1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin ∧ (log‘𝑝) ∈ ℂ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝) =
((#‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) · (log‘𝑝))) |
27 | 18, 25, 26 | syl2anc 693 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝) =
((#‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) · (log‘𝑝))) |
28 | | ppisval 24830 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ) =
((2...(⌊‘𝐴))
∩ ℙ)) |
29 | | inss1 3833 |
. . . . . . . . . . . . . 14
⊢
((2...(⌊‘𝐴)) ∩ ℙ) ⊆
(2...(⌊‘𝐴)) |
30 | 28, 29 | syl6eqss 3655 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ)
⊆ (2...(⌊‘𝐴))) |
31 | 30 | sselda 3603 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (2...(⌊‘𝐴))) |
32 | | elfzuz2 12346 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈
(2...(⌊‘𝐴))
→ (⌊‘𝐴)
∈ (ℤ≥‘2)) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘𝐴) ∈
(ℤ≥‘2)) |
34 | | simpl 473 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 𝐴 ∈ ℝ) |
35 | | 0red 10041 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 0 ∈ ℝ) |
36 | | 2re 11090 |
. . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ |
37 | 36 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 2 ∈ ℝ) |
38 | | 2pos 11112 |
. . . . . . . . . . . . . 14
⊢ 0 <
2 |
39 | 38 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 0 < 2) |
40 | | eluzle 11700 |
. . . . . . . . . . . . . . 15
⊢
((⌊‘𝐴)
∈ (ℤ≥‘2) → 2 ≤ (⌊‘𝐴)) |
41 | | 2z 11409 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ |
42 | | flge 12606 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ ∧ 2 ∈
ℤ) → (2 ≤ 𝐴
↔ 2 ≤ (⌊‘𝐴))) |
43 | 41, 42 | mpan2 707 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ → (2 ≤
𝐴 ↔ 2 ≤
(⌊‘𝐴))) |
44 | 40, 43 | syl5ibr 236 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ →
((⌊‘𝐴) ∈
(ℤ≥‘2) → 2 ≤ 𝐴)) |
45 | 44 | imp 445 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 2 ≤ 𝐴) |
46 | 35, 37, 34, 39, 45 | ltletrd 10197 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 0 < 𝐴) |
47 | 34, 46 | elrpd 11869 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 𝐴 ∈
ℝ+) |
48 | 33, 47 | syldan 487 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈
ℝ+) |
49 | 48 | relogcld 24369 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈
ℝ) |
50 | 49, 24 | rerpdivcld 11903 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈
ℝ) |
51 | | 1red 10055 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 1 ∈ ℝ) |
52 | | 1lt2 11194 |
. . . . . . . . . . . . . 14
⊢ 1 <
2 |
53 | 52 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 1 < 2) |
54 | 51, 37, 34, 53, 45 | ltletrd 10197 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 1 < 𝐴) |
55 | 33, 54 | syldan 487 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝐴) |
56 | | rplogcl 24350 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 1 <
𝐴) → (log‘𝐴) ∈
ℝ+) |
57 | 55, 56 | syldan 487 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈
ℝ+) |
58 | 57, 24 | rpdivcld 11889 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈
ℝ+) |
59 | 58 | rpge0d 11876 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 ≤
((log‘𝐴) /
(log‘𝑝))) |
60 | | flge0nn0 12621 |
. . . . . . . 8
⊢
((((log‘𝐴) /
(log‘𝑝)) ∈
ℝ ∧ 0 ≤ ((log‘𝐴) / (log‘𝑝))) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈
ℕ0) |
61 | 50, 59, 60 | syl2anc 693 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈
ℕ0) |
62 | | hashfz1 13134 |
. . . . . . 7
⊢
((⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℕ0 →
(#‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) = (⌊‘((log‘𝐴) / (log‘𝑝)))) |
63 | 61, 62 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(#‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) = (⌊‘((log‘𝐴) / (log‘𝑝)))) |
64 | 63 | oveq1d 6665 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((#‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) · (log‘𝑝)) = ((⌊‘((log‘𝐴) / (log‘𝑝))) · (log‘𝑝))) |
65 | 61 | nn0cnd 11353 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℂ) |
66 | 65, 25 | mulcomd 10061 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((⌊‘((log‘𝐴) / (log‘𝑝))) · (log‘𝑝)) = ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝))))) |
67 | 27, 64, 66 | 3eqtrd 2660 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝) = ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝))))) |
68 | 17, 67 | eqtrd 2656 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(Λ‘(𝑝↑𝑘)) = ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝))))) |
69 | 68 | sumeq2dv 14433 |
. 2
⊢ (𝐴 ∈ ℝ →
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(Λ‘(𝑝↑𝑘)) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝))))) |
70 | 1, 10, 69 | 3eqtrd 2660 |
1
⊢ (𝐴 ∈ ℝ →
(ψ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩
ℙ)((log‘𝑝)
· (⌊‘((log‘𝐴) / (log‘𝑝))))) |