Metamath Proof Explorer


Theorem chpub

Description: An upper bound on the second Chebyshev function. (Contributed by Mario Carneiro, 8-Apr-2016)

Ref Expression
Assertion chpub ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ψ ‘ 𝐴 ) ≤ ( ( θ ‘ 𝐴 ) + ( ( √ ‘ 𝐴 ) · ( log ‘ 𝐴 ) ) ) )

Proof

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 ‘ 𝐴 ) ) ) )