This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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