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