| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | chpcl 27167 | . . . . 5
⊢ (𝐴 ∈ ℝ →
(ψ‘𝐴) ∈
ℝ) | 
| 2 | 1 | adantr 480 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(ψ‘𝐴) ∈
ℝ) | 
| 3 |  | chtcl 27152 | . . . . 5
⊢ (𝐴 ∈ ℝ →
(θ‘𝐴) ∈
ℝ) | 
| 4 | 3 | adantr 480 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(θ‘𝐴) ∈
ℝ) | 
| 5 | 2, 4 | resubcld 11691 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((ψ‘𝐴) −
(θ‘𝐴)) ∈
ℝ) | 
| 6 |  | simpl 482 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 𝐴 ∈ ℝ) | 
| 7 |  | 0red 11264 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 0 ∈
ℝ) | 
| 8 |  | 1red 11262 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 1 ∈
ℝ) | 
| 9 |  | 0lt1 11785 | . . . . . . . . . 10
⊢ 0 <
1 | 
| 10 | 9 | a1i 11 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 0 <
1) | 
| 11 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 1 ≤ 𝐴) | 
| 12 | 7, 8, 6, 10, 11 | ltletrd 11421 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 0 < 𝐴) | 
| 13 | 6, 12 | elrpd 13074 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 𝐴 ∈
ℝ+) | 
| 14 | 13 | rpge0d 13081 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 0 ≤ 𝐴) | 
| 15 | 6, 14 | resqrtcld 15456 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(√‘𝐴) ∈
ℝ) | 
| 16 |  | ppifi 27149 | . . . . 5
⊢
((√‘𝐴)
∈ ℝ → ((0[,](√‘𝐴)) ∩ ℙ) ∈
Fin) | 
| 17 | 15, 16 | syl 17 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((0[,](√‘𝐴))
∩ ℙ) ∈ Fin) | 
| 18 | 13 | adantr 480 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝐴 ∈
ℝ+) | 
| 19 | 18 | relogcld 26665 | . . . 4
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(log‘𝐴) ∈
ℝ) | 
| 20 | 17, 19 | fsumrecl 15770 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → Σ𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)(log‘𝐴)
∈ ℝ) | 
| 21 | 13 | relogcld 26665 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → (log‘𝐴) ∈
ℝ) | 
| 22 | 15, 21 | remulcld 11291 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((√‘𝐴) ·
(log‘𝐴)) ∈
ℝ) | 
| 23 |  | ppifi 27149 | . . . . . . 7
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ)
∈ Fin) | 
| 24 | 23 | adantr 480 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → ((0[,]𝐴) ∩ ℙ) ∈
Fin) | 
| 25 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) | 
| 26 | 25 | elin2d 4205 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ) | 
| 27 |  | prmnn 16711 | . . . . . . . . . . 11
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) | 
| 28 | 26, 27 | syl 17 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ) | 
| 29 | 28 | nnrpd 13075 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ+) | 
| 30 | 29 | relogcld 26665 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℝ) | 
| 31 | 21 | adantr 480 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈
ℝ) | 
| 32 | 28 | nnred 12281 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ) | 
| 33 |  | prmuz2 16733 | . . . . . . . . . . . . 13
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) | 
| 34 | 26, 33 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈
(ℤ≥‘2)) | 
| 35 |  | eluz2gt1 12962 | . . . . . . . . . . . 12
⊢ (𝑝 ∈
(ℤ≥‘2) → 1 < 𝑝) | 
| 36 | 34, 35 | syl 17 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝑝) | 
| 37 | 32, 36 | rplogcld 26671 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℝ+) | 
| 38 | 31, 37 | rerpdivcld 13108 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈
ℝ) | 
| 39 |  | reflcl 13836 | . . . . . . . . 9
⊢
(((log‘𝐴) /
(log‘𝑝)) ∈
ℝ → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ) | 
| 40 | 38, 39 | syl 17 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ) | 
| 41 | 30, 40 | remulcld 11291 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℝ) | 
| 42 | 41 | recnd 11289 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℂ) | 
| 43 | 30 | recnd 11289 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℂ) | 
| 44 | 24, 42, 43 | fsumsub 15824 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = (Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝))) | 
| 45 |  | 0le0 12367 | . . . . . . . . 9
⊢ 0 ≤
0 | 
| 46 | 45 | a1i 11 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 0 ≤
0) | 
| 47 | 8, 6, 6, 14, 11 | lemul2ad 12208 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → (𝐴 · 1) ≤ (𝐴 · 𝐴)) | 
| 48 | 6 | recnd 11289 | . . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 𝐴 ∈ ℂ) | 
| 49 | 48 | sqsqrtd 15478 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((√‘𝐴)↑2)
= 𝐴) | 
| 50 | 48 | mulridd 11278 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → (𝐴 · 1) = 𝐴) | 
| 51 | 49, 50 | eqtr4d 2780 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((√‘𝐴)↑2)
= (𝐴 ·
1)) | 
| 52 | 48 | sqvald 14183 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → (𝐴↑2) = (𝐴 · 𝐴)) | 
| 53 | 47, 51, 52 | 3brtr4d 5175 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((√‘𝐴)↑2)
≤ (𝐴↑2)) | 
| 54 | 6, 14 | sqrtge0d 15459 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 0 ≤
(√‘𝐴)) | 
| 55 | 15, 6, 54, 14 | le2sqd 14296 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((√‘𝐴) ≤
𝐴 ↔
((√‘𝐴)↑2)
≤ (𝐴↑2))) | 
| 56 | 53, 55 | mpbird 257 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(√‘𝐴) ≤
𝐴) | 
| 57 |  | iccss 13455 | . . . . . . . 8
⊢ (((0
∈ ℝ ∧ 𝐴
∈ ℝ) ∧ (0 ≤ 0 ∧ (√‘𝐴) ≤ 𝐴)) → (0[,](√‘𝐴)) ⊆ (0[,]𝐴)) | 
| 58 | 7, 6, 46, 56, 57 | syl22anc 839 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(0[,](√‘𝐴))
⊆ (0[,]𝐴)) | 
| 59 | 58 | ssrind 4244 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((0[,](√‘𝐴))
∩ ℙ) ⊆ ((0[,]𝐴) ∩ ℙ)) | 
| 60 | 59 | sselda 3983 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) | 
| 61 | 41, 30 | resubcld 11691 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℝ) | 
| 62 | 61 | recnd 11289 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℂ) | 
| 63 | 60, 62 | syldan 591 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℂ) | 
| 64 |  | eldifi 4131 | . . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ)) → 𝑝
∈ ((0[,]𝐴) ∩
ℙ)) | 
| 65 | 64, 43 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (log‘𝑝) ∈ ℂ) | 
| 66 | 65 | mullidd 11279 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (1 · (log‘𝑝)) = (log‘𝑝)) | 
| 67 | 25 | elin1d 4204 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (0[,]𝐴)) | 
| 68 |  | 0re 11263 | . . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ | 
| 69 | 6 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℝ) | 
| 70 |  | elicc2 13452 | . . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑝
∈ (0[,]𝐴) ↔
(𝑝 ∈ ℝ ∧ 0
≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) | 
| 71 | 68, 69, 70 | sylancr 587 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) | 
| 72 | 67, 71 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴)) | 
| 73 | 72 | simp3d 1145 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≤ 𝐴) | 
| 74 | 64, 73 | sylan2 593 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝑝
≤ 𝐴) | 
| 75 | 64, 29 | sylan2 593 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝑝
∈ ℝ+) | 
| 76 | 13 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝐴
∈ ℝ+) | 
| 77 | 75, 76 | logled 26669 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (𝑝
≤ 𝐴 ↔
(log‘𝑝) ≤
(log‘𝐴))) | 
| 78 | 74, 77 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (log‘𝑝) ≤ (log‘𝐴)) | 
| 79 | 66, 78 | eqbrtrd 5165 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (1 · (log‘𝑝)) ≤ (log‘𝐴)) | 
| 80 |  | 1red 11262 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 1 ∈ ℝ) | 
| 81 | 21 | adantr 480 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (log‘𝐴) ∈ ℝ) | 
| 82 | 64, 37 | sylan2 593 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (log‘𝑝) ∈
ℝ+) | 
| 83 | 80, 81, 82 | lemuldivd 13126 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((1 · (log‘𝑝)) ≤ (log‘𝐴) ↔ 1 ≤ ((log‘𝐴) / (log‘𝑝)))) | 
| 84 | 79, 83 | mpbid 232 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 1 ≤ ((log‘𝐴) / (log‘𝑝))) | 
| 85 | 6 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝐴
∈ ℝ) | 
| 86 | 85 | recnd 11289 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝐴
∈ ℂ) | 
| 87 | 86 | sqsqrtd 15478 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((√‘𝐴)↑2) = 𝐴) | 
| 88 |  | eldifn 4132 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ)) → ¬ 𝑝 ∈ ((0[,](√‘𝐴)) ∩
ℙ)) | 
| 89 | 88 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ¬ 𝑝 ∈ ((0[,](√‘𝐴)) ∩
ℙ)) | 
| 90 | 64, 26 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝑝
∈ ℙ) | 
| 91 |  | elin 3967 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ) ↔ (𝑝
∈ (0[,](√‘𝐴)) ∧ 𝑝 ∈ ℙ)) | 
| 92 | 91 | rbaib 538 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 ∈ ℙ → (𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ) ↔ 𝑝
∈ (0[,](√‘𝐴)))) | 
| 93 | 90, 92 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (𝑝
∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ 𝑝 ∈ (0[,](√‘𝐴)))) | 
| 94 |  | 0red 11264 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 0 ∈ ℝ) | 
| 95 | 15 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (√‘𝐴) ∈ ℝ) | 
| 96 | 64, 28 | sylan2 593 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝑝
∈ ℕ) | 
| 97 | 96 | nnred 12281 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝑝
∈ ℝ) | 
| 98 | 75 | rpge0d 13081 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 0 ≤ 𝑝) | 
| 99 |  | elicc2 13452 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((0
∈ ℝ ∧ (√‘𝐴) ∈ ℝ) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ (√‘𝐴)))) | 
| 100 |  | df-3an 1089 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑝 ∈ ℝ ∧ 0 ≤
𝑝 ∧ 𝑝 ≤ (√‘𝐴)) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ (√‘𝐴))) | 
| 101 | 99, 100 | bitrdi 287 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((0
∈ ℝ ∧ (√‘𝐴) ∈ ℝ) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ (√‘𝐴)))) | 
| 102 | 101 | baibd 539 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((0
∈ ℝ ∧ (√‘𝐴) ∈ ℝ) ∧ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝)) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ 𝑝 ≤ (√‘𝐴))) | 
| 103 | 94, 95, 97, 98, 102 | syl22anc 839 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (𝑝
∈ (0[,](√‘𝐴)) ↔ 𝑝 ≤ (√‘𝐴))) | 
| 104 | 93, 103 | bitrd 279 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (𝑝
∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ 𝑝 ≤ (√‘𝐴))) | 
| 105 | 89, 104 | mtbid 324 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ¬ 𝑝 ≤ (√‘𝐴)) | 
| 106 | 95, 97 | ltnled 11408 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((√‘𝐴) < 𝑝 ↔ ¬ 𝑝 ≤ (√‘𝐴))) | 
| 107 | 105, 106 | mpbird 257 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (√‘𝐴) < 𝑝) | 
| 108 | 54 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 0 ≤ (√‘𝐴)) | 
| 109 | 95, 97, 108, 98 | lt2sqd 14295 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((√‘𝐴) < 𝑝 ↔ ((√‘𝐴)↑2) < (𝑝↑2))) | 
| 110 | 107, 109 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((√‘𝐴)↑2) < (𝑝↑2)) | 
| 111 | 87, 110 | eqbrtrrd 5167 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝐴
< (𝑝↑2)) | 
| 112 | 96 | nnsqcld 14283 | . . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (𝑝↑2) ∈ ℕ) | 
| 113 | 112 | nnrpd 13075 | . . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (𝑝↑2) ∈
ℝ+) | 
| 114 |  | logltb 26642 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ+
∧ (𝑝↑2) ∈
ℝ+) → (𝐴 < (𝑝↑2) ↔ (log‘𝐴) < (log‘(𝑝↑2)))) | 
| 115 | 76, 113, 114 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (𝐴
< (𝑝↑2) ↔
(log‘𝐴) <
(log‘(𝑝↑2)))) | 
| 116 | 111, 115 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (log‘𝐴) < (log‘(𝑝↑2))) | 
| 117 |  | 2z 12649 | . . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ | 
| 118 |  | relogexp 26638 | . . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ ℝ+
∧ 2 ∈ ℤ) → (log‘(𝑝↑2)) = (2 · (log‘𝑝))) | 
| 119 | 75, 117, 118 | sylancl 586 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (log‘(𝑝↑2)) = (2 · (log‘𝑝))) | 
| 120 | 116, 119 | breqtrd 5169 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (log‘𝐴) < (2 · (log‘𝑝))) | 
| 121 |  | 2re 12340 | . . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ | 
| 122 | 121 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 2 ∈ ℝ) | 
| 123 | 81, 122, 82 | ltdivmul2d 13129 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (((log‘𝐴) / (log‘𝑝)) < 2 ↔ (log‘𝐴) < (2 · (log‘𝑝)))) | 
| 124 | 120, 123 | mpbird 257 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) < 2) | 
| 125 |  | df-2 12329 | . . . . . . . . . . . 12
⊢ 2 = (1 +
1) | 
| 126 | 124, 125 | breqtrdi 5184 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) < (1 + 1)) | 
| 127 | 64, 38 | sylan2 593 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ) | 
| 128 |  | 1z 12647 | . . . . . . . . . . . 12
⊢ 1 ∈
ℤ | 
| 129 |  | flbi 13856 | . . . . . . . . . . . 12
⊢
((((log‘𝐴) /
(log‘𝑝)) ∈
ℝ ∧ 1 ∈ ℤ) → ((⌊‘((log‘𝐴) / (log‘𝑝))) = 1 ↔ (1 ≤
((log‘𝐴) /
(log‘𝑝)) ∧
((log‘𝐴) /
(log‘𝑝)) < (1 +
1)))) | 
| 130 | 127, 128,
129 | sylancl 586 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((⌊‘((log‘𝐴) / (log‘𝑝))) = 1 ↔ (1 ≤ ((log‘𝐴) / (log‘𝑝)) ∧ ((log‘𝐴) / (log‘𝑝)) < (1 +
1)))) | 
| 131 | 84, 126, 130 | mpbir2and 713 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (⌊‘((log‘𝐴) / (log‘𝑝))) = 1) | 
| 132 | 131 | oveq2d 7447 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) = ((log‘𝑝) · 1)) | 
| 133 | 65 | mulridd 11278 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((log‘𝑝) · 1) = (log‘𝑝)) | 
| 134 | 132, 133 | eqtrd 2777 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) = (log‘𝑝)) | 
| 135 | 134 | oveq1d 7446 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = ((log‘𝑝) − (log‘𝑝))) | 
| 136 | 65 | subidd 11608 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((log‘𝑝) − (log‘𝑝)) = 0) | 
| 137 | 135, 136 | eqtrd 2777 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = 0) | 
| 138 | 59, 63, 137, 24 | fsumss 15761 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → Σ𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝))) | 
| 139 |  | chpval2 27262 | . . . . . . 7
⊢ (𝐴 ∈ ℝ →
(ψ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩
ℙ)((log‘𝑝)
· (⌊‘((log‘𝐴) / (log‘𝑝))))) | 
| 140 | 139 | adantr 480 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(ψ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩
ℙ)((log‘𝑝)
· (⌊‘((log‘𝐴) / (log‘𝑝))))) | 
| 141 |  | chtval 27153 | . . . . . . 7
⊢ (𝐴 ∈ ℝ →
(θ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) | 
| 142 | 141 | adantr 480 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(θ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) | 
| 143 | 140, 142 | oveq12d 7449 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((ψ‘𝐴) −
(θ‘𝐴)) =
(Σ𝑝 ∈
((0[,]𝐴) ∩
ℙ)((log‘𝑝)
· (⌊‘((log‘𝐴) / (log‘𝑝)))) − Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝))) | 
| 144 | 44, 138, 143 | 3eqtr4rd 2788 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((ψ‘𝐴) −
(θ‘𝐴)) =
Σ𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝))) | 
| 145 | 60, 61 | syldan 591 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℝ) | 
| 146 | 60, 41 | syldan 591 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℝ) | 
| 147 | 60, 37 | syldan 591 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(log‘𝑝) ∈
ℝ+) | 
| 148 | 147 | rpge0d 13081 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 0 ≤
(log‘𝑝)) | 
| 149 |  | simpr 484 | . . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)) | 
| 150 | 149 | elin2d 4205 | . . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈
ℙ) | 
| 151 | 150, 27 | syl 17 | . . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈
ℕ) | 
| 152 | 151 | nnrpd 13075 | . . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈
ℝ+) | 
| 153 | 152 | relogcld 26665 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(log‘𝑝) ∈
ℝ) | 
| 154 | 146, 153 | subge02d 11855 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (0
≤ (log‘𝑝) ↔
(((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))))) | 
| 155 | 148, 154 | mpbid 232 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝))))) | 
| 156 | 60, 38 | syldan 591 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
((log‘𝐴) /
(log‘𝑝)) ∈
ℝ) | 
| 157 |  | flle 13839 | . . . . . . . 8
⊢
(((log‘𝐴) /
(log‘𝑝)) ∈
ℝ → (⌊‘((log‘𝐴) / (log‘𝑝))) ≤ ((log‘𝐴) / (log‘𝑝))) | 
| 158 | 156, 157 | syl 17 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ≤ ((log‘𝐴) / (log‘𝑝))) | 
| 159 | 60, 40 | syldan 591 | . . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ) | 
| 160 | 159, 19, 147 | lemuldiv2d 13127 | . . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) ≤ (log‘𝐴) ↔ (⌊‘((log‘𝐴) / (log‘𝑝))) ≤ ((log‘𝐴) / (log‘𝑝)))) | 
| 161 | 158, 160 | mpbird 257 | . . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) ≤ (log‘𝐴)) | 
| 162 | 145, 146,
19, 155, 161 | letrd 11418 | . . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ (log‘𝐴)) | 
| 163 | 17, 145, 19, 162 | fsumle 15835 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → Σ𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ Σ𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)(log‘𝐴)) | 
| 164 | 144, 163 | eqbrtrd 5165 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((ψ‘𝐴) −
(θ‘𝐴)) ≤
Σ𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)(log‘𝐴)) | 
| 165 | 21 | recnd 11289 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → (log‘𝐴) ∈
ℂ) | 
| 166 |  | fsumconst 15826 | . . . . 5
⊢
((((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin ∧
(log‘𝐴) ∈
ℂ) → Σ𝑝
∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) =
((♯‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴))) | 
| 167 | 17, 165, 166 | syl2anc 584 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → Σ𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)(log‘𝐴)
= ((♯‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴))) | 
| 168 |  | hashcl 14395 | . . . . . . 7
⊢
(((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin →
(♯‘((0[,](√‘𝐴)) ∩ ℙ)) ∈
ℕ0) | 
| 169 | 17, 168 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(♯‘((0[,](√‘𝐴)) ∩ ℙ)) ∈
ℕ0) | 
| 170 | 169 | nn0red 12588 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(♯‘((0[,](√‘𝐴)) ∩ ℙ)) ∈
ℝ) | 
| 171 |  | logge0 26647 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 0 ≤
(log‘𝐴)) | 
| 172 |  | reflcl 13836 | . . . . . . 7
⊢
((√‘𝐴)
∈ ℝ → (⌊‘(√‘𝐴)) ∈ ℝ) | 
| 173 | 15, 172 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(⌊‘(√‘𝐴)) ∈ ℝ) | 
| 174 |  | fzfid 14014 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(1...(⌊‘(√‘𝐴))) ∈ Fin) | 
| 175 |  | ppisval 27147 | . . . . . . . . . . 11
⊢
((√‘𝐴)
∈ ℝ → ((0[,](√‘𝐴)) ∩ ℙ) =
((2...(⌊‘(√‘𝐴))) ∩ ℙ)) | 
| 176 | 15, 175 | syl 17 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((0[,](√‘𝐴))
∩ ℙ) = ((2...(⌊‘(√‘𝐴))) ∩ ℙ)) | 
| 177 |  | inss1 4237 | . . . . . . . . . . 11
⊢
((2...(⌊‘(√‘𝐴))) ∩ ℙ) ⊆
(2...(⌊‘(√‘𝐴))) | 
| 178 |  | 2eluzge1 12936 | . . . . . . . . . . . 12
⊢ 2 ∈
(ℤ≥‘1) | 
| 179 |  | fzss1 13603 | . . . . . . . . . . . 12
⊢ (2 ∈
(ℤ≥‘1) →
(2...(⌊‘(√‘𝐴))) ⊆
(1...(⌊‘(√‘𝐴)))) | 
| 180 | 178, 179 | mp1i 13 | . . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(2...(⌊‘(√‘𝐴))) ⊆
(1...(⌊‘(√‘𝐴)))) | 
| 181 | 177, 180 | sstrid 3995 | . . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((2...(⌊‘(√‘𝐴))) ∩ ℙ) ⊆
(1...(⌊‘(√‘𝐴)))) | 
| 182 | 176, 181 | eqsstrd 4018 | . . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((0[,](√‘𝐴))
∩ ℙ) ⊆ (1...(⌊‘(√‘𝐴)))) | 
| 183 |  | ssdomg 9040 | . . . . . . . . 9
⊢
((1...(⌊‘(√‘𝐴))) ∈ Fin →
(((0[,](√‘𝐴))
∩ ℙ) ⊆ (1...(⌊‘(√‘𝐴))) → ((0[,](√‘𝐴)) ∩ ℙ) ≼
(1...(⌊‘(√‘𝐴))))) | 
| 184 | 174, 182,
183 | sylc 65 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((0[,](√‘𝐴))
∩ ℙ) ≼ (1...(⌊‘(√‘𝐴)))) | 
| 185 |  | hashdom 14418 | . . . . . . . . 9
⊢
((((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin ∧
(1...(⌊‘(√‘𝐴))) ∈ Fin) →
((♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤
(♯‘(1...(⌊‘(√‘𝐴)))) ↔ ((0[,](√‘𝐴)) ∩ ℙ) ≼
(1...(⌊‘(√‘𝐴))))) | 
| 186 | 17, 174, 185 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤
(♯‘(1...(⌊‘(√‘𝐴)))) ↔ ((0[,](√‘𝐴)) ∩ ℙ) ≼
(1...(⌊‘(√‘𝐴))))) | 
| 187 | 184, 186 | mpbird 257 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤
(♯‘(1...(⌊‘(√‘𝐴))))) | 
| 188 |  | flge0nn0 13860 | . . . . . . . . 9
⊢
(((√‘𝐴)
∈ ℝ ∧ 0 ≤ (√‘𝐴)) →
(⌊‘(√‘𝐴)) ∈
ℕ0) | 
| 189 | 15, 54, 188 | syl2anc 584 | . . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(⌊‘(√‘𝐴)) ∈
ℕ0) | 
| 190 |  | hashfz1 14385 | . . . . . . . 8
⊢
((⌊‘(√‘𝐴)) ∈ ℕ0 →
(♯‘(1...(⌊‘(√‘𝐴)))) = (⌊‘(√‘𝐴))) | 
| 191 | 189, 190 | syl 17 | . . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(♯‘(1...(⌊‘(√‘𝐴)))) = (⌊‘(√‘𝐴))) | 
| 192 | 187, 191 | breqtrd 5169 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤
(⌊‘(√‘𝐴))) | 
| 193 |  | flle 13839 | . . . . . . 7
⊢
((√‘𝐴)
∈ ℝ → (⌊‘(√‘𝐴)) ≤ (√‘𝐴)) | 
| 194 | 15, 193 | syl 17 | . . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(⌊‘(√‘𝐴)) ≤ (√‘𝐴)) | 
| 195 | 170, 173,
15, 192, 194 | letrd 11418 | . . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(♯‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (√‘𝐴)) | 
| 196 | 170, 15, 21, 171, 195 | lemul1ad 12207 | . . . 4
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((♯‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴)) ≤ ((√‘𝐴) · (log‘𝐴))) | 
| 197 | 167, 196 | eqbrtrd 5165 | . . 3
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → Σ𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)(log‘𝐴)
≤ ((√‘𝐴)
· (log‘𝐴))) | 
| 198 | 5, 20, 22, 164, 197 | letrd 11418 | . 2
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((ψ‘𝐴) −
(θ‘𝐴)) ≤
((√‘𝐴) ·
(log‘𝐴))) | 
| 199 | 2, 4, 22 | lesubadd2d 11862 | . 2
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(((ψ‘𝐴) −
(θ‘𝐴)) ≤
((√‘𝐴) ·
(log‘𝐴)) ↔
(ψ‘𝐴) ≤
((θ‘𝐴) +
((√‘𝐴) ·
(log‘𝐴))))) | 
| 200 | 198, 199 | mpbid 232 | 1
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(ψ‘𝐴) ≤
((θ‘𝐴) +
((√‘𝐴) ·
(log‘𝐴)))) |