Metamath Proof Explorer

Theorem aks4d1p1p4

Description: Technical step for inequality. The hard work is in to prove the final hypothesis. (Contributed by metakunt, 19-Aug-2024)

Ref Expression
Hypotheses aks4d1p1p4.1 
|- ( ph -> N e. NN )
aks4d1p1p4.2 
|- A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
aks4d1p1p4.3 
|- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
aks4d1p1p4.4 
|- ( ph -> 3 <_ N )
aks4d1p1p4.5 
|- C = ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) )
aks4d1p1p4.6 
|- D = ( ( 2 logb N ) ^ 2 )
aks4d1p1p4.7 
|- E = ( ( 2 logb N ) ^ 4 )
aks4d1p1p4.8 
|- ( ph -> ( ( 2 x. C ) + D ) <_ E )
Assertion aks4d1p1p4 
|- ( ph -> A < ( 2 ^ B ) )

Proof

Step Hyp Ref Expression
1 aks4d1p1p4.1 
 |-  ( ph -> N e. NN )
2 aks4d1p1p4.2 
 |-  A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
3 aks4d1p1p4.3 
 |-  B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
4 aks4d1p1p4.4 
 |-  ( ph -> 3 <_ N )
5 aks4d1p1p4.5 
 |-  C = ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) )
6 aks4d1p1p4.6 
 |-  D = ( ( 2 logb N ) ^ 2 )
7 aks4d1p1p4.7 
 |-  E = ( ( 2 logb N ) ^ 4 )
8 aks4d1p1p4.8 
 |-  ( ph -> ( ( 2 x. C ) + D ) <_ E )
9 1 nnred 
 |-  ( ph -> N e. RR )
10 2re 
 |-  2 e. RR
11 10 a1i 
 |-  ( ph -> 2 e. RR )
12 2pos 
 |-  0 < 2
13 12 a1i 
 |-  ( ph -> 0 < 2 )
14 1 nngt0d 
 |-  ( ph -> 0 < N )
15 1red 
 |-  ( ph -> 1 e. RR )
16 1lt2 
 |-  1 < 2
17 16 a1i 
 |-  ( ph -> 1 < 2 )
18 15 17 ltned 
 |-  ( ph -> 1 =/= 2 )
19 18 necomd 
 |-  ( ph -> 2 =/= 1 )
20 11 13 9 14 19 relogbcld 
 |-  ( ph -> ( 2 logb N ) e. RR )
21 5nn0 
 |-  5 e. NN0
22 21 a1i 
 |-  ( ph -> 5 e. NN0 )
23 20 22 reexpcld 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) e. RR )
24 ceilcl 
 |-  ( ( ( 2 logb N ) ^ 5 ) e. RR -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
25 23 24 syl 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
26 25 zred 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. RR )
27 3 a1i 
 |-  ( ph -> B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
28 27 eleq1d 
 |-  ( ph -> ( B e. RR <-> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. RR ) )
29 26 28 mpbird 
 |-  ( ph -> B e. RR )
30 0red 
 |-  ( ph -> 0 e. RR )
31 7re 
 |-  7 e. RR
32 31 a1i 
 |-  ( ph -> 7 e. RR )
33 7pos 
 |-  0 < 7
34 33 a1i 
 |-  ( ph -> 0 < 7 )
35 9 4 3lexlogpow5ineq3 
 |-  ( ph -> 7 < ( ( 2 logb N ) ^ 5 ) )
36 32 23 35 ltled 
 |-  ( ph -> 7 <_ ( ( 2 logb N ) ^ 5 ) )
37 ceilge 
 |-  ( ( ( 2 logb N ) ^ 5 ) e. RR -> ( ( 2 logb N ) ^ 5 ) <_ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
38 23 37 syl 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) <_ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
39 38 27 breqtrrd 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) <_ B )
40 32 23 29 36 39 letrd 
 |-  ( ph -> 7 <_ B )
41 30 32 29 34 40 ltletrd 
 |-  ( ph -> 0 < B )
42 11 13 29 41 19 relogbcld 
 |-  ( ph -> ( 2 logb B ) e. RR )
43 42 flcld 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. ZZ )
44 30 15 readdcld 
 |-  ( ph -> ( 0 + 1 ) e. RR )
45 43 zred 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. RR )
46 45 15 readdcld 
 |-  ( ph -> ( ( |_ ` ( 2 logb B ) ) + 1 ) e. RR )
47 11 13 11 13 19 relogbcld 
 |-  ( ph -> ( 2 logb 2 ) e. RR )
48 15 leidd 
 |-  ( ph -> 1 <_ 1 )
49 1cnd 
 |-  ( ph -> 1 e. CC )
50 49 addlidd 
 |-  ( ph -> ( 0 + 1 ) = 1 )
51 11 recnd 
 |-  ( ph -> 2 e. CC )
52 30 13 gtned 
 |-  ( ph -> 2 =/= 0 )
53 logbid1 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) -> ( 2 logb 2 ) = 1 )
54 51 52 19 53 syl3anc 
 |-  ( ph -> ( 2 logb 2 ) = 1 )
55 54 eqcomd 
 |-  ( ph -> 1 = ( 2 logb 2 ) )
56 55 eqcomd 
 |-  ( ph -> ( 2 logb 2 ) = 1 )
57 50 56 breq12d 
 |-  ( ph -> ( ( 0 + 1 ) <_ ( 2 logb 2 ) <-> 1 <_ 1 ) )
58 48 57 mpbird 
 |-  ( ph -> ( 0 + 1 ) <_ ( 2 logb 2 ) )
59 5re 
 |-  5 e. RR
60 59 a1i 
 |-  ( ph -> 5 e. RR )
61 11 60 readdcld 
 |-  ( ph -> ( 2 + 5 ) e. RR )
62 10 21 nn0addge1i 
 |-  2 <_ ( 2 + 5 )
63 62 a1i 
 |-  ( ph -> 2 <_ ( 2 + 5 ) )
64 10 recni 
 |-  2 e. CC
65 5cn 
 |-  5 e. CC
66 64 65 addcomi 
 |-  ( 2 + 5 ) = ( 5 + 2 )
67 5p2e7 
 |-  ( 5 + 2 ) = 7
68 66 67 eqtri 
 |-  ( 2 + 5 ) = 7
69 68 a1i 
 |-  ( ph -> ( 2 + 5 ) = 7 )
70 32 leidd 
 |-  ( ph -> 7 <_ 7 )
71 69 70 eqbrtrd 
 |-  ( ph -> ( 2 + 5 ) <_ 7 )
72 11 61 32 63 71 letrd 
 |-  ( ph -> 2 <_ 7 )
73 11 32 29 72 40 letrd 
 |-  ( ph -> 2 <_ B )
74 2z 
 |-  2 e. ZZ
75 74 a1i 
 |-  ( ph -> 2 e. ZZ )
76 75 uzidd 
 |-  ( ph -> 2 e. ( ZZ>= ` 2 ) )
77 2rp 
 |-  2 e. RR+
78 77 a1i 
 |-  ( ph -> 2 e. RR+ )
79 29 41 elrpd 
 |-  ( ph -> B e. RR+ )
80 logbleb 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ 2 e. RR+ /\ B e. RR+ ) -> ( 2 <_ B <-> ( 2 logb 2 ) <_ ( 2 logb B ) ) )
81 76 78 79 80 syl3anc 
 |-  ( ph -> ( 2 <_ B <-> ( 2 logb 2 ) <_ ( 2 logb B ) ) )
82 73 81 mpbid 
 |-  ( ph -> ( 2 logb 2 ) <_ ( 2 logb B ) )
83 44 47 42 58 82 letrd 
 |-  ( ph -> ( 0 + 1 ) <_ ( 2 logb B ) )
84 fllep1 
 |-  ( ( 2 logb B ) e. RR -> ( 2 logb B ) <_ ( ( |_ ` ( 2 logb B ) ) + 1 ) )
85 42 84 syl 
 |-  ( ph -> ( 2 logb B ) <_ ( ( |_ ` ( 2 logb B ) ) + 1 ) )
86 44 42 46 83 85 letrd 
 |-  ( ph -> ( 0 + 1 ) <_ ( ( |_ ` ( 2 logb B ) ) + 1 ) )
87 30 45 15 leadd1d 
 |-  ( ph -> ( 0 <_ ( |_ ` ( 2 logb B ) ) <-> ( 0 + 1 ) <_ ( ( |_ ` ( 2 logb B ) ) + 1 ) ) )
88 86 87 mpbird 
 |-  ( ph -> 0 <_ ( |_ ` ( 2 logb B ) ) )
89 43 88 jca 
 |-  ( ph -> ( ( |_ ` ( 2 logb B ) ) e. ZZ /\ 0 <_ ( |_ ` ( 2 logb B ) ) ) )
90 elnn0z 
 |-  ( ( |_ ` ( 2 logb B ) ) e. NN0 <-> ( ( |_ ` ( 2 logb B ) ) e. ZZ /\ 0 <_ ( |_ ` ( 2 logb B ) ) ) )
91 89 90 sylibr 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. NN0 )
92 9 91 reexpcld 
 |-  ( ph -> ( N ^ ( |_ ` ( 2 logb B ) ) ) e. RR )
93 fzfid 
 |-  ( ph -> ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) e. Fin )
94 9 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> N e. RR )
95 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> k e. NN )
96 95 adantl 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> k e. NN )
97 96 nnnn0d 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> k e. NN0 )
98 94 97 reexpcld 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( N ^ k ) e. RR )
99 1red 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 1 e. RR )
100 98 99 resubcld 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( ( N ^ k ) - 1 ) e. RR )
101 93 100 fprodrecl 
 |-  ( ph -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) e. RR )
102 92 101 remulcld 
 |-  ( ph -> ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) e. RR )
103 2 a1i 
 |-  ( ph -> A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) )
104 103 eleq1d 
 |-  ( ph -> ( A e. RR <-> ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) e. RR ) )
105 102 104 mpbird 
 |-  ( ph -> A e. RR )
106 7 a1i 
 |-  ( ph -> E = ( ( 2 logb N ) ^ 4 ) )
107 106 oveq2d 
 |-  ( ph -> ( N ^c E ) = ( N ^c ( ( 2 logb N ) ^ 4 ) ) )
108 2cnd 
 |-  ( ph -> 2 e. CC )
109 78 rpne0d 
 |-  ( ph -> 2 =/= 0 )
110 109 19 nelprd 
 |-  ( ph -> -. 2 e. { 0 , 1 } )
111 108 110 eldifd 
 |-  ( ph -> 2 e. ( CC \ { 0 , 1 } ) )
112 9 recnd 
 |-  ( ph -> N e. CC )
113 30 14 ltned 
 |-  ( ph -> 0 =/= N )
114 necom 
 |-  ( 0 =/= N <-> N =/= 0 )
115 114 imbi2i 
 |-  ( ( ph -> 0 =/= N ) <-> ( ph -> N =/= 0 ) )
116 113 115 mpbi 
 |-  ( ph -> N =/= 0 )
117 116 neneqd 
 |-  ( ph -> -. N = 0 )
118 c0ex 
 |-  0 e. _V
119 118 elsn2 
 |-  ( N e. { 0 } <-> N = 0 )
120 117 119 sylnibr 
 |-  ( ph -> -. N e. { 0 } )
121 112 120 eldifd 
 |-  ( ph -> N e. ( CC \ { 0 } ) )
122 cxplogb 
 |-  ( ( 2 e. ( CC \ { 0 , 1 } ) /\ N e. ( CC \ { 0 } ) ) -> ( 2 ^c ( 2 logb N ) ) = N )
123 111 121 122 syl2anc 
 |-  ( ph -> ( 2 ^c ( 2 logb N ) ) = N )
124 123 eqcomd 
 |-  ( ph -> N = ( 2 ^c ( 2 logb N ) ) )
125 124 oveq1d 
 |-  ( ph -> ( N ^c ( ( 2 logb N ) ^ 4 ) ) = ( ( 2 ^c ( 2 logb N ) ) ^c ( ( 2 logb N ) ^ 4 ) ) )
126 eqidd 
 |-  ( ph -> ( ( 2 ^c ( 2 logb N ) ) ^c ( ( 2 logb N ) ^ 4 ) ) = ( ( 2 ^c ( 2 logb N ) ) ^c ( ( 2 logb N ) ^ 4 ) ) )
127 125 126 eqtrd 
 |-  ( ph -> ( N ^c ( ( 2 logb N ) ^ 4 ) ) = ( ( 2 ^c ( 2 logb N ) ) ^c ( ( 2 logb N ) ^ 4 ) ) )
128 107 127 eqtrd 
 |-  ( ph -> ( N ^c E ) = ( ( 2 ^c ( 2 logb N ) ) ^c ( ( 2 logb N ) ^ 4 ) ) )
129 106 eqcomd 
 |-  ( ph -> ( ( 2 logb N ) ^ 4 ) = E )
130 4nn0 
 |-  4 e. NN0
131 130 a1i 
 |-  ( ph -> 4 e. NN0 )
132 20 131 reexpcld 
 |-  ( ph -> ( ( 2 logb N ) ^ 4 ) e. RR )
133 106 eleq1d 
 |-  ( ph -> ( E e. RR <-> ( ( 2 logb N ) ^ 4 ) e. RR ) )
134 132 133 mpbird 
 |-  ( ph -> E e. RR )
135 134 recnd 
 |-  ( ph -> E e. CC )
136 129 135 eqeltrd 
 |-  ( ph -> ( ( 2 logb N ) ^ 4 ) e. CC )
137 78 20 136 cxpmuld 
 |-  ( ph -> ( 2 ^c ( ( 2 logb N ) x. ( ( 2 logb N ) ^ 4 ) ) ) = ( ( 2 ^c ( 2 logb N ) ) ^c ( ( 2 logb N ) ^ 4 ) ) )
138 137 eqcomd 
 |-  ( ph -> ( ( 2 ^c ( 2 logb N ) ) ^c ( ( 2 logb N ) ^ 4 ) ) = ( 2 ^c ( ( 2 logb N ) x. ( ( 2 logb N ) ^ 4 ) ) ) )
139 128 138 eqtrd 
 |-  ( ph -> ( N ^c E ) = ( 2 ^c ( ( 2 logb N ) x. ( ( 2 logb N ) ^ 4 ) ) ) )
140 20 recnd 
 |-  ( ph -> ( 2 logb N ) e. CC )
141 140 exp1d 
 |-  ( ph -> ( ( 2 logb N ) ^ 1 ) = ( 2 logb N ) )
142 141 eqcomd 
 |-  ( ph -> ( 2 logb N ) = ( ( 2 logb N ) ^ 1 ) )
143 142 oveq1d 
 |-  ( ph -> ( ( 2 logb N ) x. ( ( 2 logb N ) ^ 4 ) ) = ( ( ( 2 logb N ) ^ 1 ) x. ( ( 2 logb N ) ^ 4 ) ) )
144 1nn0 
 |-  1 e. NN0
145 144 a1i 
 |-  ( ph -> 1 e. NN0 )
146 140 131 145 expaddd 
 |-  ( ph -> ( ( 2 logb N ) ^ ( 1 + 4 ) ) = ( ( ( 2 logb N ) ^ 1 ) x. ( ( 2 logb N ) ^ 4 ) ) )
147 146 eqcomd 
 |-  ( ph -> ( ( ( 2 logb N ) ^ 1 ) x. ( ( 2 logb N ) ^ 4 ) ) = ( ( 2 logb N ) ^ ( 1 + 4 ) ) )
148 143 147 eqtrd 
 |-  ( ph -> ( ( 2 logb N ) x. ( ( 2 logb N ) ^ 4 ) ) = ( ( 2 logb N ) ^ ( 1 + 4 ) ) )
149 148 oveq2d 
 |-  ( ph -> ( 2 ^c ( ( 2 logb N ) x. ( ( 2 logb N ) ^ 4 ) ) ) = ( 2 ^c ( ( 2 logb N ) ^ ( 1 + 4 ) ) ) )
150 139 149 eqtrd 
 |-  ( ph -> ( N ^c E ) = ( 2 ^c ( ( 2 logb N ) ^ ( 1 + 4 ) ) ) )
151 4cn 
 |-  4 e. CC
152 ax-1cn 
 |-  1 e. CC
153 4p1e5 
 |-  ( 4 + 1 ) = 5
154 151 152 153 addcomli 
 |-  ( 1 + 4 ) = 5
155 154 a1i 
 |-  ( ph -> ( 1 + 4 ) = 5 )
156 155 oveq2d 
 |-  ( ph -> ( ( 2 logb N ) ^ ( 1 + 4 ) ) = ( ( 2 logb N ) ^ 5 ) )
157 156 oveq2d 
 |-  ( ph -> ( 2 ^c ( ( 2 logb N ) ^ ( 1 + 4 ) ) ) = ( 2 ^c ( ( 2 logb N ) ^ 5 ) ) )
158 150 157 eqtrd 
 |-  ( ph -> ( N ^c E ) = ( 2 ^c ( ( 2 logb N ) ^ 5 ) ) )
159 3re 
 |-  3 e. RR
160 159 a1i 
 |-  ( ph -> 3 e. RR )
161 0le1 
 |-  0 <_ 1
162 161 a1i 
 |-  ( ph -> 0 <_ 1 )
163 1lt3 
 |-  1 < 3
164 163 a1i 
 |-  ( ph -> 1 < 3 )
165 15 160 164 ltled 
 |-  ( ph -> 1 <_ 3 )
166 30 15 160 162 165 letrd 
 |-  ( ph -> 0 <_ 3 )
167 30 160 9 166 4 letrd 
 |-  ( ph -> 0 <_ N )
168 9 167 134 recxpcld 
 |-  ( ph -> ( N ^c E ) e. RR )
169 158 168 eqeltrrd 
 |-  ( ph -> ( 2 ^c ( ( 2 logb N ) ^ 5 ) ) e. RR )
170 27 eleq1d 
 |-  ( ph -> ( B e. ZZ <-> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ ) )
171 25 170 mpbird 
 |-  ( ph -> B e. ZZ )
172 30 29 41 ltled 
 |-  ( ph -> 0 <_ B )
173 171 172 jca 
 |-  ( ph -> ( B e. ZZ /\ 0 <_ B ) )
174 elnn0z 
 |-  ( B e. NN0 <-> ( B e. ZZ /\ 0 <_ B ) )
175 173 174 sylibr 
 |-  ( ph -> B e. NN0 )
176 11 175 reexpcld 
 |-  ( ph -> ( 2 ^ B ) e. RR )
177 9 14 elrpd 
 |-  ( ph -> N e. RR+ )
178 23 15 readdcld 
 |-  ( ph -> ( ( ( 2 logb N ) ^ 5 ) + 1 ) e. RR )
179 22 nn0zd 
 |-  ( ph -> 5 e. ZZ )
180 logb1 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) -> ( 2 logb 1 ) = 0 )
181 51 52 19 180 syl3anc 
 |-  ( ph -> ( 2 logb 1 ) = 0 )
182 181 30 eqeltrd 
 |-  ( ph -> ( 2 logb 1 ) e. RR )
183 30 leidd 
 |-  ( ph -> 0 <_ 0 )
184 181 eqcomd 
 |-  ( ph -> 0 = ( 2 logb 1 ) )
185 183 184 breqtrd 
 |-  ( ph -> 0 <_ ( 2 logb 1 ) )
186 15 160 9 164 4 ltletrd 
 |-  ( ph -> 1 < N )
187 1rp 
 |-  1 e. RR+
188 187 a1i 
 |-  ( ph -> 1 e. RR+ )
189 logblt 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ 1 e. RR+ /\ N e. RR+ ) -> ( 1 < N <-> ( 2 logb 1 ) < ( 2 logb N ) ) )
190 76 188 177 189 syl3anc 
 |-  ( ph -> ( 1 < N <-> ( 2 logb 1 ) < ( 2 logb N ) ) )
191 186 190 mpbid 
 |-  ( ph -> ( 2 logb 1 ) < ( 2 logb N ) )
192 30 182 20 185 191 lelttrd 
 |-  ( ph -> 0 < ( 2 logb N ) )
193 20 179 192 3jca 
 |-  ( ph -> ( ( 2 logb N ) e. RR /\ 5 e. ZZ /\ 0 < ( 2 logb N ) ) )
194 expgt0 
 |-  ( ( ( 2 logb N ) e. RR /\ 5 e. ZZ /\ 0 < ( 2 logb N ) ) -> 0 < ( ( 2 logb N ) ^ 5 ) )
195 193 194 syl 
 |-  ( ph -> 0 < ( ( 2 logb N ) ^ 5 ) )
196 ltp1 
 |-  ( ( ( 2 logb N ) ^ 5 ) e. RR -> ( ( 2 logb N ) ^ 5 ) < ( ( ( 2 logb N ) ^ 5 ) + 1 ) )
197 23 196 syl 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) < ( ( ( 2 logb N ) ^ 5 ) + 1 ) )
198 30 23 178 195 197 lttrd 
 |-  ( ph -> 0 < ( ( ( 2 logb N ) ^ 5 ) + 1 ) )
199 11 13 178 198 19 relogbcld 
 |-  ( ph -> ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) e. RR )
200 5 a1i 
 |-  ( ph -> C = ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) )
201 200 eleq1d 
 |-  ( ph -> ( C e. RR <-> ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) e. RR ) )
202 199 201 mpbird 
 |-  ( ph -> C e. RR )
203 20 resqcld 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) e. RR )
204 6 a1i 
 |-  ( ph -> D = ( ( 2 logb N ) ^ 2 ) )
205 204 eleq1d 
 |-  ( ph -> ( D e. RR <-> ( ( 2 logb N ) ^ 2 ) e. RR ) )
206 203 205 mpbird 
 |-  ( ph -> D e. RR )
207 206 rehalfcld 
 |-  ( ph -> ( D / 2 ) e. RR )
208 202 207 readdcld 
 |-  ( ph -> ( C + ( D / 2 ) ) e. RR )
209 134 11 109 redivcld 
 |-  ( ph -> ( E / 2 ) e. RR )
210 208 209 readdcld 
 |-  ( ph -> ( ( C + ( D / 2 ) ) + ( E / 2 ) ) e. RR )
211 177 210 rpcxpcld 
 |-  ( ph -> ( N ^c ( ( C + ( D / 2 ) ) + ( E / 2 ) ) ) e. RR+ )
212 211 rpred 
 |-  ( ph -> ( N ^c ( ( C + ( D / 2 ) ) + ( E / 2 ) ) ) e. RR )
213 1 2 3 4 aks4d1p1p2 
 |-  ( ph -> A < ( N ^c ( ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) + ( ( ( 2 logb N ) ^ 4 ) / 2 ) ) ) )
214 129 oveq1d 
 |-  ( ph -> ( ( ( 2 logb N ) ^ 4 ) / 2 ) = ( E / 2 ) )
215 214 oveq2d 
 |-  ( ph -> ( ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) + ( ( ( 2 logb N ) ^ 4 ) / 2 ) ) = ( ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) + ( E / 2 ) ) )
216 200 eqcomd 
 |-  ( ph -> ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) = C )
217 216 oveq1d 
 |-  ( ph -> ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) = ( C + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) )
218 204 eqcomd 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) = D )
219 218 oveq1d 
 |-  ( ph -> ( ( ( 2 logb N ) ^ 2 ) / 2 ) = ( D / 2 ) )
220 219 oveq2d 
 |-  ( ph -> ( C + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) = ( C + ( D / 2 ) ) )
221 217 220 eqtrd 
 |-  ( ph -> ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) = ( C + ( D / 2 ) ) )
222 221 oveq1d 
 |-  ( ph -> ( ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) + ( E / 2 ) ) = ( ( C + ( D / 2 ) ) + ( E / 2 ) ) )
223 215 222 eqtrd 
 |-  ( ph -> ( ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) + ( ( ( 2 logb N ) ^ 4 ) / 2 ) ) = ( ( C + ( D / 2 ) ) + ( E / 2 ) ) )
224 223 oveq2d 
 |-  ( ph -> ( N ^c ( ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) + ( ( ( 2 logb N ) ^ 4 ) / 2 ) ) ) = ( N ^c ( ( C + ( D / 2 ) ) + ( E / 2 ) ) ) )
225 213 224 breqtrd 
 |-  ( ph -> A < ( N ^c ( ( C + ( D / 2 ) ) + ( E / 2 ) ) ) )
226 202 recnd 
 |-  ( ph -> C e. CC )
227 226 108 109 divcan3d 
 |-  ( ph -> ( ( 2 x. C ) / 2 ) = C )
228 227 eqcomd 
 |-  ( ph -> C = ( ( 2 x. C ) / 2 ) )
229 228 oveq1d 
 |-  ( ph -> ( C + ( D / 2 ) ) = ( ( ( 2 x. C ) / 2 ) + ( D / 2 ) ) )
230 11 202 remulcld 
 |-  ( ph -> ( 2 x. C ) e. RR )
231 230 recnd 
 |-  ( ph -> ( 2 x. C ) e. CC )
232 206 recnd 
 |-  ( ph -> D e. CC )
233 231 232 51 109 divdird 
 |-  ( ph -> ( ( ( 2 x. C ) + D ) / 2 ) = ( ( ( 2 x. C ) / 2 ) + ( D / 2 ) ) )
234 233 eqcomd 
 |-  ( ph -> ( ( ( 2 x. C ) / 2 ) + ( D / 2 ) ) = ( ( ( 2 x. C ) + D ) / 2 ) )
235 229 234 eqtrd 
 |-  ( ph -> ( C + ( D / 2 ) ) = ( ( ( 2 x. C ) + D ) / 2 ) )
236 230 206 readdcld 
 |-  ( ph -> ( ( 2 x. C ) + D ) e. RR )
237 236 134 78 lediv1d 
 |-  ( ph -> ( ( ( 2 x. C ) + D ) <_ E <-> ( ( ( 2 x. C ) + D ) / 2 ) <_ ( E / 2 ) ) )
238 8 237 mpbid 
 |-  ( ph -> ( ( ( 2 x. C ) + D ) / 2 ) <_ ( E / 2 ) )
239 235 238 eqbrtrd 
 |-  ( ph -> ( C + ( D / 2 ) ) <_ ( E / 2 ) )
240 208 209 209 239 leadd1dd 
 |-  ( ph -> ( ( C + ( D / 2 ) ) + ( E / 2 ) ) <_ ( ( E / 2 ) + ( E / 2 ) ) )
241 135 2halvesd 
 |-  ( ph -> ( ( E / 2 ) + ( E / 2 ) ) = E )
242 240 241 breqtrd 
 |-  ( ph -> ( ( C + ( D / 2 ) ) + ( E / 2 ) ) <_ E )
243 9 186 210 134 cxpled 
 |-  ( ph -> ( ( ( C + ( D / 2 ) ) + ( E / 2 ) ) <_ E <-> ( N ^c ( ( C + ( D / 2 ) ) + ( E / 2 ) ) ) <_ ( N ^c E ) ) )
244 242 243 mpbid 
 |-  ( ph -> ( N ^c ( ( C + ( D / 2 ) ) + ( E / 2 ) ) ) <_ ( N ^c E ) )
245 105 212 168 225 244 ltletrd 
 |-  ( ph -> A < ( N ^c E ) )
246 245 158 breqtrd 
 |-  ( ph -> A < ( 2 ^c ( ( 2 logb N ) ^ 5 ) ) )
247 1le2 
 |-  1 <_ 2
248 247 a1i 
 |-  ( ph -> 1 <_ 2 )
249 175 nn0red 
 |-  ( ph -> B e. RR )
250 27 eqcomd 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) = B )
251 38 250 breqtrd 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) <_ B )
252 11 248 23 249 251 cxplead 
 |-  ( ph -> ( 2 ^c ( ( 2 logb N ) ^ 5 ) ) <_ ( 2 ^c B ) )
253 cxpexp 
 |-  ( ( 2 e. CC /\ B e. NN0 ) -> ( 2 ^c B ) = ( 2 ^ B ) )
254 108 175 253 syl2anc 
 |-  ( ph -> ( 2 ^c B ) = ( 2 ^ B ) )
255 252 254 breqtrd 
 |-  ( ph -> ( 2 ^c ( ( 2 logb N ) ^ 5 ) ) <_ ( 2 ^ B ) )
256 105 169 176 246 255 ltletrd 
 |-  ( ph -> A < ( 2 ^ B ) )