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 
|- ( ( A e. RR /\ 1 <_ A ) -> ( psi ` A ) <_ ( ( theta ` A ) + ( ( sqrt ` A ) x. ( log ` A ) ) ) )

Proof

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