Metamath Proof Explorer

Theorem aks4d1p1p2

Description: Rewrite A in more suitable form. (Contributed by metakunt, 19-Aug-2024)

Ref Expression
Hypotheses aks4d1p1p2.1 
|- ( ph -> N e. NN )
aks4d1p1p2.2 
|- A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
aks4d1p1p2.3 
|- B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
aks4d1p1p2.4 
|- ( ph -> 3 <_ N )
Assertion aks4d1p1p2 
|- ( ph -> A < ( N ^c ( ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) + ( ( ( 2 logb N ) ^ 4 ) / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 aks4d1p1p2.1 
 |-  ( ph -> N e. NN )
2 aks4d1p1p2.2 
 |-  A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
3 aks4d1p1p2.3 
 |-  B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
4 aks4d1p1p2.4 
 |-  ( ph -> 3 <_ N )
5 1 nnred 
 |-  ( ph -> N e. RR )
6 2re 
 |-  2 e. RR
7 6 a1i 
 |-  ( ph -> 2 e. RR )
8 2pos 
 |-  0 < 2
9 8 a1i 
 |-  ( ph -> 0 < 2 )
10 1 nngt0d 
 |-  ( ph -> 0 < N )
11 1red 
 |-  ( ph -> 1 e. RR )
12 1lt2 
 |-  1 < 2
13 12 a1i 
 |-  ( ph -> 1 < 2 )
14 11 13 ltned 
 |-  ( ph -> 1 =/= 2 )
15 14 necomd 
 |-  ( ph -> 2 =/= 1 )
16 7 9 5 10 15 relogbcld 
 |-  ( ph -> ( 2 logb N ) e. RR )
17 5nn0 
 |-  5 e. NN0
18 17 a1i 
 |-  ( ph -> 5 e. NN0 )
19 16 18 reexpcld 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) e. RR )
20 ceilcl 
 |-  ( ( ( 2 logb N ) ^ 5 ) e. RR -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
21 19 20 syl 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. ZZ )
22 21 zred 
 |-  ( ph -> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. RR )
23 3 a1i 
 |-  ( ph -> B = ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
24 23 eleq1d 
 |-  ( ph -> ( B e. RR <-> ( |^ ` ( ( 2 logb N ) ^ 5 ) ) e. RR ) )
25 22 24 mpbird 
 |-  ( ph -> B e. RR )
26 0red 
 |-  ( ph -> 0 e. RR )
27 18 nn0zd 
 |-  ( ph -> 5 e. ZZ )
28 3re 
 |-  3 e. RR
29 28 a1i 
 |-  ( ph -> 3 e. RR )
30 1lt3 
 |-  1 < 3
31 30 a1i 
 |-  ( ph -> 1 < 3 )
32 11 29 5 31 4 ltletrd 
 |-  ( ph -> 1 < N )
33 5 10 elrpd 
 |-  ( ph -> N e. RR+ )
34 2rp 
 |-  2 e. RR+
35 34 12 pm3.2i 
 |-  ( 2 e. RR+ /\ 1 < 2 )
36 35 a1i 
 |-  ( ph -> ( 2 e. RR+ /\ 1 < 2 ) )
37 logbgt0b 
 |-  ( ( N e. RR+ /\ ( 2 e. RR+ /\ 1 < 2 ) ) -> ( 0 < ( 2 logb N ) <-> 1 < N ) )
38 33 36 37 syl2anc 
 |-  ( ph -> ( 0 < ( 2 logb N ) <-> 1 < N ) )
39 32 38 mpbird 
 |-  ( ph -> 0 < ( 2 logb N ) )
40 expgt0 
 |-  ( ( ( 2 logb N ) e. RR /\ 5 e. ZZ /\ 0 < ( 2 logb N ) ) -> 0 < ( ( 2 logb N ) ^ 5 ) )
41 16 27 39 40 syl3anc 
 |-  ( ph -> 0 < ( ( 2 logb N ) ^ 5 ) )
42 ceilge 
 |-  ( ( ( 2 logb N ) ^ 5 ) e. RR -> ( ( 2 logb N ) ^ 5 ) <_ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
43 19 42 syl 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) <_ ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
44 26 19 22 41 43 ltletrd 
 |-  ( ph -> 0 < ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
45 23 breq2d 
 |-  ( ph -> ( 0 < B <-> 0 < ( |^ ` ( ( 2 logb N ) ^ 5 ) ) ) )
46 44 45 mpbird 
 |-  ( ph -> 0 < B )
47 7 9 25 46 15 relogbcld 
 |-  ( ph -> ( 2 logb B ) e. RR )
48 47 flcld 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. ZZ )
49 7re 
 |-  7 e. RR
50 49 a1i 
 |-  ( ph -> 7 e. RR )
51 1lt7 
 |-  1 < 7
52 51 a1i 
 |-  ( ph -> 1 < 7 )
53 5 4 3lexlogpow5ineq3 
 |-  ( ph -> 7 < ( ( 2 logb N ) ^ 5 ) )
54 11 50 19 52 53 lttrd 
 |-  ( ph -> 1 < ( ( 2 logb N ) ^ 5 ) )
55 11 19 22 54 43 ltletrd 
 |-  ( ph -> 1 < ( |^ ` ( ( 2 logb N ) ^ 5 ) ) )
56 23 breq2d 
 |-  ( ph -> ( 1 < B <-> 1 < ( |^ ` ( ( 2 logb N ) ^ 5 ) ) ) )
57 55 56 mpbird 
 |-  ( ph -> 1 < B )
58 25 46 elrpd 
 |-  ( ph -> B e. RR+ )
59 logbgt0b 
 |-  ( ( B e. RR+ /\ ( 2 e. RR+ /\ 1 < 2 ) ) -> ( 0 < ( 2 logb B ) <-> 1 < B ) )
60 58 36 59 syl2anc 
 |-  ( ph -> ( 0 < ( 2 logb B ) <-> 1 < B ) )
61 57 60 mpbird 
 |-  ( ph -> 0 < ( 2 logb B ) )
62 26 47 61 ltled 
 |-  ( ph -> 0 <_ ( 2 logb B ) )
63 0zd 
 |-  ( ph -> 0 e. ZZ )
64 flge 
 |-  ( ( ( 2 logb B ) e. RR /\ 0 e. ZZ ) -> ( 0 <_ ( 2 logb B ) <-> 0 <_ ( |_ ` ( 2 logb B ) ) ) )
65 47 63 64 syl2anc 
 |-  ( ph -> ( 0 <_ ( 2 logb B ) <-> 0 <_ ( |_ ` ( 2 logb B ) ) ) )
66 62 65 mpbid 
 |-  ( ph -> 0 <_ ( |_ ` ( 2 logb B ) ) )
67 48 66 jca 
 |-  ( ph -> ( ( |_ ` ( 2 logb B ) ) e. ZZ /\ 0 <_ ( |_ ` ( 2 logb B ) ) ) )
68 elnn0z 
 |-  ( ( |_ ` ( 2 logb B ) ) e. NN0 <-> ( ( |_ ` ( 2 logb B ) ) e. ZZ /\ 0 <_ ( |_ ` ( 2 logb B ) ) ) )
69 67 68 sylibr 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. NN0 )
70 5 69 reexpcld 
 |-  ( ph -> ( N ^ ( |_ ` ( 2 logb B ) ) ) e. RR )
71 fzfid 
 |-  ( ph -> ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) e. Fin )
72 5 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> N e. RR )
73 elfznn 
 |-  ( k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) -> k e. NN )
74 73 adantl 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> k e. NN )
75 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
76 74 75 syl 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> k e. NN0 )
77 72 76 reexpcld 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( N ^ k ) e. RR )
78 1red 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 1 e. RR )
79 77 78 resubcld 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( ( N ^ k ) - 1 ) e. RR )
80 71 79 fprodrecl 
 |-  ( ph -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) e. RR )
81 70 80 remulcld 
 |-  ( ph -> ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) e. RR )
82 2 a1i 
 |-  ( ph -> A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) )
83 82 eleq1d 
 |-  ( ph -> ( A e. RR <-> ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) e. RR ) )
84 81 83 mpbird 
 |-  ( ph -> A e. RR )
85 1 nnnn0d 
 |-  ( ph -> N e. NN0 )
86 85 nn0ge0d 
 |-  ( ph -> 0 <_ N )
87 19 11 readdcld 
 |-  ( ph -> ( ( ( 2 logb N ) ^ 5 ) + 1 ) e. RR )
88 19 ltp1d 
 |-  ( ph -> ( ( 2 logb N ) ^ 5 ) < ( ( ( 2 logb N ) ^ 5 ) + 1 ) )
89 26 19 87 41 88 lttrd 
 |-  ( ph -> 0 < ( ( ( 2 logb N ) ^ 5 ) + 1 ) )
90 7 9 87 89 15 relogbcld 
 |-  ( ph -> ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) e. RR )
91 16 resqcld 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) e. RR )
92 91 flcld 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) ^ 2 ) ) e. ZZ )
93 92 zred 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) ^ 2 ) ) e. RR )
94 0lt1 
 |-  0 < 1
95 94 a1i 
 |-  ( ph -> 0 < 1 )
96 7 9 7 9 15 relogbcld 
 |-  ( ph -> ( 2 logb 2 ) e. RR )
97 96 resqcld 
 |-  ( ph -> ( ( 2 logb 2 ) ^ 2 ) e. RR )
98 2nn0 
 |-  2 e. NN0
99 98 a1i 
 |-  ( ph -> 2 e. NN0 )
100 11 leidd 
 |-  ( ph -> 1 <_ 1 )
101 7 recnd 
 |-  ( ph -> 2 e. CC )
102 26 9 gtned 
 |-  ( ph -> 2 =/= 0 )
103 logbid1 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) -> ( 2 logb 2 ) = 1 )
104 101 102 15 103 syl3anc 
 |-  ( ph -> ( 2 logb 2 ) = 1 )
105 104 eqcomd 
 |-  ( ph -> 1 = ( 2 logb 2 ) )
106 100 105 breqtrd 
 |-  ( ph -> 1 <_ ( 2 logb 2 ) )
107 96 99 106 expge1d 
 |-  ( ph -> 1 <_ ( ( 2 logb 2 ) ^ 2 ) )
108 105 eqcomd 
 |-  ( ph -> ( 2 logb 2 ) = 1 )
109 108 oveq1d 
 |-  ( ph -> ( ( 2 logb 2 ) ^ 2 ) = ( 1 ^ 2 ) )
110 99 nn0zd 
 |-  ( ph -> 2 e. ZZ )
111 1exp 
 |-  ( 2 e. ZZ -> ( 1 ^ 2 ) = 1 )
112 110 111 syl 
 |-  ( ph -> ( 1 ^ 2 ) = 1 )
113 109 112 eqtrd 
 |-  ( ph -> ( ( 2 logb 2 ) ^ 2 ) = 1 )
114 7 leidd 
 |-  ( ph -> 2 <_ 2 )
115 1nn0 
 |-  1 e. NN0
116 6 115 nn0addge1i 
 |-  2 <_ ( 2 + 1 )
117 2p1e3 
 |-  ( 2 + 1 ) = 3
118 116 117 breqtri 
 |-  2 <_ 3
119 118 a1i 
 |-  ( ph -> 2 <_ 3 )
120 7 29 5 119 4 letrd 
 |-  ( ph -> 2 <_ N )
121 110 114 7 9 5 10 120 logblebd 
 |-  ( ph -> ( 2 logb 2 ) <_ ( 2 logb N ) )
122 11 96 16 106 121 letrd 
 |-  ( ph -> 1 <_ ( 2 logb N ) )
123 16 99 122 expge1d 
 |-  ( ph -> 1 <_ ( ( 2 logb N ) ^ 2 ) )
124 113 123 eqbrtrd 
 |-  ( ph -> ( ( 2 logb 2 ) ^ 2 ) <_ ( ( 2 logb N ) ^ 2 ) )
125 1z 
 |-  1 e. ZZ
126 zsqcl 
 |-  ( 1 e. ZZ -> ( 1 ^ 2 ) e. ZZ )
127 125 126 ax-mp 
 |-  ( 1 ^ 2 ) e. ZZ
128 127 a1i 
 |-  ( ph -> ( 1 ^ 2 ) e. ZZ )
129 109 eleq1d 
 |-  ( ph -> ( ( ( 2 logb 2 ) ^ 2 ) e. ZZ <-> ( 1 ^ 2 ) e. ZZ ) )
130 128 129 mpbird 
 |-  ( ph -> ( ( 2 logb 2 ) ^ 2 ) e. ZZ )
131 91 130 jca 
 |-  ( ph -> ( ( ( 2 logb N ) ^ 2 ) e. RR /\ ( ( 2 logb 2 ) ^ 2 ) e. ZZ ) )
132 flge 
 |-  ( ( ( ( 2 logb N ) ^ 2 ) e. RR /\ ( ( 2 logb 2 ) ^ 2 ) e. ZZ ) -> ( ( ( 2 logb 2 ) ^ 2 ) <_ ( ( 2 logb N ) ^ 2 ) <-> ( ( 2 logb 2 ) ^ 2 ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) )
133 131 132 syl 
 |-  ( ph -> ( ( ( 2 logb 2 ) ^ 2 ) <_ ( ( 2 logb N ) ^ 2 ) <-> ( ( 2 logb 2 ) ^ 2 ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) )
134 124 133 mpbid 
 |-  ( ph -> ( ( 2 logb 2 ) ^ 2 ) <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) )
135 11 97 93 107 134 letrd 
 |-  ( ph -> 1 <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) )
136 26 11 93 95 135 ltletrd 
 |-  ( ph -> 0 < ( |_ ` ( ( 2 logb N ) ^ 2 ) ) )
137 92 136 jca 
 |-  ( ph -> ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) e. ZZ /\ 0 < ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) )
138 elnnz 
 |-  ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) e. NN <-> ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) e. ZZ /\ 0 < ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) )
139 138 bicomi 
 |-  ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) e. ZZ /\ 0 < ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) <-> ( |_ ` ( ( 2 logb N ) ^ 2 ) ) e. NN )
140 139 a1i 
 |-  ( ph -> ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) e. ZZ /\ 0 < ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) <-> ( |_ ` ( ( 2 logb N ) ^ 2 ) ) e. NN ) )
141 137 140 mpbid 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) ^ 2 ) ) e. NN )
142 141 nnnn0d 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) ^ 2 ) ) e. NN0 )
143 arisum 
 |-  ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) e. NN0 -> sum_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) k = ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) )
144 142 143 syl 
 |-  ( ph -> sum_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) k = ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) )
145 74 nnred 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> k e. RR )
146 71 145 fsumrecl 
 |-  ( ph -> sum_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) k e. RR )
147 144 146 eqeltrrd 
 |-  ( ph -> ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) e. RR )
148 90 147 readdcld 
 |-  ( ph -> ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) ) e. RR )
149 5 86 148 recxpcld 
 |-  ( ph -> ( N ^c ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) ) ) e. RR )
150 4nn0 
 |-  4 e. NN0
151 150 a1i 
 |-  ( ph -> 4 e. NN0 )
152 16 151 reexpcld 
 |-  ( ph -> ( ( 2 logb N ) ^ 4 ) e. RR )
153 152 91 readdcld 
 |-  ( ph -> ( ( ( 2 logb N ) ^ 4 ) + ( ( 2 logb N ) ^ 2 ) ) e. RR )
154 153 rehalfcld 
 |-  ( ph -> ( ( ( ( 2 logb N ) ^ 4 ) + ( ( 2 logb N ) ^ 2 ) ) / 2 ) e. RR )
155 90 154 readdcld 
 |-  ( ph -> ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( 2 logb N ) ^ 4 ) + ( ( 2 logb N ) ^ 2 ) ) / 2 ) ) e. RR )
156 5 86 155 recxpcld 
 |-  ( ph -> ( N ^c ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( 2 logb N ) ^ 4 ) + ( ( 2 logb N ) ^ 2 ) ) / 2 ) ) ) e. RR )
157 reflcl 
 |-  ( ( 2 logb B ) e. RR -> ( |_ ` ( 2 logb B ) ) e. RR )
158 47 157 syl 
 |-  ( ph -> ( |_ ` ( 2 logb B ) ) e. RR )
159 5 86 158 recxpcld 
 |-  ( ph -> ( N ^c ( |_ ` ( 2 logb B ) ) ) e. RR )
160 33 146 rpcxpcld 
 |-  ( ph -> ( N ^c sum_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) k ) e. RR+ )
161 33 141 aks4d1p1p1 
 |-  ( ph -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) = ( N ^c sum_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) k ) )
162 161 eleq1d 
 |-  ( ph -> ( prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) e. RR+ <-> ( N ^c sum_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) k ) e. RR+ ) )
163 160 162 mpbird 
 |-  ( ph -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) e. RR+ )
164 163 rpregt0d 
 |-  ( ph -> ( prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) e. RR /\ 0 < prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) )
165 164 simpld 
 |-  ( ph -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) e. RR )
166 159 165 remulcld 
 |-  ( ph -> ( ( N ^c ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) e. RR )
167 5 86 90 recxpcld 
 |-  ( ph -> ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) e. RR )
168 167 165 remulcld 
 |-  ( ph -> ( ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) e. RR )
169 71 77 fprodrecl 
 |-  ( ph -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^ k ) e. RR )
170 5 69 86 expge0d 
 |-  ( ph -> 0 <_ ( N ^ ( |_ ` ( 2 logb B ) ) ) )
171 nfv 
 |-  F/ k ph
172 0red 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 0 e. RR )
173 1 nnge1d 
 |-  ( ph -> 1 <_ N )
174 173 adantr 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 1 <_ N )
175 72 76 174 expge1d 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 1 <_ ( N ^ k ) )
176 77 recnd 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( N ^ k ) e. CC )
177 176 subid1d 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( ( N ^ k ) - 0 ) = ( N ^ k ) )
178 177 breq2d 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( 1 <_ ( ( N ^ k ) - 0 ) <-> 1 <_ ( N ^ k ) ) )
179 175 178 mpbird 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 1 <_ ( ( N ^ k ) - 0 ) )
180 78 77 172 179 lesubd 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> 0 <_ ( ( N ^ k ) - 1 ) )
181 77 lem1d 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( ( N ^ k ) - 1 ) <_ ( N ^ k ) )
182 171 71 79 180 77 181 fprodle 
 |-  ( ph -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) <_ prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^ k ) )
183 80 169 70 170 182 lemul2ad 
 |-  ( ph -> ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) <_ ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^ k ) ) )
184 82 breq1d 
 |-  ( ph -> ( A <_ ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^ k ) ) <-> ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) ) <_ ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^ k ) ) ) )
185 183 184 mpbird 
 |-  ( ph -> A <_ ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^ k ) ) )
186 72 recnd 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> N e. CC )
187 cxpexp 
 |-  ( ( N e. CC /\ k e. NN0 ) -> ( N ^c k ) = ( N ^ k ) )
188 186 76 187 syl2anc 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( N ^c k ) = ( N ^ k ) )
189 188 eqcomd 
 |-  ( ( ph /\ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ) -> ( N ^ k ) = ( N ^c k ) )
190 189 prodeq2dv 
 |-  ( ph -> prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^ k ) = prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) )
191 190 oveq2d 
 |-  ( ph -> ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^ k ) ) = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) )
192 185 191 breqtrd 
 |-  ( ph -> A <_ ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) )
193 5 recnd 
 |-  ( ph -> N e. CC )
194 cxpexp 
 |-  ( ( N e. CC /\ ( |_ ` ( 2 logb B ) ) e. NN0 ) -> ( N ^c ( |_ ` ( 2 logb B ) ) ) = ( N ^ ( |_ ` ( 2 logb B ) ) ) )
195 193 69 194 syl2anc 
 |-  ( ph -> ( N ^c ( |_ ` ( 2 logb B ) ) ) = ( N ^ ( |_ ` ( 2 logb B ) ) ) )
196 195 oveq1d 
 |-  ( ph -> ( ( N ^c ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) )
197 196 eqcomd 
 |-  ( ph -> ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) = ( ( N ^c ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) )
198 192 197 breqtrd 
 |-  ( ph -> A <_ ( ( N ^c ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) )
199 159 167 164 3jca 
 |-  ( ph -> ( ( N ^c ( |_ ` ( 2 logb B ) ) ) e. RR /\ ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) e. RR /\ ( prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) e. RR /\ 0 < prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) ) )
200 1 3 4 aks4d1p1p3 
 |-  ( ph -> ( N ^c ( |_ ` ( 2 logb B ) ) ) < ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) )
201 ltmul1a 
 |-  ( ( ( ( N ^c ( |_ ` ( 2 logb B ) ) ) e. RR /\ ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) e. RR /\ ( prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) e. RR /\ 0 < prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) ) /\ ( N ^c ( |_ ` ( 2 logb B ) ) ) < ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) ) -> ( ( N ^c ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) < ( ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) )
202 199 200 201 syl2anc 
 |-  ( ph -> ( ( N ^c ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) < ( ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) )
203 84 166 168 198 202 lelttrd 
 |-  ( ph -> A < ( ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) )
204 161 oveq2d 
 |-  ( ph -> ( ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( N ^c k ) ) = ( ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) x. ( N ^c sum_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) k ) ) )
205 203 204 breqtrd 
 |-  ( ph -> A < ( ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) x. ( N ^c sum_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) k ) ) )
206 144 oveq2d 
 |-  ( ph -> ( N ^c sum_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) k ) = ( N ^c ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) ) )
207 206 oveq2d 
 |-  ( ph -> ( ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) x. ( N ^c sum_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) k ) ) = ( ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) x. ( N ^c ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) ) ) )
208 205 207 breqtrd 
 |-  ( ph -> A < ( ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) x. ( N ^c ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) ) ) )
209 26 10 gtned 
 |-  ( ph -> N =/= 0 )
210 90 recnd 
 |-  ( ph -> ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) e. CC )
211 141 nncnd 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) ^ 2 ) ) e. CC )
212 211 sqcld 
 |-  ( ph -> ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) e. CC )
213 212 211 addcld 
 |-  ( ph -> ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) e. CC )
214 213 halfcld 
 |-  ( ph -> ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) e. CC )
215 193 209 210 214 cxpaddd 
 |-  ( ph -> ( N ^c ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) ) ) = ( ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) x. ( N ^c ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) ) ) )
216 215 eqcomd 
 |-  ( ph -> ( ( N ^c ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) x. ( N ^c ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) ) ) = ( N ^c ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) ) ) )
217 208 216 breqtrd 
 |-  ( ph -> A < ( N ^c ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) ) ) )
218 reflcl 
 |-  ( ( ( 2 logb N ) ^ 2 ) e. RR -> ( |_ ` ( ( 2 logb N ) ^ 2 ) ) e. RR )
219 91 218 syl 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) ^ 2 ) ) e. RR )
220 219 resqcld 
 |-  ( ph -> ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) e. RR )
221 220 219 readdcld 
 |-  ( ph -> ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) e. RR )
222 34 a1i 
 |-  ( ph -> 2 e. RR+ )
223 91 99 reexpcld 
 |-  ( ph -> ( ( ( 2 logb N ) ^ 2 ) ^ 2 ) e. RR )
224 id 
 |-  ( ph -> ph )
225 142 nn0ge0d 
 |-  ( ph -> 0 <_ ( |_ ` ( ( 2 logb N ) ^ 2 ) ) )
226 flle 
 |-  ( ( ( 2 logb N ) ^ 2 ) e. RR -> ( |_ ` ( ( 2 logb N ) ^ 2 ) ) <_ ( ( 2 logb N ) ^ 2 ) )
227 91 226 syl 
 |-  ( ph -> ( |_ ` ( ( 2 logb N ) ^ 2 ) ) <_ ( ( 2 logb N ) ^ 2 ) )
228 219 91 99 225 227 leexp1ad 
 |-  ( ph -> ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) <_ ( ( ( 2 logb N ) ^ 2 ) ^ 2 ) )
229 224 228 syl 
 |-  ( ph -> ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) <_ ( ( ( 2 logb N ) ^ 2 ) ^ 2 ) )
230 16 recnd 
 |-  ( ph -> ( 2 logb N ) e. CC )
231 230 99 99 expmuld 
 |-  ( ph -> ( ( 2 logb N ) ^ ( 2 x. 2 ) ) = ( ( ( 2 logb N ) ^ 2 ) ^ 2 ) )
232 231 eqcomd 
 |-  ( ph -> ( ( ( 2 logb N ) ^ 2 ) ^ 2 ) = ( ( 2 logb N ) ^ ( 2 x. 2 ) ) )
233 2t2e4 
 |-  ( 2 x. 2 ) = 4
234 233 oveq2i 
 |-  ( ( 2 logb N ) ^ ( 2 x. 2 ) ) = ( ( 2 logb N ) ^ 4 )
235 234 a1i 
 |-  ( ph -> ( ( 2 logb N ) ^ ( 2 x. 2 ) ) = ( ( 2 logb N ) ^ 4 ) )
236 232 235 eqtrd 
 |-  ( ph -> ( ( ( 2 logb N ) ^ 2 ) ^ 2 ) = ( ( 2 logb N ) ^ 4 ) )
237 223 236 eqled 
 |-  ( ph -> ( ( ( 2 logb N ) ^ 2 ) ^ 2 ) <_ ( ( 2 logb N ) ^ 4 ) )
238 220 223 152 229 237 letrd 
 |-  ( ph -> ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) <_ ( ( 2 logb N ) ^ 4 ) )
239 220 219 152 91 238 227 le2addd 
 |-  ( ph -> ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) <_ ( ( ( 2 logb N ) ^ 4 ) + ( ( 2 logb N ) ^ 2 ) ) )
240 221 153 222 239 lediv1dd 
 |-  ( ph -> ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) <_ ( ( ( ( 2 logb N ) ^ 4 ) + ( ( 2 logb N ) ^ 2 ) ) / 2 ) )
241 147 154 90 240 leadd2dd 
 |-  ( ph -> ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) ) <_ ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( 2 logb N ) ^ 4 ) + ( ( 2 logb N ) ^ 2 ) ) / 2 ) ) )
242 5 32 148 155 cxpled 
 |-  ( ph -> ( ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) ) <_ ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( 2 logb N ) ^ 4 ) + ( ( 2 logb N ) ^ 2 ) ) / 2 ) ) <-> ( N ^c ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) ) ) <_ ( N ^c ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( 2 logb N ) ^ 4 ) + ( ( 2 logb N ) ^ 2 ) ) / 2 ) ) ) ) )
243 241 242 mpbid 
 |-  ( ph -> ( N ^c ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ^ 2 ) + ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) / 2 ) ) ) <_ ( N ^c ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( 2 logb N ) ^ 4 ) + ( ( 2 logb N ) ^ 2 ) ) / 2 ) ) ) )
244 84 149 156 217 243 ltletrd 
 |-  ( ph -> A < ( N ^c ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( 2 logb N ) ^ 4 ) + ( ( 2 logb N ) ^ 2 ) ) / 2 ) ) ) )
245 152 recnd 
 |-  ( ph -> ( ( 2 logb N ) ^ 4 ) e. CC )
246 91 recnd 
 |-  ( ph -> ( ( 2 logb N ) ^ 2 ) e. CC )
247 245 246 101 102 divdird 
 |-  ( ph -> ( ( ( ( 2 logb N ) ^ 4 ) + ( ( 2 logb N ) ^ 2 ) ) / 2 ) = ( ( ( ( 2 logb N ) ^ 4 ) / 2 ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) )
248 247 oveq2d 
 |-  ( ph -> ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( 2 logb N ) ^ 4 ) + ( ( 2 logb N ) ^ 2 ) ) / 2 ) ) = ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( 2 logb N ) ^ 4 ) / 2 ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) ) )
249 248 oveq2d 
 |-  ( ph -> ( N ^c ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( 2 logb N ) ^ 4 ) + ( ( 2 logb N ) ^ 2 ) ) / 2 ) ) ) = ( N ^c ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( 2 logb N ) ^ 4 ) / 2 ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) ) ) )
250 244 249 breqtrd 
 |-  ( ph -> A < ( N ^c ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( 2 logb N ) ^ 4 ) / 2 ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) ) ) )
251 245 101 102 divcld 
 |-  ( ph -> ( ( ( 2 logb N ) ^ 4 ) / 2 ) e. CC )
252 246 101 102 divcld 
 |-  ( ph -> ( ( ( 2 logb N ) ^ 2 ) / 2 ) e. CC )
253 251 252 addcomd 
 |-  ( ph -> ( ( ( ( 2 logb N ) ^ 4 ) / 2 ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) = ( ( ( ( 2 logb N ) ^ 2 ) / 2 ) + ( ( ( 2 logb N ) ^ 4 ) / 2 ) ) )
254 253 oveq2d 
 |-  ( ph -> ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( 2 logb N ) ^ 4 ) / 2 ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) ) = ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( 2 logb N ) ^ 2 ) / 2 ) + ( ( ( 2 logb N ) ^ 4 ) / 2 ) ) ) )
255 210 252 251 addassd 
 |-  ( 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 ) + ( ( ( 2 logb N ) ^ 4 ) / 2 ) ) ) )
256 255 eqcomd 
 |-  ( 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 ) ) + ( ( ( 2 logb N ) ^ 4 ) / 2 ) ) )
257 254 256 eqtrd 
 |-  ( ph -> ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( 2 logb N ) ^ 4 ) / 2 ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) ) = ( ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) + ( ( ( 2 logb N ) ^ 4 ) / 2 ) ) )
258 257 oveq2d 
 |-  ( ph -> ( N ^c ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( ( 2 logb N ) ^ 4 ) / 2 ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) ) ) = ( N ^c ( ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) + ( ( ( 2 logb N ) ^ 4 ) / 2 ) ) ) )
259 250 258 breqtrd 
 |-  ( ph -> A < ( N ^c ( ( ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) + ( ( ( 2 logb N ) ^ 2 ) / 2 ) ) + ( ( ( 2 logb N ) ^ 4 ) / 2 ) ) ) )