Step | Hyp | Ref
| Expression |
1 | | chpcl 24650 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(ψ‘𝐴) ∈
ℝ) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(ψ‘𝐴) ∈
ℝ) |
3 | | chtcl 24635 |
. . . . 5
⊢ (𝐴 ∈ ℝ →
(θ‘𝐴) ∈
ℝ) |
4 | 3 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(θ‘𝐴) ∈
ℝ) |
5 | 2, 4 | resubcld 10337 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((ψ‘𝐴) −
(θ‘𝐴)) ∈
ℝ) |
6 | | simpl 472 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 𝐴 ∈ ℝ) |
7 | | 0red 9920 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 0 ∈
ℝ) |
8 | | 1red 9934 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 1 ∈
ℝ) |
9 | | 0lt1 10429 |
. . . . . . . . . 10
⊢ 0 <
1 |
10 | 9 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 0 <
1) |
11 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 1 ≤ 𝐴) |
12 | 7, 8, 6, 10, 11 | ltletrd 10076 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 0 < 𝐴) |
13 | 6, 12 | elrpd 11745 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 𝐴 ∈
ℝ+) |
14 | 13 | rpge0d 11752 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 0 ≤ 𝐴) |
15 | 6, 14 | resqrtcld 14004 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(√‘𝐴) ∈
ℝ) |
16 | | ppifi 24632 |
. . . . 5
⊢
((√‘𝐴)
∈ ℝ → ((0[,](√‘𝐴)) ∩ ℙ) ∈
Fin) |
17 | 15, 16 | syl 17 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((0[,](√‘𝐴))
∩ ℙ) ∈ Fin) |
18 | 13 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝐴 ∈
ℝ+) |
19 | 18 | relogcld 24173 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(log‘𝐴) ∈
ℝ) |
20 | 17, 19 | fsumrecl 14312 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → Σ𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)(log‘𝐴)
∈ ℝ) |
21 | 13 | relogcld 24173 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → (log‘𝐴) ∈
ℝ) |
22 | 15, 21 | remulcld 9949 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((√‘𝐴) ·
(log‘𝐴)) ∈
ℝ) |
23 | | ppifi 24632 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
((0[,]𝐴) ∩ ℙ)
∈ Fin) |
24 | 23 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → ((0[,]𝐴) ∩ ℙ) ∈
Fin) |
25 | | inss2 3796 |
. . . . . . . . . . . 12
⊢
((0[,]𝐴) ∩
ℙ) ⊆ ℙ |
26 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) |
27 | 25, 26 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℙ) |
28 | | prmnn 15226 |
. . . . . . . . . . 11
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℕ) |
30 | 29 | nnrpd 11746 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ+) |
31 | 30 | relogcld 24173 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℝ) |
32 | 21 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝐴) ∈
ℝ) |
33 | 29 | nnred 10912 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ ℝ) |
34 | | prmuz2 15246 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) |
35 | 27, 34 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈
(ℤ≥‘2)) |
36 | | eluz2b2 11637 |
. . . . . . . . . . . . 13
⊢ (𝑝 ∈
(ℤ≥‘2) ↔ (𝑝 ∈ ℕ ∧ 1 < 𝑝)) |
37 | 36 | simprbi 479 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈
(ℤ≥‘2) → 1 < 𝑝) |
38 | 35, 37 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 1 < 𝑝) |
39 | 33, 38 | rplogcld 24179 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℝ+) |
40 | 32, 39 | rerpdivcld 11779 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝐴) / (log‘𝑝)) ∈
ℝ) |
41 | | reflcl 12459 |
. . . . . . . . 9
⊢
(((log‘𝐴) /
(log‘𝑝)) ∈
ℝ → (⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ) |
42 | 40, 41 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ) |
43 | 31, 42 | remulcld 9949 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℝ) |
44 | 43 | recnd 9947 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → ((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℂ) |
45 | 31 | recnd 9947 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (log‘𝑝) ∈
ℂ) |
46 | 24, 44, 45 | fsumsub 14362 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = (Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝))) |
47 | | 0le0 10987 |
. . . . . . . . 9
⊢ 0 ≤
0 |
48 | 47 | a1i 11 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 0 ≤
0) |
49 | 8, 6, 6, 14, 11 | lemul2ad 10843 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → (𝐴 · 1) ≤ (𝐴 · 𝐴)) |
50 | 6 | recnd 9947 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 𝐴 ∈ ℂ) |
51 | 50 | sqsqrtd 14026 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((√‘𝐴)↑2)
= 𝐴) |
52 | 50 | mulid1d 9936 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → (𝐴 · 1) = 𝐴) |
53 | 51, 52 | eqtr4d 2647 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((√‘𝐴)↑2)
= (𝐴 ·
1)) |
54 | 50 | sqvald 12867 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → (𝐴↑2) = (𝐴 · 𝐴)) |
55 | 49, 53, 54 | 3brtr4d 4615 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((√‘𝐴)↑2)
≤ (𝐴↑2)) |
56 | 6, 14 | sqrtge0d 14007 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 0 ≤
(√‘𝐴)) |
57 | 15, 6, 56, 14 | le2sqd 12906 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((√‘𝐴) ≤
𝐴 ↔
((√‘𝐴)↑2)
≤ (𝐴↑2))) |
58 | 55, 57 | mpbird 246 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(√‘𝐴) ≤
𝐴) |
59 | | iccss 12112 |
. . . . . . . 8
⊢ (((0
∈ ℝ ∧ 𝐴
∈ ℝ) ∧ (0 ≤ 0 ∧ (√‘𝐴) ≤ 𝐴)) → (0[,](√‘𝐴)) ⊆ (0[,]𝐴)) |
60 | 7, 6, 48, 58, 59 | syl22anc 1319 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(0[,](√‘𝐴))
⊆ (0[,]𝐴)) |
61 | | ssrin 3800 |
. . . . . . 7
⊢
((0[,](√‘𝐴)) ⊆ (0[,]𝐴) → ((0[,](√‘𝐴)) ∩ ℙ) ⊆
((0[,]𝐴) ∩
ℙ)) |
62 | 60, 61 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((0[,](√‘𝐴))
∩ ℙ) ⊆ ((0[,]𝐴) ∩ ℙ)) |
63 | 62 | sselda 3568 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) |
64 | 43, 31 | resubcld 10337 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℝ) |
65 | 64 | recnd 9947 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℂ) |
66 | 63, 65 | syldan 486 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℂ) |
67 | | eldifi 3694 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ)) → 𝑝
∈ ((0[,]𝐴) ∩
ℙ)) |
68 | 67, 45 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (log‘𝑝) ∈ ℂ) |
69 | 68 | mulid2d 9937 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (1 · (log‘𝑝)) = (log‘𝑝)) |
70 | | inss1 3795 |
. . . . . . . . . . . . . . . . . 18
⊢
((0[,]𝐴) ∩
ℙ) ⊆ (0[,]𝐴) |
71 | 70, 26 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ∈ (0[,]𝐴)) |
72 | | 0re 9919 |
. . . . . . . . . . . . . . . . . 18
⊢ 0 ∈
ℝ |
73 | 6 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝐴 ∈ ℝ) |
74 | | elicc2 12109 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑝
∈ (0[,]𝐴) ↔
(𝑝 ∈ ℝ ∧ 0
≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) |
75 | 72, 73, 74 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ (0[,]𝐴) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴))) |
76 | 71, 75 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴)) |
77 | 76 | simp3d 1068 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,]𝐴) ∩ ℙ)) → 𝑝 ≤ 𝐴) |
78 | 67, 77 | sylan2 490 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝑝
≤ 𝐴) |
79 | 67, 30 | sylan2 490 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝑝
∈ ℝ+) |
80 | 13 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝐴
∈ ℝ+) |
81 | 79, 80 | logled 24177 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (𝑝
≤ 𝐴 ↔
(log‘𝑝) ≤
(log‘𝐴))) |
82 | 78, 81 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (log‘𝑝) ≤ (log‘𝐴)) |
83 | 69, 82 | eqbrtrd 4605 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (1 · (log‘𝑝)) ≤ (log‘𝐴)) |
84 | | 1red 9934 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 1 ∈ ℝ) |
85 | 21 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (log‘𝐴) ∈ ℝ) |
86 | 67, 39 | sylan2 490 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (log‘𝑝) ∈
ℝ+) |
87 | 84, 85, 86 | lemuldivd 11797 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((1 · (log‘𝑝)) ≤ (log‘𝐴) ↔ 1 ≤ ((log‘𝐴) / (log‘𝑝)))) |
88 | 83, 87 | mpbid 221 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 1 ≤ ((log‘𝐴) / (log‘𝑝))) |
89 | 6 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝐴
∈ ℝ) |
90 | 89 | recnd 9947 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝐴
∈ ℂ) |
91 | 90 | sqsqrtd 14026 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((√‘𝐴)↑2) = 𝐴) |
92 | | eldifn 3695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ)) → ¬ 𝑝 ∈ ((0[,](√‘𝐴)) ∩
ℙ)) |
93 | 92 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ¬ 𝑝 ∈ ((0[,](√‘𝐴)) ∩
ℙ)) |
94 | 67, 27 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝑝
∈ ℙ) |
95 | | elin 3758 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ) ↔ (𝑝
∈ (0[,](√‘𝐴)) ∧ 𝑝 ∈ ℙ)) |
96 | 95 | rbaib 945 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 ∈ ℙ → (𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ) ↔ 𝑝
∈ (0[,](√‘𝐴)))) |
97 | 94, 96 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (𝑝
∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ 𝑝 ∈ (0[,](√‘𝐴)))) |
98 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 0 ∈ ℝ) |
99 | 15 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (√‘𝐴) ∈ ℝ) |
100 | 67, 29 | sylan2 490 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝑝
∈ ℕ) |
101 | 100 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝑝
∈ ℝ) |
102 | 79 | rpge0d 11752 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 0 ≤ 𝑝) |
103 | | elicc2 12109 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((0
∈ ℝ ∧ (√‘𝐴) ∈ ℝ) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ (√‘𝐴)))) |
104 | | df-3an 1033 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑝 ∈ ℝ ∧ 0 ≤
𝑝 ∧ 𝑝 ≤ (√‘𝐴)) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ (√‘𝐴))) |
105 | 103, 104 | syl6bb 275 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((0
∈ ℝ ∧ (√‘𝐴) ∈ ℝ) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ ((𝑝 ∈ ℝ ∧ 0 ≤ 𝑝) ∧ 𝑝 ≤ (√‘𝐴)))) |
106 | 105 | baibd 946 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((0
∈ ℝ ∧ (√‘𝐴) ∈ ℝ) ∧ (𝑝 ∈ ℝ ∧ 0 ≤ 𝑝)) → (𝑝 ∈ (0[,](√‘𝐴)) ↔ 𝑝 ≤ (√‘𝐴))) |
107 | 98, 99, 101, 102, 106 | syl22anc 1319 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (𝑝
∈ (0[,](√‘𝐴)) ↔ 𝑝 ≤ (√‘𝐴))) |
108 | 97, 107 | bitrd 267 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (𝑝
∈ ((0[,](√‘𝐴)) ∩ ℙ) ↔ 𝑝 ≤ (√‘𝐴))) |
109 | 93, 108 | mtbid 313 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ¬ 𝑝 ≤ (√‘𝐴)) |
110 | 99, 101 | ltnled 10063 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((√‘𝐴) < 𝑝 ↔ ¬ 𝑝 ≤ (√‘𝐴))) |
111 | 109, 110 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (√‘𝐴) < 𝑝) |
112 | 56 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 0 ≤ (√‘𝐴)) |
113 | 99, 101, 112, 102 | lt2sqd 12905 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((√‘𝐴) < 𝑝 ↔ ((√‘𝐴)↑2) < (𝑝↑2))) |
114 | 111, 113 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((√‘𝐴)↑2) < (𝑝↑2)) |
115 | 91, 114 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 𝐴
< (𝑝↑2)) |
116 | 100 | nnsqcld 12891 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (𝑝↑2) ∈ ℕ) |
117 | 116 | nnrpd 11746 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (𝑝↑2) ∈
ℝ+) |
118 | | logltb 24150 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℝ+
∧ (𝑝↑2) ∈
ℝ+) → (𝐴 < (𝑝↑2) ↔ (log‘𝐴) < (log‘(𝑝↑2)))) |
119 | 80, 117, 118 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (𝐴
< (𝑝↑2) ↔
(log‘𝐴) <
(log‘(𝑝↑2)))) |
120 | 115, 119 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (log‘𝐴) < (log‘(𝑝↑2))) |
121 | | 2z 11286 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℤ |
122 | | relogexp 24146 |
. . . . . . . . . . . . . . 15
⊢ ((𝑝 ∈ ℝ+
∧ 2 ∈ ℤ) → (log‘(𝑝↑2)) = (2 · (log‘𝑝))) |
123 | 79, 121, 122 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (log‘(𝑝↑2)) = (2 · (log‘𝑝))) |
124 | 120, 123 | breqtrd 4609 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (log‘𝐴) < (2 · (log‘𝑝))) |
125 | | 2re 10967 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
126 | 125 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → 2 ∈ ℝ) |
127 | 85, 126, 86 | ltdivmul2d 11800 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (((log‘𝐴) / (log‘𝑝)) < 2 ↔ (log‘𝐴) < (2 · (log‘𝑝)))) |
128 | 124, 127 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) < 2) |
129 | | df-2 10956 |
. . . . . . . . . . . 12
⊢ 2 = (1 +
1) |
130 | 128, 129 | syl6breq 4624 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) < (1 + 1)) |
131 | 67, 40 | sylan2 490 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((log‘𝐴) / (log‘𝑝)) ∈ ℝ) |
132 | | 1z 11284 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℤ |
133 | | flbi 12479 |
. . . . . . . . . . . 12
⊢
((((log‘𝐴) /
(log‘𝑝)) ∈
ℝ ∧ 1 ∈ ℤ) → ((⌊‘((log‘𝐴) / (log‘𝑝))) = 1 ↔ (1 ≤
((log‘𝐴) /
(log‘𝑝)) ∧
((log‘𝐴) /
(log‘𝑝)) < (1 +
1)))) |
134 | 131, 132,
133 | sylancl 693 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((⌊‘((log‘𝐴) / (log‘𝑝))) = 1 ↔ (1 ≤ ((log‘𝐴) / (log‘𝑝)) ∧ ((log‘𝐴) / (log‘𝑝)) < (1 +
1)))) |
135 | 88, 130, 134 | mpbir2and 959 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (⌊‘((log‘𝐴) / (log‘𝑝))) = 1) |
136 | 135 | oveq2d 6565 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) = ((log‘𝑝) · 1)) |
137 | 68 | mulid1d 9936 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((log‘𝑝) · 1) = (log‘𝑝)) |
138 | 136, 137 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) = (log‘𝑝)) |
139 | 138 | oveq1d 6564 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = ((log‘𝑝) − (log‘𝑝))) |
140 | 68 | subidd 10259 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → ((log‘𝑝) − (log‘𝑝)) = 0) |
141 | 139, 140 | eqtrd 2644 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ (((0[,]𝐴) ∩ ℙ) ∖
((0[,](√‘𝐴))
∩ ℙ))) → (((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = 0) |
142 | 62, 66, 141, 24 | fsumss 14303 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → Σ𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) = Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝))) |
143 | | chpval2 24743 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(ψ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩
ℙ)((log‘𝑝)
· (⌊‘((log‘𝐴) / (log‘𝑝))))) |
144 | 143 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(ψ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩
ℙ)((log‘𝑝)
· (⌊‘((log‘𝐴) / (log‘𝑝))))) |
145 | | chtval 24636 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
(θ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) |
146 | 145 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(θ‘𝐴) =
Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝)) |
147 | 144, 146 | oveq12d 6567 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((ψ‘𝐴) −
(θ‘𝐴)) =
(Σ𝑝 ∈
((0[,]𝐴) ∩
ℙ)((log‘𝑝)
· (⌊‘((log‘𝐴) / (log‘𝑝)))) − Σ𝑝 ∈ ((0[,]𝐴) ∩ ℙ)(log‘𝑝))) |
148 | 46, 142, 147 | 3eqtr4rd 2655 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((ψ‘𝐴) −
(θ‘𝐴)) =
Σ𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝))) |
149 | 63, 64 | syldan 486 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ∈ ℝ) |
150 | 63, 43 | syldan 486 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) ∈ ℝ) |
151 | 63, 39 | syldan 486 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(log‘𝑝) ∈
ℝ+) |
152 | 151 | rpge0d 11752 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 0 ≤
(log‘𝑝)) |
153 | | inss2 3796 |
. . . . . . . . . . . 12
⊢
((0[,](√‘𝐴)) ∩ ℙ) ⊆
ℙ |
154 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)) |
155 | 153, 154 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈
ℙ) |
156 | 155, 28 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈
ℕ) |
157 | 156 | nnrpd 11746 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → 𝑝 ∈
ℝ+) |
158 | 157 | relogcld 24173 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(log‘𝑝) ∈
ℝ) |
159 | 150, 158 | subge02d 10498 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) → (0
≤ (log‘𝑝) ↔
(((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))))) |
160 | 152, 159 | mpbid 221 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ ((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝))))) |
161 | 63, 40 | syldan 486 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
((log‘𝐴) /
(log‘𝑝)) ∈
ℝ) |
162 | | flle 12462 |
. . . . . . . 8
⊢
(((log‘𝐴) /
(log‘𝑝)) ∈
ℝ → (⌊‘((log‘𝐴) / (log‘𝑝))) ≤ ((log‘𝐴) / (log‘𝑝))) |
163 | 161, 162 | syl 17 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ≤ ((log‘𝐴) / (log‘𝑝))) |
164 | 63, 42 | syldan 486 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(⌊‘((log‘𝐴) / (log‘𝑝))) ∈ ℝ) |
165 | 164, 19, 151 | lemuldiv2d 11798 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) ≤ (log‘𝐴) ↔ (⌊‘((log‘𝐴) / (log‘𝑝))) ≤ ((log‘𝐴) / (log‘𝑝)))) |
166 | 163, 165 | mpbird 246 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) ≤ (log‘𝐴)) |
167 | 149, 150,
19, 160, 166 | letrd 10073 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) ∧ 𝑝 ∈ ((0[,](√‘𝐴)) ∩ ℙ)) →
(((log‘𝑝) ·
(⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ (log‘𝐴)) |
168 | 17, 149, 19, 167 | fsumle 14372 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → Σ𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)(((log‘𝑝) · (⌊‘((log‘𝐴) / (log‘𝑝)))) − (log‘𝑝)) ≤ Σ𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)(log‘𝐴)) |
169 | 148, 168 | eqbrtrd 4605 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((ψ‘𝐴) −
(θ‘𝐴)) ≤
Σ𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)(log‘𝐴)) |
170 | 21 | recnd 9947 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → (log‘𝐴) ∈
ℂ) |
171 | | fsumconst 14364 |
. . . . 5
⊢
((((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin ∧
(log‘𝐴) ∈
ℂ) → Σ𝑝
∈ ((0[,](√‘𝐴)) ∩ ℙ)(log‘𝐴) =
((#‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴))) |
172 | 17, 170, 171 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → Σ𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)(log‘𝐴)
= ((#‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴))) |
173 | | hashcl 13009 |
. . . . . . 7
⊢
(((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin →
(#‘((0[,](√‘𝐴)) ∩ ℙ)) ∈
ℕ0) |
174 | 17, 173 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(#‘((0[,](√‘𝐴)) ∩ ℙ)) ∈
ℕ0) |
175 | 174 | nn0red 11229 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(#‘((0[,](√‘𝐴)) ∩ ℙ)) ∈
ℝ) |
176 | | logge0 24155 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → 0 ≤
(log‘𝐴)) |
177 | | reflcl 12459 |
. . . . . . 7
⊢
((√‘𝐴)
∈ ℝ → (⌊‘(√‘𝐴)) ∈ ℝ) |
178 | 15, 177 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(⌊‘(√‘𝐴)) ∈ ℝ) |
179 | | fzfid 12634 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(1...(⌊‘(√‘𝐴))) ∈ Fin) |
180 | | ppisval 24630 |
. . . . . . . . . . 11
⊢
((√‘𝐴)
∈ ℝ → ((0[,](√‘𝐴)) ∩ ℙ) =
((2...(⌊‘(√‘𝐴))) ∩ ℙ)) |
181 | 15, 180 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((0[,](√‘𝐴))
∩ ℙ) = ((2...(⌊‘(√‘𝐴))) ∩ ℙ)) |
182 | | inss1 3795 |
. . . . . . . . . . 11
⊢
((2...(⌊‘(√‘𝐴))) ∩ ℙ) ⊆
(2...(⌊‘(√‘𝐴))) |
183 | | 2eluzge1 11610 |
. . . . . . . . . . . 12
⊢ 2 ∈
(ℤ≥‘1) |
184 | | fzss1 12251 |
. . . . . . . . . . . 12
⊢ (2 ∈
(ℤ≥‘1) →
(2...(⌊‘(√‘𝐴))) ⊆
(1...(⌊‘(√‘𝐴)))) |
185 | 183, 184 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(2...(⌊‘(√‘𝐴))) ⊆
(1...(⌊‘(√‘𝐴)))) |
186 | 182, 185 | syl5ss 3579 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((2...(⌊‘(√‘𝐴))) ∩ ℙ) ⊆
(1...(⌊‘(√‘𝐴)))) |
187 | 181, 186 | eqsstrd 3602 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((0[,](√‘𝐴))
∩ ℙ) ⊆ (1...(⌊‘(√‘𝐴)))) |
188 | | ssdomg 7887 |
. . . . . . . . 9
⊢
((1...(⌊‘(√‘𝐴))) ∈ Fin →
(((0[,](√‘𝐴))
∩ ℙ) ⊆ (1...(⌊‘(√‘𝐴))) → ((0[,](√‘𝐴)) ∩ ℙ) ≼
(1...(⌊‘(√‘𝐴))))) |
189 | 179, 187,
188 | sylc 63 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((0[,](√‘𝐴))
∩ ℙ) ≼ (1...(⌊‘(√‘𝐴)))) |
190 | | hashdom 13029 |
. . . . . . . . 9
⊢
((((0[,](√‘𝐴)) ∩ ℙ) ∈ Fin ∧
(1...(⌊‘(√‘𝐴))) ∈ Fin) →
((#‘((0[,](√‘𝐴)) ∩ ℙ)) ≤
(#‘(1...(⌊‘(√‘𝐴)))) ↔ ((0[,](√‘𝐴)) ∩ ℙ) ≼
(1...(⌊‘(√‘𝐴))))) |
191 | 17, 179, 190 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((#‘((0[,](√‘𝐴)) ∩ ℙ)) ≤
(#‘(1...(⌊‘(√‘𝐴)))) ↔ ((0[,](√‘𝐴)) ∩ ℙ) ≼
(1...(⌊‘(√‘𝐴))))) |
192 | 189, 191 | mpbird 246 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(#‘((0[,](√‘𝐴)) ∩ ℙ)) ≤
(#‘(1...(⌊‘(√‘𝐴))))) |
193 | | flge0nn0 12483 |
. . . . . . . . 9
⊢
(((√‘𝐴)
∈ ℝ ∧ 0 ≤ (√‘𝐴)) →
(⌊‘(√‘𝐴)) ∈
ℕ0) |
194 | 15, 56, 193 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(⌊‘(√‘𝐴)) ∈
ℕ0) |
195 | | hashfz1 12996 |
. . . . . . . 8
⊢
((⌊‘(√‘𝐴)) ∈ ℕ0 →
(#‘(1...(⌊‘(√‘𝐴)))) = (⌊‘(√‘𝐴))) |
196 | 194, 195 | syl 17 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(#‘(1...(⌊‘(√‘𝐴)))) = (⌊‘(√‘𝐴))) |
197 | 192, 196 | breqtrd 4609 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(#‘((0[,](√‘𝐴)) ∩ ℙ)) ≤
(⌊‘(√‘𝐴))) |
198 | | flle 12462 |
. . . . . . 7
⊢
((√‘𝐴)
∈ ℝ → (⌊‘(√‘𝐴)) ≤ (√‘𝐴)) |
199 | 15, 198 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(⌊‘(√‘𝐴)) ≤ (√‘𝐴)) |
200 | 175, 178,
15, 197, 199 | letrd 10073 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(#‘((0[,](√‘𝐴)) ∩ ℙ)) ≤ (√‘𝐴)) |
201 | 175, 15, 21, 176, 200 | lemul1ad 10842 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((#‘((0[,](√‘𝐴)) ∩ ℙ)) · (log‘𝐴)) ≤ ((√‘𝐴) · (log‘𝐴))) |
202 | 172, 201 | eqbrtrd 4605 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) → Σ𝑝 ∈
((0[,](√‘𝐴))
∩ ℙ)(log‘𝐴)
≤ ((√‘𝐴)
· (log‘𝐴))) |
203 | 5, 20, 22, 169, 202 | letrd 10073 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
((ψ‘𝐴) −
(θ‘𝐴)) ≤
((√‘𝐴) ·
(log‘𝐴))) |
204 | 2, 4, 22 | lesubadd2d 10505 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(((ψ‘𝐴) −
(θ‘𝐴)) ≤
((√‘𝐴) ·
(log‘𝐴)) ↔
(ψ‘𝐴) ≤
((θ‘𝐴) +
((√‘𝐴) ·
(log‘𝐴))))) |
205 | 203, 204 | mpbid 221 |
1
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤
𝐴) →
(ψ‘𝐴) ≤
((θ‘𝐴) +
((√‘𝐴) ·
(log‘𝐴)))) |