Step |
Hyp |
Ref |
Expression |
1 |
|
chpcl |
⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) ∈ ℝ ) |
2 |
1
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ψ ‘ 𝐴 ) ∈ ℝ ) |
3 |
|
chtcl |
⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) ∈ ℝ ) |
4 |
3
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( θ ‘ 𝐴 ) ∈ ℝ ) |
5 |
2 4
|
resubcld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ψ ‘ 𝐴 ) − ( θ ‘ 𝐴 ) ) ∈ ℝ ) |
6 |
|
simpl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℝ ) |
7 |
|
0red |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ∈ ℝ ) |
8 |
|
1red |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 1 ∈ ℝ ) |
9 |
|
0lt1 |
⊢ 0 < 1 |
10 |
9
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 < 1 ) |
11 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 1 ≤ 𝐴 ) |
12 |
7 8 6 10 11
|
ltletrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 < 𝐴 ) |
13 |
6 12
|
elrpd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℝ+ ) |
14 |
13
|
rpge0d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ≤ 𝐴 ) |
15 |
6 14
|
resqrtcld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ∈ ℝ ) |
16 |
|
ppifi |
⊢ ( ( √ ‘ 𝐴 ) ∈ ℝ → ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin ) |
17 |
15 16
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin ) |
18 |
13
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝐴 ∈ ℝ+ ) |
19 |
18
|
relogcld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( log ‘ 𝐴 ) ∈ ℝ ) |
20 |
17 19
|
fsumrecl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( log ‘ 𝐴 ) ∈ ℝ ) |
21 |
13
|
relogcld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℝ ) |
22 |
15 21
|
remulcld |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) ∈ ℝ ) |
23 |
|
ppifi |
⊢ ( 𝐴 ∈ ℝ → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin ) |
24 |
23
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∈ Fin ) |
25 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) |
26 |
25
|
elin2d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℙ ) |
27 |
|
prmnn |
⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℕ ) |
28 |
26 27
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℕ ) |
29 |
28
|
nnrpd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ ) |
30 |
29
|
relogcld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ ) |
31 |
21
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝐴 ) ∈ ℝ ) |
32 |
28
|
nnred |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ℝ ) |
33 |
|
prmuz2 |
⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ( ℤ≥ ‘ 2 ) ) |
34 |
26 33
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( ℤ≥ ‘ 2 ) ) |
35 |
|
eluz2gt1 |
⊢ ( 𝑝 ∈ ( ℤ≥ ‘ 2 ) → 1 < 𝑝 ) |
36 |
34 35
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 1 < 𝑝 ) |
37 |
32 36
|
rplogcld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ ) |
38 |
31 37
|
rerpdivcld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ ) |
39 |
|
reflcl |
⊢ ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℝ ) |
40 |
38 39
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℝ ) |
41 |
30 40
|
remulcld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ ℝ ) |
42 |
41
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ ℂ ) |
43 |
30
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℂ ) |
44 |
24 42 43
|
fsumsub |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) = ( Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ) ) |
45 |
|
0le0 |
⊢ 0 ≤ 0 |
46 |
45
|
a1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ≤ 0 ) |
47 |
8 6 6 14 11
|
lemul2ad |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 𝐴 · 1 ) ≤ ( 𝐴 · 𝐴 ) ) |
48 |
6
|
recnd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 𝐴 ∈ ℂ ) |
49 |
48
|
sqsqrtd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 ) |
50 |
48
|
mulid1d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 𝐴 · 1 ) = 𝐴 ) |
51 |
49 50
|
eqtr4d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) = ( 𝐴 · 1 ) ) |
52 |
48
|
sqvald |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) ) |
53 |
47 51 52
|
3brtr4d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) ≤ ( 𝐴 ↑ 2 ) ) |
54 |
6 14
|
sqrtge0d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ≤ ( √ ‘ 𝐴 ) ) |
55 |
15 6 54 14
|
le2sqd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( √ ‘ 𝐴 ) ≤ 𝐴 ↔ ( ( √ ‘ 𝐴 ) ↑ 2 ) ≤ ( 𝐴 ↑ 2 ) ) ) |
56 |
53 55
|
mpbird |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( √ ‘ 𝐴 ) ≤ 𝐴 ) |
57 |
|
iccss |
⊢ ( ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ ( 0 ≤ 0 ∧ ( √ ‘ 𝐴 ) ≤ 𝐴 ) ) → ( 0 [,] ( √ ‘ 𝐴 ) ) ⊆ ( 0 [,] 𝐴 ) ) |
58 |
7 6 46 56 57
|
syl22anc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 0 [,] ( √ ‘ 𝐴 ) ) ⊆ ( 0 [,] 𝐴 ) ) |
59 |
58
|
ssrind |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) |
60 |
59
|
sselda |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) |
61 |
41 30
|
resubcld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ∈ ℝ ) |
62 |
61
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ∈ ℂ ) |
63 |
60 62
|
syldan |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ∈ ℂ ) |
64 |
|
eldifi |
⊢ ( 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) |
65 |
64 43
|
sylan2 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( log ‘ 𝑝 ) ∈ ℂ ) |
66 |
65
|
mulid2d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 1 · ( log ‘ 𝑝 ) ) = ( log ‘ 𝑝 ) ) |
67 |
25
|
elin1d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ∈ ( 0 [,] 𝐴 ) ) |
68 |
|
0re |
⊢ 0 ∈ ℝ |
69 |
6
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝐴 ∈ ℝ ) |
70 |
|
elicc2 |
⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ) ) |
71 |
68 69 70
|
sylancr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ∈ ( 0 [,] 𝐴 ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ) ) |
72 |
67 71
|
mpbid |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ 𝐴 ) ) |
73 |
72
|
simp3d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ) → 𝑝 ≤ 𝐴 ) |
74 |
64 73
|
sylan2 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝑝 ≤ 𝐴 ) |
75 |
64 29
|
sylan2 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝑝 ∈ ℝ+ ) |
76 |
13
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝐴 ∈ ℝ+ ) |
77 |
75 76
|
logled |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 𝑝 ≤ 𝐴 ↔ ( log ‘ 𝑝 ) ≤ ( log ‘ 𝐴 ) ) ) |
78 |
74 77
|
mpbid |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( log ‘ 𝑝 ) ≤ ( log ‘ 𝐴 ) ) |
79 |
66 78
|
eqbrtrd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 1 · ( log ‘ 𝑝 ) ) ≤ ( log ‘ 𝐴 ) ) |
80 |
|
1red |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 1 ∈ ℝ ) |
81 |
21
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( log ‘ 𝐴 ) ∈ ℝ ) |
82 |
64 37
|
sylan2 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ ) |
83 |
80 81 82
|
lemuldivd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( 1 · ( log ‘ 𝑝 ) ) ≤ ( log ‘ 𝐴 ) ↔ 1 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) |
84 |
79 83
|
mpbid |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 1 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) |
85 |
6
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝐴 ∈ ℝ ) |
86 |
85
|
recnd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝐴 ∈ ℂ ) |
87 |
86
|
sqsqrtd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) = 𝐴 ) |
88 |
|
eldifn |
⊢ ( 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ¬ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) |
89 |
88
|
adantl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ¬ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) |
90 |
64 26
|
sylan2 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝑝 ∈ ℙ ) |
91 |
|
elin |
⊢ ( 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ↔ ( 𝑝 ∈ ( 0 [,] ( √ ‘ 𝐴 ) ) ∧ 𝑝 ∈ ℙ ) ) |
92 |
91
|
rbaib |
⊢ ( 𝑝 ∈ ℙ → ( 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ↔ 𝑝 ∈ ( 0 [,] ( √ ‘ 𝐴 ) ) ) ) |
93 |
90 92
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ↔ 𝑝 ∈ ( 0 [,] ( √ ‘ 𝐴 ) ) ) ) |
94 |
|
0red |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 0 ∈ ℝ ) |
95 |
15
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( √ ‘ 𝐴 ) ∈ ℝ ) |
96 |
64 28
|
sylan2 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝑝 ∈ ℕ ) |
97 |
96
|
nnred |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝑝 ∈ ℝ ) |
98 |
75
|
rpge0d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 0 ≤ 𝑝 ) |
99 |
|
elicc2 |
⊢ ( ( 0 ∈ ℝ ∧ ( √ ‘ 𝐴 ) ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] ( √ ‘ 𝐴 ) ) ↔ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ ( √ ‘ 𝐴 ) ) ) ) |
100 |
|
df-3an |
⊢ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ∧ 𝑝 ≤ ( √ ‘ 𝐴 ) ) ↔ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ∧ 𝑝 ≤ ( √ ‘ 𝐴 ) ) ) |
101 |
99 100
|
bitrdi |
⊢ ( ( 0 ∈ ℝ ∧ ( √ ‘ 𝐴 ) ∈ ℝ ) → ( 𝑝 ∈ ( 0 [,] ( √ ‘ 𝐴 ) ) ↔ ( ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ∧ 𝑝 ≤ ( √ ‘ 𝐴 ) ) ) ) |
102 |
101
|
baibd |
⊢ ( ( ( 0 ∈ ℝ ∧ ( √ ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝑝 ∈ ℝ ∧ 0 ≤ 𝑝 ) ) → ( 𝑝 ∈ ( 0 [,] ( √ ‘ 𝐴 ) ) ↔ 𝑝 ≤ ( √ ‘ 𝐴 ) ) ) |
103 |
94 95 97 98 102
|
syl22anc |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 𝑝 ∈ ( 0 [,] ( √ ‘ 𝐴 ) ) ↔ 𝑝 ≤ ( √ ‘ 𝐴 ) ) ) |
104 |
93 103
|
bitrd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ↔ 𝑝 ≤ ( √ ‘ 𝐴 ) ) ) |
105 |
89 104
|
mtbid |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ¬ 𝑝 ≤ ( √ ‘ 𝐴 ) ) |
106 |
95 97
|
ltnled |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( √ ‘ 𝐴 ) < 𝑝 ↔ ¬ 𝑝 ≤ ( √ ‘ 𝐴 ) ) ) |
107 |
105 106
|
mpbird |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( √ ‘ 𝐴 ) < 𝑝 ) |
108 |
54
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 0 ≤ ( √ ‘ 𝐴 ) ) |
109 |
95 97 108 98
|
lt2sqd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( √ ‘ 𝐴 ) < 𝑝 ↔ ( ( √ ‘ 𝐴 ) ↑ 2 ) < ( 𝑝 ↑ 2 ) ) ) |
110 |
107 109
|
mpbid |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( √ ‘ 𝐴 ) ↑ 2 ) < ( 𝑝 ↑ 2 ) ) |
111 |
87 110
|
eqbrtrrd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 𝐴 < ( 𝑝 ↑ 2 ) ) |
112 |
96
|
nnsqcld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 𝑝 ↑ 2 ) ∈ ℕ ) |
113 |
112
|
nnrpd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 𝑝 ↑ 2 ) ∈ ℝ+ ) |
114 |
|
logltb |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( 𝑝 ↑ 2 ) ∈ ℝ+ ) → ( 𝐴 < ( 𝑝 ↑ 2 ) ↔ ( log ‘ 𝐴 ) < ( log ‘ ( 𝑝 ↑ 2 ) ) ) ) |
115 |
76 113 114
|
syl2anc |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( 𝐴 < ( 𝑝 ↑ 2 ) ↔ ( log ‘ 𝐴 ) < ( log ‘ ( 𝑝 ↑ 2 ) ) ) ) |
116 |
111 115
|
mpbid |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( log ‘ 𝐴 ) < ( log ‘ ( 𝑝 ↑ 2 ) ) ) |
117 |
|
2z |
⊢ 2 ∈ ℤ |
118 |
|
relogexp |
⊢ ( ( 𝑝 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( log ‘ ( 𝑝 ↑ 2 ) ) = ( 2 · ( log ‘ 𝑝 ) ) ) |
119 |
75 117 118
|
sylancl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( log ‘ ( 𝑝 ↑ 2 ) ) = ( 2 · ( log ‘ 𝑝 ) ) ) |
120 |
116 119
|
breqtrd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( log ‘ 𝐴 ) < ( 2 · ( log ‘ 𝑝 ) ) ) |
121 |
|
2re |
⊢ 2 ∈ ℝ |
122 |
121
|
a1i |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → 2 ∈ ℝ ) |
123 |
81 122 82
|
ltdivmul2d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) < 2 ↔ ( log ‘ 𝐴 ) < ( 2 · ( log ‘ 𝑝 ) ) ) ) |
124 |
120 123
|
mpbird |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) < 2 ) |
125 |
|
df-2 |
⊢ 2 = ( 1 + 1 ) |
126 |
124 125
|
breqtrdi |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) < ( 1 + 1 ) ) |
127 |
64 38
|
sylan2 |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ ) |
128 |
|
1z |
⊢ 1 ∈ ℤ |
129 |
|
flbi |
⊢ ( ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) = 1 ↔ ( 1 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∧ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) < ( 1 + 1 ) ) ) ) |
130 |
127 128 129
|
sylancl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) = 1 ↔ ( 1 ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∧ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) < ( 1 + 1 ) ) ) ) |
131 |
84 126 130
|
mpbir2and |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) = 1 ) |
132 |
131
|
oveq2d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) = ( ( log ‘ 𝑝 ) · 1 ) ) |
133 |
65
|
mulid1d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( log ‘ 𝑝 ) · 1 ) = ( log ‘ 𝑝 ) ) |
134 |
132 133
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) = ( log ‘ 𝑝 ) ) |
135 |
134
|
oveq1d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) = ( ( log ‘ 𝑝 ) − ( log ‘ 𝑝 ) ) ) |
136 |
65
|
subidd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( log ‘ 𝑝 ) − ( log ‘ 𝑝 ) ) = 0 ) |
137 |
135 136
|
eqtrd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( ( 0 [,] 𝐴 ) ∩ ℙ ) ∖ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) = 0 ) |
138 |
59 63 137 24
|
fsumss |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ) |
139 |
|
chpval2 |
⊢ ( 𝐴 ∈ ℝ → ( ψ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) |
140 |
139
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ψ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) |
141 |
|
chtval |
⊢ ( 𝐴 ∈ ℝ → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ) |
142 |
141
|
adantr |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( θ ‘ 𝐴 ) = Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ) |
143 |
140 142
|
oveq12d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ψ ‘ 𝐴 ) − ( θ ‘ 𝐴 ) ) = ( Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − Σ 𝑝 ∈ ( ( 0 [,] 𝐴 ) ∩ ℙ ) ( log ‘ 𝑝 ) ) ) |
144 |
44 138 143
|
3eqtr4rd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ψ ‘ 𝐴 ) − ( θ ‘ 𝐴 ) ) = Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ) |
145 |
60 61
|
syldan |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ∈ ℝ ) |
146 |
60 41
|
syldan |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ∈ ℝ ) |
147 |
60 37
|
syldan |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ+ ) |
148 |
147
|
rpge0d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → 0 ≤ ( log ‘ 𝑝 ) ) |
149 |
|
simpr |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) |
150 |
149
|
elin2d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℙ ) |
151 |
150 27
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℕ ) |
152 |
151
|
nnrpd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → 𝑝 ∈ ℝ+ ) |
153 |
152
|
relogcld |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( log ‘ 𝑝 ) ∈ ℝ ) |
154 |
146 153
|
subge02d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( 0 ≤ ( log ‘ 𝑝 ) ↔ ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ≤ ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) ) |
155 |
148 154
|
mpbid |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ≤ ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ) |
156 |
60 38
|
syldan |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ ) |
157 |
|
flle |
⊢ ( ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ∈ ℝ → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) |
158 |
156 157
|
syl |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) |
159 |
60 40
|
syldan |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ∈ ℝ ) |
160 |
159 19 147
|
lemuldiv2d |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ≤ ( log ‘ 𝐴 ) ↔ ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ≤ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) |
161 |
158 160
|
mpbird |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) ≤ ( log ‘ 𝐴 ) ) |
162 |
145 146 19 155 161
|
letrd |
⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) ∧ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) → ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ≤ ( log ‘ 𝐴 ) ) |
163 |
17 145 19 162
|
fsumle |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( ( ( log ‘ 𝑝 ) · ( ⌊ ‘ ( ( log ‘ 𝐴 ) / ( log ‘ 𝑝 ) ) ) ) − ( log ‘ 𝑝 ) ) ≤ Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( log ‘ 𝐴 ) ) |
164 |
144 163
|
eqbrtrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ψ ‘ 𝐴 ) − ( θ ‘ 𝐴 ) ) ≤ Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( log ‘ 𝐴 ) ) |
165 |
21
|
recnd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℂ ) |
166 |
|
fsumconst |
⊢ ( ( ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin ∧ ( log ‘ 𝐴 ) ∈ ℂ ) → Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( log ‘ 𝐴 ) = ( ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) · ( log ‘ 𝐴 ) ) ) |
167 |
17 165 166
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( log ‘ 𝐴 ) = ( ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) · ( log ‘ 𝐴 ) ) ) |
168 |
|
hashcl |
⊢ ( ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin → ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ∈ ℕ0 ) |
169 |
17 168
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ∈ ℕ0 ) |
170 |
169
|
nn0red |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ∈ ℝ ) |
171 |
|
logge0 |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → 0 ≤ ( log ‘ 𝐴 ) ) |
172 |
|
reflcl |
⊢ ( ( √ ‘ 𝐴 ) ∈ ℝ → ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ∈ ℝ ) |
173 |
15 172
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ∈ ℝ ) |
174 |
|
fzfid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ∈ Fin ) |
175 |
|
ppisval |
⊢ ( ( √ ‘ 𝐴 ) ∈ ℝ → ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ∩ ℙ ) ) |
176 |
15 175
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) = ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ∩ ℙ ) ) |
177 |
|
inss1 |
⊢ ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ∩ ℙ ) ⊆ ( 2 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) |
178 |
|
2eluzge1 |
⊢ 2 ∈ ( ℤ≥ ‘ 1 ) |
179 |
|
fzss1 |
⊢ ( 2 ∈ ( ℤ≥ ‘ 1 ) → ( 2 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ⊆ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) |
180 |
178 179
|
mp1i |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( 2 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ⊆ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) |
181 |
177 180
|
sstrid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( 2 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ∩ ℙ ) ⊆ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) |
182 |
176 181
|
eqsstrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) |
183 |
|
ssdomg |
⊢ ( ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ∈ Fin → ( ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ⊆ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) → ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ≼ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) ) |
184 |
174 182 183
|
sylc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ≼ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) |
185 |
|
hashdom |
⊢ ( ( ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ∈ Fin ∧ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ∈ Fin ) → ( ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ≤ ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) ↔ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ≼ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) ) |
186 |
17 174 185
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ≤ ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) ↔ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ≼ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) ) |
187 |
184 186
|
mpbird |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ≤ ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) ) |
188 |
|
flge0nn0 |
⊢ ( ( ( √ ‘ 𝐴 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝐴 ) ) → ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ∈ ℕ0 ) |
189 |
15 54 188
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ∈ ℕ0 ) |
190 |
|
hashfz1 |
⊢ ( ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) = ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) |
191 |
189 190
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) ) = ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) |
192 |
187 191
|
breqtrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ≤ ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ) |
193 |
|
flle |
⊢ ( ( √ ‘ 𝐴 ) ∈ ℝ → ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ≤ ( √ ‘ 𝐴 ) ) |
194 |
15 193
|
syl |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ ( √ ‘ 𝐴 ) ) ≤ ( √ ‘ 𝐴 ) ) |
195 |
170 173 15 192 194
|
letrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) ≤ ( √ ‘ 𝐴 ) ) |
196 |
170 15 21 171 195
|
lemul1ad |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ♯ ‘ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ) · ( log ‘ 𝐴 ) ) ≤ ( ( √ ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) ) |
197 |
167 196
|
eqbrtrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → Σ 𝑝 ∈ ( ( 0 [,] ( √ ‘ 𝐴 ) ) ∩ ℙ ) ( log ‘ 𝐴 ) ≤ ( ( √ ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) ) |
198 |
5 20 22 164 197
|
letrd |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ψ ‘ 𝐴 ) − ( θ ‘ 𝐴 ) ) ≤ ( ( √ ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) ) |
199 |
2 4 22
|
lesubadd2d |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ( ( ψ ‘ 𝐴 ) − ( θ ‘ 𝐴 ) ) ≤ ( ( √ ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) ↔ ( ψ ‘ 𝐴 ) ≤ ( ( θ ‘ 𝐴 ) + ( ( √ ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) ) ) ) |
200 |
198 199
|
mpbid |
⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ψ ‘ 𝐴 ) ≤ ( ( θ ‘ 𝐴 ) + ( ( √ ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) ) ) |