Metamath Proof Explorer


Theorem chtppilimlem1

Description: Lemma for chtppilim . (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Hypotheses chtppilim.1
|- ( ph -> A e. RR+ )
chtppilim.2
|- ( ph -> A < 1 )
chtppilim.3
|- ( ph -> N e. ( 2 [,) +oo ) )
chtppilim.4
|- ( ph -> ( ( N ^c A ) / ( ppi ` N ) ) < ( 1 - A ) )
Assertion chtppilimlem1
|- ( ph -> ( ( A ^ 2 ) x. ( ( ppi ` N ) x. ( log ` N ) ) ) < ( theta ` N ) )

Proof

Step Hyp Ref Expression
1 chtppilim.1
 |-  ( ph -> A e. RR+ )
2 chtppilim.2
 |-  ( ph -> A < 1 )
3 chtppilim.3
 |-  ( ph -> N e. ( 2 [,) +oo ) )
4 chtppilim.4
 |-  ( ph -> ( ( N ^c A ) / ( ppi ` N ) ) < ( 1 - A ) )
5 1 rpred
 |-  ( ph -> A e. RR )
6 5 recnd
 |-  ( ph -> A e. CC )
7 6 sqvald
 |-  ( ph -> ( A ^ 2 ) = ( A x. A ) )
8 7 oveq1d
 |-  ( ph -> ( ( A ^ 2 ) x. ( ( ppi ` N ) x. ( log ` N ) ) ) = ( ( A x. A ) x. ( ( ppi ` N ) x. ( log ` N ) ) ) )
9 2re
 |-  2 e. RR
10 elicopnf
 |-  ( 2 e. RR -> ( N e. ( 2 [,) +oo ) <-> ( N e. RR /\ 2 <_ N ) ) )
11 9 10 ax-mp
 |-  ( N e. ( 2 [,) +oo ) <-> ( N e. RR /\ 2 <_ N ) )
12 3 11 sylib
 |-  ( ph -> ( N e. RR /\ 2 <_ N ) )
13 12 simpld
 |-  ( ph -> N e. RR )
14 ppicl
 |-  ( N e. RR -> ( ppi ` N ) e. NN0 )
15 13 14 syl
 |-  ( ph -> ( ppi ` N ) e. NN0 )
16 15 nn0red
 |-  ( ph -> ( ppi ` N ) e. RR )
17 16 recnd
 |-  ( ph -> ( ppi ` N ) e. CC )
18 0red
 |-  ( ph -> 0 e. RR )
19 9 a1i
 |-  ( ph -> 2 e. RR )
20 2pos
 |-  0 < 2
21 20 a1i
 |-  ( ph -> 0 < 2 )
22 12 simprd
 |-  ( ph -> 2 <_ N )
23 18 19 13 21 22 ltletrd
 |-  ( ph -> 0 < N )
24 13 23 elrpd
 |-  ( ph -> N e. RR+ )
25 24 relogcld
 |-  ( ph -> ( log ` N ) e. RR )
26 25 recnd
 |-  ( ph -> ( log ` N ) e. CC )
27 6 6 17 26 mul4d
 |-  ( ph -> ( ( A x. A ) x. ( ( ppi ` N ) x. ( log ` N ) ) ) = ( ( A x. ( ppi ` N ) ) x. ( A x. ( log ` N ) ) ) )
28 8 27 eqtrd
 |-  ( ph -> ( ( A ^ 2 ) x. ( ( ppi ` N ) x. ( log ` N ) ) ) = ( ( A x. ( ppi ` N ) ) x. ( A x. ( log ` N ) ) ) )
29 5 16 remulcld
 |-  ( ph -> ( A x. ( ppi ` N ) ) e. RR )
30 5 25 remulcld
 |-  ( ph -> ( A x. ( log ` N ) ) e. RR )
31 29 30 remulcld
 |-  ( ph -> ( ( A x. ( ppi ` N ) ) x. ( A x. ( log ` N ) ) ) e. RR )
32 24 5 rpcxpcld
 |-  ( ph -> ( N ^c A ) e. RR+ )
33 32 rpred
 |-  ( ph -> ( N ^c A ) e. RR )
34 ppicl
 |-  ( ( N ^c A ) e. RR -> ( ppi ` ( N ^c A ) ) e. NN0 )
35 33 34 syl
 |-  ( ph -> ( ppi ` ( N ^c A ) ) e. NN0 )
36 35 nn0red
 |-  ( ph -> ( ppi ` ( N ^c A ) ) e. RR )
37 16 36 resubcld
 |-  ( ph -> ( ( ppi ` N ) - ( ppi ` ( N ^c A ) ) ) e. RR )
38 37 30 remulcld
 |-  ( ph -> ( ( ( ppi ` N ) - ( ppi ` ( N ^c A ) ) ) x. ( A x. ( log ` N ) ) ) e. RR )
39 chtcl
 |-  ( N e. RR -> ( theta ` N ) e. RR )
40 13 39 syl
 |-  ( ph -> ( theta ` N ) e. RR )
41 1red
 |-  ( ph -> 1 e. RR )
42 1lt2
 |-  1 < 2
43 42 a1i
 |-  ( ph -> 1 < 2 )
44 41 19 13 43 22 ltletrd
 |-  ( ph -> 1 < N )
45 13 44 rplogcld
 |-  ( ph -> ( log ` N ) e. RR+ )
46 1 45 rpmulcld
 |-  ( ph -> ( A x. ( log ` N ) ) e. RR+ )
47 16 33 resubcld
 |-  ( ph -> ( ( ppi ` N ) - ( N ^c A ) ) e. RR )
48 ppinncl
 |-  ( ( N e. RR /\ 2 <_ N ) -> ( ppi ` N ) e. NN )
49 12 48 syl
 |-  ( ph -> ( ppi ` N ) e. NN )
50 33 49 nndivred
 |-  ( ph -> ( ( N ^c A ) / ( ppi ` N ) ) e. RR )
51 50 41 5 4 ltsub13d
 |-  ( ph -> A < ( 1 - ( ( N ^c A ) / ( ppi ` N ) ) ) )
52 33 recnd
 |-  ( ph -> ( N ^c A ) e. CC )
53 49 nnrpd
 |-  ( ph -> ( ppi ` N ) e. RR+ )
54 53 rpcnne0d
 |-  ( ph -> ( ( ppi ` N ) e. CC /\ ( ppi ` N ) =/= 0 ) )
55 divsubdir
 |-  ( ( ( ppi ` N ) e. CC /\ ( N ^c A ) e. CC /\ ( ( ppi ` N ) e. CC /\ ( ppi ` N ) =/= 0 ) ) -> ( ( ( ppi ` N ) - ( N ^c A ) ) / ( ppi ` N ) ) = ( ( ( ppi ` N ) / ( ppi ` N ) ) - ( ( N ^c A ) / ( ppi ` N ) ) ) )
56 17 52 54 55 syl3anc
 |-  ( ph -> ( ( ( ppi ` N ) - ( N ^c A ) ) / ( ppi ` N ) ) = ( ( ( ppi ` N ) / ( ppi ` N ) ) - ( ( N ^c A ) / ( ppi ` N ) ) ) )
57 divid
 |-  ( ( ( ppi ` N ) e. CC /\ ( ppi ` N ) =/= 0 ) -> ( ( ppi ` N ) / ( ppi ` N ) ) = 1 )
58 54 57 syl
 |-  ( ph -> ( ( ppi ` N ) / ( ppi ` N ) ) = 1 )
59 58 oveq1d
 |-  ( ph -> ( ( ( ppi ` N ) / ( ppi ` N ) ) - ( ( N ^c A ) / ( ppi ` N ) ) ) = ( 1 - ( ( N ^c A ) / ( ppi ` N ) ) ) )
60 56 59 eqtrd
 |-  ( ph -> ( ( ( ppi ` N ) - ( N ^c A ) ) / ( ppi ` N ) ) = ( 1 - ( ( N ^c A ) / ( ppi ` N ) ) ) )
61 51 60 breqtrrd
 |-  ( ph -> A < ( ( ( ppi ` N ) - ( N ^c A ) ) / ( ppi ` N ) ) )
62 5 47 53 ltmuldivd
 |-  ( ph -> ( ( A x. ( ppi ` N ) ) < ( ( ppi ` N ) - ( N ^c A ) ) <-> A < ( ( ( ppi ` N ) - ( N ^c A ) ) / ( ppi ` N ) ) ) )
63 61 62 mpbird
 |-  ( ph -> ( A x. ( ppi ` N ) ) < ( ( ppi ` N ) - ( N ^c A ) ) )
64 ppiltx
 |-  ( ( N ^c A ) e. RR+ -> ( ppi ` ( N ^c A ) ) < ( N ^c A ) )
65 32 64 syl
 |-  ( ph -> ( ppi ` ( N ^c A ) ) < ( N ^c A ) )
66 36 33 16 65 ltsub2dd
 |-  ( ph -> ( ( ppi ` N ) - ( N ^c A ) ) < ( ( ppi ` N ) - ( ppi ` ( N ^c A ) ) ) )
67 29 47 37 63 66 lttrd
 |-  ( ph -> ( A x. ( ppi ` N ) ) < ( ( ppi ` N ) - ( ppi ` ( N ^c A ) ) ) )
68 29 37 46 67 ltmul1dd
 |-  ( ph -> ( ( A x. ( ppi ` N ) ) x. ( A x. ( log ` N ) ) ) < ( ( ( ppi ` N ) - ( ppi ` ( N ^c A ) ) ) x. ( A x. ( log ` N ) ) ) )
69 fzfid
 |-  ( ph -> ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) e. Fin )
70 inss1
 |-  ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) C_ ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) )
71 ssfi
 |-  ( ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) e. Fin /\ ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) C_ ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) ) -> ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) e. Fin )
72 69 70 71 sylancl
 |-  ( ph -> ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) e. Fin )
73 simpr
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) )
74 73 elin2d
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> p e. Prime )
75 prmnn
 |-  ( p e. Prime -> p e. NN )
76 75 nnrpd
 |-  ( p e. Prime -> p e. RR+ )
77 74 76 syl
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> p e. RR+ )
78 77 relogcld
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> ( log ` p ) e. RR )
79 72 78 fsumrecl
 |-  ( ph -> sum_ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ( log ` p ) e. RR )
80 30 recnd
 |-  ( ph -> ( A x. ( log ` N ) ) e. CC )
81 fsumconst
 |-  ( ( ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) e. Fin /\ ( A x. ( log ` N ) ) e. CC ) -> sum_ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ( A x. ( log ` N ) ) = ( ( # ` ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) x. ( A x. ( log ` N ) ) ) )
82 72 80 81 syl2anc
 |-  ( ph -> sum_ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ( A x. ( log ` N ) ) = ( ( # ` ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) x. ( A x. ( log ` N ) ) ) )
83 ppifl
 |-  ( N e. RR -> ( ppi ` ( |_ ` N ) ) = ( ppi ` N ) )
84 13 83 syl
 |-  ( ph -> ( ppi ` ( |_ ` N ) ) = ( ppi ` N ) )
85 ppifl
 |-  ( ( N ^c A ) e. RR -> ( ppi ` ( |_ ` ( N ^c A ) ) ) = ( ppi ` ( N ^c A ) ) )
86 33 85 syl
 |-  ( ph -> ( ppi ` ( |_ ` ( N ^c A ) ) ) = ( ppi ` ( N ^c A ) ) )
87 84 86 oveq12d
 |-  ( ph -> ( ( ppi ` ( |_ ` N ) ) - ( ppi ` ( |_ ` ( N ^c A ) ) ) ) = ( ( ppi ` N ) - ( ppi ` ( N ^c A ) ) ) )
88 41 13 44 ltled
 |-  ( ph -> 1 <_ N )
89 1re
 |-  1 e. RR
90 ltle
 |-  ( ( A e. RR /\ 1 e. RR ) -> ( A < 1 -> A <_ 1 ) )
91 5 89 90 sylancl
 |-  ( ph -> ( A < 1 -> A <_ 1 ) )
92 2 91 mpd
 |-  ( ph -> A <_ 1 )
93 13 88 5 41 92 cxplead
 |-  ( ph -> ( N ^c A ) <_ ( N ^c 1 ) )
94 13 recnd
 |-  ( ph -> N e. CC )
95 94 cxp1d
 |-  ( ph -> ( N ^c 1 ) = N )
96 93 95 breqtrd
 |-  ( ph -> ( N ^c A ) <_ N )
97 flword2
 |-  ( ( ( N ^c A ) e. RR /\ N e. RR /\ ( N ^c A ) <_ N ) -> ( |_ ` N ) e. ( ZZ>= ` ( |_ ` ( N ^c A ) ) ) )
98 33 13 96 97 syl3anc
 |-  ( ph -> ( |_ ` N ) e. ( ZZ>= ` ( |_ ` ( N ^c A ) ) ) )
99 ppidif
 |-  ( ( |_ ` N ) e. ( ZZ>= ` ( |_ ` ( N ^c A ) ) ) -> ( ( ppi ` ( |_ ` N ) ) - ( ppi ` ( |_ ` ( N ^c A ) ) ) ) = ( # ` ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) )
100 98 99 syl
 |-  ( ph -> ( ( ppi ` ( |_ ` N ) ) - ( ppi ` ( |_ ` ( N ^c A ) ) ) ) = ( # ` ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) )
101 87 100 eqtr3d
 |-  ( ph -> ( ( ppi ` N ) - ( ppi ` ( N ^c A ) ) ) = ( # ` ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) )
102 101 oveq1d
 |-  ( ph -> ( ( ( ppi ` N ) - ( ppi ` ( N ^c A ) ) ) x. ( A x. ( log ` N ) ) ) = ( ( # ` ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) x. ( A x. ( log ` N ) ) ) )
103 82 102 eqtr4d
 |-  ( ph -> sum_ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ( A x. ( log ` N ) ) = ( ( ( ppi ` N ) - ( ppi ` ( N ^c A ) ) ) x. ( A x. ( log ` N ) ) ) )
104 30 adantr
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> ( A x. ( log ` N ) ) e. RR )
105 33 adantr
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> ( N ^c A ) e. RR )
106 reflcl
 |-  ( ( N ^c A ) e. RR -> ( |_ ` ( N ^c A ) ) e. RR )
107 peano2re
 |-  ( ( |_ ` ( N ^c A ) ) e. RR -> ( ( |_ ` ( N ^c A ) ) + 1 ) e. RR )
108 33 106 107 3syl
 |-  ( ph -> ( ( |_ ` ( N ^c A ) ) + 1 ) e. RR )
109 108 adantr
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> ( ( |_ ` ( N ^c A ) ) + 1 ) e. RR )
110 77 rpred
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> p e. RR )
111 fllep1
 |-  ( ( N ^c A ) e. RR -> ( N ^c A ) <_ ( ( |_ ` ( N ^c A ) ) + 1 ) )
112 33 111 syl
 |-  ( ph -> ( N ^c A ) <_ ( ( |_ ` ( N ^c A ) ) + 1 ) )
113 112 adantr
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> ( N ^c A ) <_ ( ( |_ ` ( N ^c A ) ) + 1 ) )
114 73 elin1d
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> p e. ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) )
115 elfzle1
 |-  ( p e. ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) -> ( ( |_ ` ( N ^c A ) ) + 1 ) <_ p )
116 114 115 syl
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> ( ( |_ ` ( N ^c A ) ) + 1 ) <_ p )
117 105 109 110 113 116 letrd
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> ( N ^c A ) <_ p )
118 24 rpne0d
 |-  ( ph -> N =/= 0 )
119 94 118 6 cxpefd
 |-  ( ph -> ( N ^c A ) = ( exp ` ( A x. ( log ` N ) ) ) )
120 119 eqcomd
 |-  ( ph -> ( exp ` ( A x. ( log ` N ) ) ) = ( N ^c A ) )
121 120 adantr
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> ( exp ` ( A x. ( log ` N ) ) ) = ( N ^c A ) )
122 77 reeflogd
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> ( exp ` ( log ` p ) ) = p )
123 117 121 122 3brtr4d
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> ( exp ` ( A x. ( log ` N ) ) ) <_ ( exp ` ( log ` p ) ) )
124 efle
 |-  ( ( ( A x. ( log ` N ) ) e. RR /\ ( log ` p ) e. RR ) -> ( ( A x. ( log ` N ) ) <_ ( log ` p ) <-> ( exp ` ( A x. ( log ` N ) ) ) <_ ( exp ` ( log ` p ) ) ) )
125 104 78 124 syl2anc
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> ( ( A x. ( log ` N ) ) <_ ( log ` p ) <-> ( exp ` ( A x. ( log ` N ) ) ) <_ ( exp ` ( log ` p ) ) ) )
126 123 125 mpbird
 |-  ( ( ph /\ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ) -> ( A x. ( log ` N ) ) <_ ( log ` p ) )
127 72 104 78 126 fsumle
 |-  ( ph -> sum_ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ( A x. ( log ` N ) ) <_ sum_ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ( log ` p ) )
128 103 127 eqbrtrrd
 |-  ( ph -> ( ( ( ppi ` N ) - ( ppi ` ( N ^c A ) ) ) x. ( A x. ( log ` N ) ) ) <_ sum_ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ( log ` p ) )
129 fzfid
 |-  ( ph -> ( 1 ... ( |_ ` N ) ) e. Fin )
130 inss1
 |-  ( ( 1 ... ( |_ ` N ) ) i^i Prime ) C_ ( 1 ... ( |_ ` N ) )
131 ssfi
 |-  ( ( ( 1 ... ( |_ ` N ) ) e. Fin /\ ( ( 1 ... ( |_ ` N ) ) i^i Prime ) C_ ( 1 ... ( |_ ` N ) ) ) -> ( ( 1 ... ( |_ ` N ) ) i^i Prime ) e. Fin )
132 129 130 131 sylancl
 |-  ( ph -> ( ( 1 ... ( |_ ` N ) ) i^i Prime ) e. Fin )
133 simpr
 |-  ( ( ph /\ p e. ( ( 1 ... ( |_ ` N ) ) i^i Prime ) ) -> p e. ( ( 1 ... ( |_ ` N ) ) i^i Prime ) )
134 133 elin2d
 |-  ( ( ph /\ p e. ( ( 1 ... ( |_ ` N ) ) i^i Prime ) ) -> p e. Prime )
135 prmuz2
 |-  ( p e. Prime -> p e. ( ZZ>= ` 2 ) )
136 134 135 syl
 |-  ( ( ph /\ p e. ( ( 1 ... ( |_ ` N ) ) i^i Prime ) ) -> p e. ( ZZ>= ` 2 ) )
137 eluz2b2
 |-  ( p e. ( ZZ>= ` 2 ) <-> ( p e. NN /\ 1 < p ) )
138 136 137 sylib
 |-  ( ( ph /\ p e. ( ( 1 ... ( |_ ` N ) ) i^i Prime ) ) -> ( p e. NN /\ 1 < p ) )
139 138 simpld
 |-  ( ( ph /\ p e. ( ( 1 ... ( |_ ` N ) ) i^i Prime ) ) -> p e. NN )
140 139 nnred
 |-  ( ( ph /\ p e. ( ( 1 ... ( |_ ` N ) ) i^i Prime ) ) -> p e. RR )
141 138 simprd
 |-  ( ( ph /\ p e. ( ( 1 ... ( |_ ` N ) ) i^i Prime ) ) -> 1 < p )
142 140 141 rplogcld
 |-  ( ( ph /\ p e. ( ( 1 ... ( |_ ` N ) ) i^i Prime ) ) -> ( log ` p ) e. RR+ )
143 142 rpred
 |-  ( ( ph /\ p e. ( ( 1 ... ( |_ ` N ) ) i^i Prime ) ) -> ( log ` p ) e. RR )
144 142 rpge0d
 |-  ( ( ph /\ p e. ( ( 1 ... ( |_ ` N ) ) i^i Prime ) ) -> 0 <_ ( log ` p ) )
145 32 rpge0d
 |-  ( ph -> 0 <_ ( N ^c A ) )
146 flge0nn0
 |-  ( ( ( N ^c A ) e. RR /\ 0 <_ ( N ^c A ) ) -> ( |_ ` ( N ^c A ) ) e. NN0 )
147 33 145 146 syl2anc
 |-  ( ph -> ( |_ ` ( N ^c A ) ) e. NN0 )
148 nn0p1nn
 |-  ( ( |_ ` ( N ^c A ) ) e. NN0 -> ( ( |_ ` ( N ^c A ) ) + 1 ) e. NN )
149 147 148 syl
 |-  ( ph -> ( ( |_ ` ( N ^c A ) ) + 1 ) e. NN )
150 nnuz
 |-  NN = ( ZZ>= ` 1 )
151 149 150 eleqtrdi
 |-  ( ph -> ( ( |_ ` ( N ^c A ) ) + 1 ) e. ( ZZ>= ` 1 ) )
152 fzss1
 |-  ( ( ( |_ ` ( N ^c A ) ) + 1 ) e. ( ZZ>= ` 1 ) -> ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) C_ ( 1 ... ( |_ ` N ) ) )
153 ssrin
 |-  ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) C_ ( 1 ... ( |_ ` N ) ) -> ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) C_ ( ( 1 ... ( |_ ` N ) ) i^i Prime ) )
154 151 152 153 3syl
 |-  ( ph -> ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) C_ ( ( 1 ... ( |_ ` N ) ) i^i Prime ) )
155 132 143 144 154 fsumless
 |-  ( ph -> sum_ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ( log ` p ) <_ sum_ p e. ( ( 1 ... ( |_ ` N ) ) i^i Prime ) ( log ` p ) )
156 chtval
 |-  ( N e. RR -> ( theta ` N ) = sum_ p e. ( ( 0 [,] N ) i^i Prime ) ( log ` p ) )
157 13 156 syl
 |-  ( ph -> ( theta ` N ) = sum_ p e. ( ( 0 [,] N ) i^i Prime ) ( log ` p ) )
158 2eluzge1
 |-  2 e. ( ZZ>= ` 1 )
159 ppisval2
 |-  ( ( N e. RR /\ 2 e. ( ZZ>= ` 1 ) ) -> ( ( 0 [,] N ) i^i Prime ) = ( ( 1 ... ( |_ ` N ) ) i^i Prime ) )
160 13 158 159 sylancl
 |-  ( ph -> ( ( 0 [,] N ) i^i Prime ) = ( ( 1 ... ( |_ ` N ) ) i^i Prime ) )
161 160 sumeq1d
 |-  ( ph -> sum_ p e. ( ( 0 [,] N ) i^i Prime ) ( log ` p ) = sum_ p e. ( ( 1 ... ( |_ ` N ) ) i^i Prime ) ( log ` p ) )
162 157 161 eqtrd
 |-  ( ph -> ( theta ` N ) = sum_ p e. ( ( 1 ... ( |_ ` N ) ) i^i Prime ) ( log ` p ) )
163 155 162 breqtrrd
 |-  ( ph -> sum_ p e. ( ( ( ( |_ ` ( N ^c A ) ) + 1 ) ... ( |_ ` N ) ) i^i Prime ) ( log ` p ) <_ ( theta ` N ) )
164 38 79 40 128 163 letrd
 |-  ( ph -> ( ( ( ppi ` N ) - ( ppi ` ( N ^c A ) ) ) x. ( A x. ( log ` N ) ) ) <_ ( theta ` N ) )
165 31 38 40 68 164 ltletrd
 |-  ( ph -> ( ( A x. ( ppi ` N ) ) x. ( A x. ( log ` N ) ) ) < ( theta ` N ) )
166 28 165 eqbrtrd
 |-  ( ph -> ( ( A ^ 2 ) x. ( ( ppi ` N ) x. ( log ` N ) ) ) < ( theta ` N ) )