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 mulridd ⊢ ( ( 𝐴 ∈ ℝ ∧ 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 mullidd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 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 mulridd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 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 ‘ 𝐴 ) ) ) )