| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | chpval 27166 | . 2
⊢ (𝐴 ∈ ℝ →
(ψ‘𝐴) =
Σ𝑛 ∈
(1...(⌊‘𝐴))(Λ‘𝑛)) | 
| 2 |  | fveq2 6905 | . . 3
⊢ (𝑛 = (𝑝↑𝑘) → (Λ‘𝑛) = (Λ‘(𝑝↑𝑘))) | 
| 3 |  | id 22 | . . 3
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℝ) | 
| 4 |  | elfznn 13594 | . . . . . 6
⊢ (𝑛 ∈
(1...(⌊‘𝐴))
→ 𝑛 ∈
ℕ) | 
| 5 | 4 | adantl 481 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ 𝑛 ∈
ℕ) | 
| 6 |  | vmacl 27162 | . . . . 5
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) | 
| 7 | 5, 6 | syl 17 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (Λ‘𝑛)
∈ ℝ) | 
| 8 | 7 | recnd 11290 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑛 ∈
(1...(⌊‘𝐴)))
→ (Λ‘𝑛)
∈ ℂ) | 
| 9 |  | simprr 772 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ (𝑛 ∈
(1...(⌊‘𝐴))
∧ (Λ‘𝑛) =
0)) → (Λ‘𝑛) = 0) | 
| 10 | 2, 3, 8, 9 | fsumvma2 27259 | . 2
⊢ (𝐴 ∈ ℝ →
Σ𝑛 ∈
(1...(⌊‘𝐴))(Λ‘𝑛) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(Λ‘(𝑝↑𝑘))) | 
| 11 |  | simpr 484 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) | 
| 12 | 11 | elin2d 4204 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ) | 
| 13 |  | elfznn 13594 | . . . . . 6
⊢ (𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) → 𝑘 ∈ ℕ) | 
| 14 |  | vmappw 27160 | . . . . . 6
⊢ ((𝑝 ∈ ℙ ∧ 𝑘 ∈ ℕ) →
(Λ‘(𝑝↑𝑘)) = (log‘𝑝)) | 
| 15 | 12, 13, 14 | syl2an 596 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) ∧ 𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))) →
(Λ‘(𝑝↑𝑘)) = (log‘𝑝)) | 
| 16 | 15 | sumeq2dv 15739 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(Λ‘(𝑝↑𝑘)) = Σ𝑘 ∈ (1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝)) | 
| 17 |  | fzfid 14015 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin) | 
| 18 |  | prmuz2 16734 | . . . . . . . 8
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) | 
| 19 |  | eluzelre 12890 | . . . . . . . . 9
⊢ (𝑝 ∈
(ℤ≥‘2) → 𝑝 ∈ ℝ) | 
| 20 |  | eluz2gt1 12963 | . . . . . . . . 9
⊢ (𝑝 ∈
(ℤ≥‘2) → 1 < 𝑝) | 
| 21 | 19, 20 | rplogcld 26672 | . . . . . . . 8
⊢ (𝑝 ∈
(ℤ≥‘2) → (log‘𝑝) ∈
ℝ+) | 
| 22 | 12, 18, 21 | 3syl 18 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℝ+) | 
| 23 | 22 | rpcnd 13080 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℂ) | 
| 24 |  | fsumconst 15827 | . . . . . 6
⊢
(((1...(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ Fin ∧ (log‘𝑝) ∈ ℂ) →
Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝) =
((♯‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) · (log‘𝑝))) | 
| 25 | 17, 23, 24 | syl2anc 584 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝) =
((♯‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) · (log‘𝑝))) | 
| 26 |  | ppisval 27148 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ) =
((2...(⌊‘𝐴))
∩ ℙ)) | 
| 27 |  | inss1 4236 | . . . . . . . . . . . . . 14
⊢
((2...(⌊‘𝐴)) ∩ ℙ) ⊆
(2...(⌊‘𝐴)) | 
| 28 | 26, 27 | eqsstrdi 4027 | . . . . . . . . . . . . 13
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ)
⊆ (2...(⌊‘𝐴))) | 
| 29 | 28 | sselda 3982 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (2...(⌊‘𝐴))) | 
| 30 |  | elfzuz2 13570 | . . . . . . . . . . . 12
⊢ (𝑝 ∈
(2...(⌊‘𝐴))
→ (⌊‘𝐴)
∈ (ℤ≥‘2)) | 
| 31 | 29, 30 | syl 17 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘𝐴) ∈
(ℤ≥‘2)) | 
| 32 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 𝐴 ∈ ℝ) | 
| 33 |  | 0red 11265 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 0 ∈ ℝ) | 
| 34 |  | 2re 12341 | . . . . . . . . . . . . . 14
⊢ 2 ∈
ℝ | 
| 35 | 34 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 2 ∈ ℝ) | 
| 36 |  | 2pos 12370 | . . . . . . . . . . . . . 14
⊢ 0 <
2 | 
| 37 | 36 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 0 < 2) | 
| 38 |  | eluzle 12892 | . . . . . . . . . . . . . . 15
⊢
((⌊‘𝐴)
∈ (ℤ≥‘2) → 2 ≤ (⌊‘𝐴)) | 
| 39 |  | 2z 12651 | . . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℤ | 
| 40 |  | flge 13846 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ ∧ 2 ∈
ℤ) → (2 ≤ 𝐴
↔ 2 ≤ (⌊‘𝐴))) | 
| 41 | 39, 40 | mpan2 691 | . . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℝ → (2 ≤
𝐴 ↔ 2 ≤
(⌊‘𝐴))) | 
| 42 | 38, 41 | imbitrrid 246 | . . . . . . . . . . . . . 14
⊢ (𝐴 ∈ ℝ →
((⌊‘𝐴) ∈
(ℤ≥‘2) → 2 ≤ 𝐴)) | 
| 43 | 42 | imp 406 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 2 ≤ 𝐴) | 
| 44 | 33, 35, 32, 37, 43 | ltletrd 11422 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 0 < 𝐴) | 
| 45 | 32, 44 | elrpd 13075 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 𝐴 ∈
ℝ+) | 
| 46 | 31, 45 | syldan 591 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈
ℝ+) | 
| 47 | 46 | relogcld 26666 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈
ℝ) | 
| 48 | 47, 22 | rerpdivcld 13109 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈
ℝ) | 
| 49 |  | 1red 11263 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 1 ∈ ℝ) | 
| 50 |  | 1lt2 12438 | . . . . . . . . . . . . . 14
⊢ 1 <
2 | 
| 51 | 50 | a1i 11 | . . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 1 < 2) | 
| 52 | 49, 35, 32, 51, 43 | ltletrd 11422 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧
(⌊‘𝐴) ∈
(ℤ≥‘2)) → 1 < 𝐴) | 
| 53 | 31, 52 | syldan 591 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝐴) | 
| 54 |  | rplogcl 26647 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 1 <
𝐴) → (log‘𝐴) ∈
ℝ+) | 
| 55 | 53, 54 | syldan 591 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈
ℝ+) | 
| 56 | 55, 22 | rpdivcld 13095 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈
ℝ+) | 
| 57 | 56 | rpge0d 13082 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 0 ≤
((log‘𝐴) /
(log‘𝑝))) | 
| 58 |  | flge0nn0 13861 | . . . . . . . 8
⊢
((((log‘𝐴) /
(log‘𝑝)) ∈
ℝ ∧ 0 ≤ ((log‘𝐴) / (log‘𝑝))) → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈
ℕ0) | 
| 59 | 48, 57, 58 | syl2anc 584 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈
ℕ0) | 
| 60 |  | hashfz1 14386 | . . . . . . 7
⊢
((⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℕ0 →
(♯‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) = (⌊‘((log‘𝐴) / (log‘𝑝)))) | 
| 61 | 59, 60 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(♯‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) = (⌊‘((log‘𝐴) / (log‘𝑝)))) | 
| 62 | 61 | oveq1d 7447 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((♯‘(1...(⌊‘((log‘𝐴) / (log‘𝑝))))) · (log‘𝑝)) = ((⌊‘((log‘𝐴) / (log‘𝑝))) · (log‘𝑝))) | 
| 63 | 59 | nn0cnd 12591 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℂ) | 
| 64 | 63, 23 | mulcomd 11283 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
((⌊‘((log‘𝐴) / (log‘𝑝))) · (log‘𝑝)) = ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝))))) | 
| 65 | 25, 62, 64 | 3eqtrd 2780 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(log‘𝑝) = ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝))))) | 
| 66 | 16, 65 | eqtrd 2776 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(Λ‘(𝑝↑𝑘)) = ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝))))) | 
| 67 | 66 | sumeq2dv 15739 | . 2
⊢ (𝐴 ∈ ℝ →
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)Σ𝑘 ∈
(1...(⌊‘((log‘𝐴) / (log‘𝑝))))(Λ‘(𝑝↑𝑘)) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝))))) | 
| 68 | 1, 10, 67 | 3eqtrd 2780 | 1
⊢ (𝐴 ∈ ℝ →
(ψ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩
ℙ)((log‘𝑝)
· (⌊‘((log‘𝐴) / (log‘𝑝))))) |