Metamath Proof Explorer

Theorem aks4d1p1p5

Description: Show inequality for existence of a non-divisor. (Contributed by metakunt, 19-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 aks4d1p1p5.1 
 |-  ( ph -> N e. NN )
2 aks4d1p1p5.2 
 |-  A = ( ( N ^ ( |_ ` ( 2 logb B ) ) ) x. prod_ k e. ( 1 ... ( |_ ` ( ( 2 logb N ) ^ 2 ) ) ) ( ( N ^ k ) - 1 ) )
3 aks4d1p1p5.3 
 |-  B = ( |^ ` ( ( 2 logb N ) ^ 5 ) )
4 aks4d1p1p5.4 
 |-  ( ph -> 4 <_ N )
5 aks4d1p1p5.5 
 |-  C = ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) )
6 aks4d1p1p5.6 
 |-  D = ( ( 2 logb N ) ^ 2 )
7 aks4d1p1p5.7 
 |-  E = ( ( 2 logb N ) ^ 4 )
8 3re 
 |-  3 e. RR
9 8 a1i 
 |-  ( ph -> 3 e. RR )
10 4re 
 |-  4 e. RR
11 10 a1i 
 |-  ( ph -> 4 e. RR )
12 1 nnred 
 |-  ( ph -> N e. RR )
13 9 lep1d 
 |-  ( ph -> 3 <_ ( 3 + 1 ) )
14 3p1e4 
 |-  ( 3 + 1 ) = 4
15 13 14 breqtrdi 
 |-  ( ph -> 3 <_ 4 )
16 9 11 12 15 4 letrd 
 |-  ( ph -> 3 <_ N )
17 2re 
 |-  2 e. RR
18 17 a1i 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 2 e. RR )
19 2pos 
 |-  0 < 2
20 19 a1i 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 0 < 2 )
21 elicc2 
 |-  ( ( 4 e. RR /\ N e. RR ) -> ( x e. ( 4 [,] N ) <-> ( x e. RR /\ 4 <_ x /\ x <_ N ) ) )
22 11 12 21 syl2anc 
 |-  ( ph -> ( x e. ( 4 [,] N ) <-> ( x e. RR /\ 4 <_ x /\ x <_ N ) ) )
23 22 biimpd 
 |-  ( ph -> ( x e. ( 4 [,] N ) -> ( x e. RR /\ 4 <_ x /\ x <_ N ) ) )
24 23 imp 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( x e. RR /\ 4 <_ x /\ x <_ N ) )
25 24 simp1d 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> x e. RR )
26 0red 
 |-  ( ph -> 0 e. RR )
27 26 adantr 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 0 e. RR )
28 10 a1i 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 4 e. RR )
29 4pos 
 |-  0 < 4
30 29 a1i 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 0 < 4 )
31 24 simp2d 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 4 <_ x )
32 27 28 25 30 31 ltletrd 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 0 < x )
33 1red 
 |-  ( ph -> 1 e. RR )
34 1lt2 
 |-  1 < 2
35 34 a1i 
 |-  ( ph -> 1 < 2 )
36 33 35 ltned 
 |-  ( ph -> 1 =/= 2 )
37 36 necomd 
 |-  ( ph -> 2 =/= 1 )
38 37 adantr 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 2 =/= 1 )
39 18 20 25 32 38 relogbcld 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( 2 logb x ) e. RR )
40 5nn0 
 |-  5 e. NN0
41 40 a1i 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 5 e. NN0 )
42 39 41 reexpcld 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( ( 2 logb x ) ^ 5 ) e. RR )
43 1red 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 1 e. RR )
44 42 43 readdcld 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( ( ( 2 logb x ) ^ 5 ) + 1 ) e. RR )
45 27 43 readdcld 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( 0 + 1 ) e. RR )
46 27 ltp1d 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 0 < ( 0 + 1 ) )
47 41 nn0zd 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 5 e. ZZ )
48 ax-resscn 
 |-  RR C_ CC
49 48 18 sselid 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 2 e. CC )
50 27 20 gtned 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 2 =/= 0 )
51 logb1 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ 2 =/= 1 ) -> ( 2 logb 1 ) = 0 )
52 49 50 38 51 syl3anc 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( 2 logb 1 ) = 0 )
53 1lt4 
 |-  1 < 4
54 53 a1i 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 1 < 4 )
55 43 28 25 54 31 ltletrd 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 1 < x )
56 2z 
 |-  2 e. ZZ
57 56 a1i 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 2 e. ZZ )
58 57 uzidd 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 2 e. ( ZZ>= ` 2 ) )
59 1rp 
 |-  1 e. RR+
60 59 a1i 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 1 e. RR+ )
61 25 32 elrpd 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> x e. RR+ )
62 logblt 
 |-  ( ( 2 e. ( ZZ>= ` 2 ) /\ 1 e. RR+ /\ x e. RR+ ) -> ( 1 < x <-> ( 2 logb 1 ) < ( 2 logb x ) ) )
63 58 60 61 62 syl3anc 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( 1 < x <-> ( 2 logb 1 ) < ( 2 logb x ) ) )
64 55 63 mpbid 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( 2 logb 1 ) < ( 2 logb x ) )
65 52 64 eqbrtrrd 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 0 < ( 2 logb x ) )
66 expgt0 
 |-  ( ( ( 2 logb x ) e. RR /\ 5 e. ZZ /\ 0 < ( 2 logb x ) ) -> 0 < ( ( 2 logb x ) ^ 5 ) )
67 39 47 65 66 syl3anc 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 0 < ( ( 2 logb x ) ^ 5 ) )
68 27 42 43 67 ltadd1dd 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( 0 + 1 ) < ( ( ( 2 logb x ) ^ 5 ) + 1 ) )
69 27 45 44 46 68 lttrd 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 0 < ( ( ( 2 logb x ) ^ 5 ) + 1 ) )
70 18 20 44 69 38 relogbcld 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) e. RR )
71 18 70 remulcld 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) e. RR )
72 0red 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 0 e. RR )
73 simpr 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> x e. ( 4 [,] N ) )
74 11 12 jca 
 |-  ( ph -> ( 4 e. RR /\ N e. RR ) )
75 74 adantr 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( 4 e. RR /\ N e. RR ) )
76 75 21 syl 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( x e. ( 4 [,] N ) <-> ( x e. RR /\ 4 <_ x /\ x <_ N ) ) )
77 73 76 mpbid 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( x e. RR /\ 4 <_ x /\ x <_ N ) )
78 77 simp2d 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 4 <_ x )
79 72 28 25 30 78 ltletrd 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 0 < x )
80 18 20 25 79 38 relogbcld 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( 2 logb x ) e. RR )
81 80 resqcld 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( ( 2 logb x ) ^ 2 ) e. RR )
82 71 81 readdcld 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) e. RR )
83 82 fmpttd 
 |-  ( ph -> ( x e. ( 4 [,] N ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) : ( 4 [,] N ) --> RR )
84 48 a1i 
 |-  ( ph -> RR C_ CC )
85 3lt4 
 |-  3 < 4
86 85 a1i 
 |-  ( ph -> 3 < 4 )
87 12 33 readdcld 
 |-  ( ph -> ( N + 1 ) e. RR )
88 12 ltp1d 
 |-  ( ph -> N < ( N + 1 ) )
89 11 12 87 4 88 lelttrd 
 |-  ( ph -> 4 < ( N + 1 ) )
90 86 89 jca 
 |-  ( ph -> ( 3 < 4 /\ 4 < ( N + 1 ) ) )
91 9 rexrd 
 |-  ( ph -> 3 e. RR* )
92 87 rexrd 
 |-  ( ph -> ( N + 1 ) e. RR* )
93 11 rexrd 
 |-  ( ph -> 4 e. RR* )
94 elioo5 
 |-  ( ( 3 e. RR* /\ ( N + 1 ) e. RR* /\ 4 e. RR* ) -> ( 4 e. ( 3 (,) ( N + 1 ) ) <-> ( 3 < 4 /\ 4 < ( N + 1 ) ) ) )
95 91 92 93 94 syl3anc 
 |-  ( ph -> ( 4 e. ( 3 (,) ( N + 1 ) ) <-> ( 3 < 4 /\ 4 < ( N + 1 ) ) ) )
96 90 95 mpbird 
 |-  ( ph -> 4 e. ( 3 (,) ( N + 1 ) ) )
97 9 11 12 86 4 ltletrd 
 |-  ( ph -> 3 < N )
98 97 88 jca 
 |-  ( ph -> ( 3 < N /\ N < ( N + 1 ) ) )
99 12 rexrd 
 |-  ( ph -> N e. RR* )
100 elioo5 
 |-  ( ( 3 e. RR* /\ ( N + 1 ) e. RR* /\ N e. RR* ) -> ( N e. ( 3 (,) ( N + 1 ) ) <-> ( 3 < N /\ N < ( N + 1 ) ) ) )
101 91 92 99 100 syl3anc 
 |-  ( ph -> ( N e. ( 3 (,) ( N + 1 ) ) <-> ( 3 < N /\ N < ( N + 1 ) ) ) )
102 98 101 mpbird 
 |-  ( ph -> N e. ( 3 (,) ( N + 1 ) ) )
103 iccssioo2 
 |-  ( ( 4 e. ( 3 (,) ( N + 1 ) ) /\ N e. ( 3 (,) ( N + 1 ) ) ) -> ( 4 [,] N ) C_ ( 3 (,) ( N + 1 ) ) )
104 96 102 103 syl2anc 
 |-  ( ph -> ( 4 [,] N ) C_ ( 3 (,) ( N + 1 ) ) )
105 104 resmptd 
 |-  ( ph -> ( ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) |` ( 4 [,] N ) ) = ( x e. ( 4 [,] N ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) )
106 2cnd 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 2 e. CC )
107 17 a1i 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 2 e. RR )
108 19 a1i 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 0 < 2 )
109 elioore 
 |-  ( x e. ( 3 (,) ( N + 1 ) ) -> x e. RR )
110 109 adantl 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> x e. RR )
111 0red 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 0 e. RR )
112 8 a1i 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 3 e. RR )
113 3pos 
 |-  0 < 3
114 113 a1i 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 0 < 3 )
115 eliooord 
 |-  ( x e. ( 3 (,) ( N + 1 ) ) -> ( 3 < x /\ x < ( N + 1 ) ) )
116 simpl 
 |-  ( ( 3 < x /\ x < ( N + 1 ) ) -> 3 < x )
117 115 116 syl 
 |-  ( x e. ( 3 (,) ( N + 1 ) ) -> 3 < x )
118 117 adantl 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 3 < x )
119 111 112 110 114 118 lttrd 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 0 < x )
120 37 adantr 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 2 =/= 1 )
121 107 108 110 119 120 relogbcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( 2 logb x ) e. RR )
122 40 a1i 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 5 e. NN0 )
123 121 122 reexpcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( 2 logb x ) ^ 5 ) e. RR )
124 1red 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 1 e. RR )
125 123 124 readdcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( ( 2 logb x ) ^ 5 ) + 1 ) e. RR )
126 111 124 readdcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( 0 + 1 ) e. RR )
127 111 ltp1d 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 0 < ( 0 + 1 ) )
128 122 nn0zd 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 5 e. ZZ )
129 34 a1i 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 1 < 2 )
130 2lt3 
 |-  2 < 3
131 130 a1i 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 2 < 3 )
132 124 107 112 129 131 lttrd 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 1 < 3 )
133 124 112 110 132 118 lttrd 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 1 < x )
134 110 119 elrpd 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> x e. RR+ )
135 2rp 
 |-  2 e. RR+
136 135 a1i 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 2 e. RR+ )
137 134 136 129 jca32 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( x e. RR+ /\ ( 2 e. RR+ /\ 1 < 2 ) ) )
138 logbgt0b 
 |-  ( ( x e. RR+ /\ ( 2 e. RR+ /\ 1 < 2 ) ) -> ( 0 < ( 2 logb x ) <-> 1 < x ) )
139 137 138 syl 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( 0 < ( 2 logb x ) <-> 1 < x ) )
140 133 139 mpbird 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 0 < ( 2 logb x ) )
141 121 128 140 66 syl3anc 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 0 < ( ( 2 logb x ) ^ 5 ) )
142 111 123 124 141 ltadd1dd 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( 0 + 1 ) < ( ( ( 2 logb x ) ^ 5 ) + 1 ) )
143 111 126 125 127 142 lttrd 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 0 < ( ( ( 2 logb x ) ^ 5 ) + 1 ) )
144 124 129 ltned 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 1 =/= 2 )
145 144 necomd 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 2 =/= 1 )
146 107 108 125 143 145 relogbcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) e. RR )
147 146 recnd 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) e. CC )
148 106 147 mulcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) e. CC )
149 48 121 sselid 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( 2 logb x ) e. CC )
150 149 sqcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( 2 logb x ) ^ 2 ) e. CC )
151 148 150 addcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) e. CC )
152 151 fmpttd 
 |-  ( ph -> ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) : ( 3 (,) ( N + 1 ) ) --> CC )
153 ioossre 
 |-  ( 3 (,) ( N + 1 ) ) C_ RR
154 153 a1i 
 |-  ( ph -> ( 3 (,) ( N + 1 ) ) C_ RR )
155 84 152 154 3jca 
 |-  ( ph -> ( RR C_ CC /\ ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) : ( 3 (,) ( N + 1 ) ) --> CC /\ ( 3 (,) ( N + 1 ) ) C_ RR ) )
156 136 relogcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( log ` 2 ) e. RR )
157 125 156 remulcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) e. RR )
158 48 123 sselid 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( 2 logb x ) ^ 5 ) e. CC )
159 1cnd 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 1 e. CC )
160 158 159 addcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( ( 2 logb x ) ^ 5 ) + 1 ) e. CC )
161 111 108 gtned 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 2 =/= 0 )
162 106 161 logcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( log ` 2 ) e. CC )
163 111 143 gtned 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( ( 2 logb x ) ^ 5 ) + 1 ) =/= 0 )
164 loggt0b 
 |-  ( 2 e. RR+ -> ( 0 < ( log ` 2 ) <-> 1 < 2 ) )
165 135 164 ax-mp 
 |-  ( 0 < ( log ` 2 ) <-> 1 < 2 )
166 35 165 sylibr 
 |-  ( ph -> 0 < ( log ` 2 ) )
167 26 166 ltned 
 |-  ( ph -> 0 =/= ( log ` 2 ) )
168 167 necomd 
 |-  ( ph -> ( log ` 2 ) =/= 0 )
169 168 adantr 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( log ` 2 ) =/= 0 )
170 160 162 163 169 mulne0d 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) =/= 0 )
171 124 157 170 redivcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) e. RR )
172 5re 
 |-  5 e. RR
173 172 a1i 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 5 e. RR )
174 4nn0 
 |-  4 e. NN0
175 174 a1i 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 4 e. NN0 )
176 121 175 reexpcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( 2 logb x ) ^ 4 ) e. RR )
177 173 176 remulcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( 5 x. ( ( 2 logb x ) ^ 4 ) ) e. RR )
178 110 156 remulcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( x x. ( log ` 2 ) ) e. RR )
179 48 110 sselid 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> x e. CC )
180 111 119 gtned 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> x =/= 0 )
181 179 162 180 169 mulne0d 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( x x. ( log ` 2 ) ) =/= 0 )
182 124 178 181 redivcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( 1 / ( x x. ( log ` 2 ) ) ) e. RR )
183 177 182 remulcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) e. RR )
184 183 111 readdcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) e. RR )
185 171 184 remulcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) e. RR )
186 107 185 remulcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( 2 x. ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) ) e. RR )
187 156 resqcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( log ` 2 ) ^ 2 ) e. RR )
188 56 a1i 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 2 e. ZZ )
189 162 169 188 expne0d 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( log ` 2 ) ^ 2 ) =/= 0 )
190 107 187 189 redivcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( 2 / ( ( log ` 2 ) ^ 2 ) ) e. RR )
191 134 relogcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( log ` x ) e. RR )
192 2m1e1 
 |-  ( 2 - 1 ) = 1
193 1nn0 
 |-  1 e. NN0
194 192 193 eqeltri 
 |-  ( 2 - 1 ) e. NN0
195 194 a1i 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( 2 - 1 ) e. NN0 )
196 191 195 reexpcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( log ` x ) ^ ( 2 - 1 ) ) e. RR )
197 196 110 180 redivcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) e. RR )
198 190 197 remulcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) ) e. RR )
199 186 198 readdcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( 2 x. ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) ) ) e. RR )
200 199 ralrimiva 
 |-  ( ph -> A. x e. ( 3 (,) ( N + 1 ) ) ( ( 2 x. ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) ) ) e. RR )
201 nfcv 
 |-  F/_ x ( 3 (,) ( N + 1 ) )
202 201 fnmptf 
 |-  ( A. x e. ( 3 (,) ( N + 1 ) ) ( ( 2 x. ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) ) ) e. RR -> ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) ) ) ) Fn ( 3 (,) ( N + 1 ) ) )
203 200 202 syl 
 |-  ( ph -> ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) ) ) ) Fn ( 3 (,) ( N + 1 ) ) )
204 9 leidd 
 |-  ( ph -> 3 <_ 3 )
205 12 lep1d 
 |-  ( ph -> N <_ ( N + 1 ) )
206 9 12 87 16 205 letrd 
 |-  ( ph -> 3 <_ ( N + 1 ) )
207 9 87 204 206 aks4d1p1p6 
 |-  ( ph -> ( RR _D ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) ) = ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) ) ) ) )
208 207 fneq1d 
 |-  ( ph -> ( ( RR _D ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) ) Fn ( 3 (,) ( N + 1 ) ) <-> ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) ) ) ) Fn ( 3 (,) ( N + 1 ) ) ) )
209 203 208 mpbird 
 |-  ( ph -> ( RR _D ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) ) Fn ( 3 (,) ( N + 1 ) ) )
210 209 fndmd 
 |-  ( ph -> dom ( RR _D ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) ) = ( 3 (,) ( N + 1 ) ) )
211 dvcn 
 |-  ( ( ( RR C_ CC /\ ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) : ( 3 (,) ( N + 1 ) ) --> CC /\ ( 3 (,) ( N + 1 ) ) C_ RR ) /\ dom ( RR _D ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) ) = ( 3 (,) ( N + 1 ) ) ) -> ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) e. ( ( 3 (,) ( N + 1 ) ) -cn-> CC ) )
212 155 210 211 syl2anc 
 |-  ( ph -> ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) e. ( ( 3 (,) ( N + 1 ) ) -cn-> CC ) )
213 rescncf 
 |-  ( ( 4 [,] N ) C_ ( 3 (,) ( N + 1 ) ) -> ( ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) e. ( ( 3 (,) ( N + 1 ) ) -cn-> CC ) -> ( ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) |` ( 4 [,] N ) ) e. ( ( 4 [,] N ) -cn-> CC ) ) )
214 104 213 syl 
 |-  ( ph -> ( ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) e. ( ( 3 (,) ( N + 1 ) ) -cn-> CC ) -> ( ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) |` ( 4 [,] N ) ) e. ( ( 4 [,] N ) -cn-> CC ) ) )
215 212 214 mpd 
 |-  ( ph -> ( ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) |` ( 4 [,] N ) ) e. ( ( 4 [,] N ) -cn-> CC ) )
216 105 215 eqeltrrd 
 |-  ( ph -> ( x e. ( 4 [,] N ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) e. ( ( 4 [,] N ) -cn-> CC ) )
217 cncffvrn 
 |-  ( ( RR C_ CC /\ ( x e. ( 4 [,] N ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) e. ( ( 4 [,] N ) -cn-> CC ) ) -> ( ( x e. ( 4 [,] N ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) e. ( ( 4 [,] N ) -cn-> RR ) <-> ( x e. ( 4 [,] N ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) : ( 4 [,] N ) --> RR ) )
218 84 216 217 syl2anc 
 |-  ( ph -> ( ( x e. ( 4 [,] N ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) e. ( ( 4 [,] N ) -cn-> RR ) <-> ( x e. ( 4 [,] N ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) : ( 4 [,] N ) --> RR ) )
219 83 218 mpbird 
 |-  ( ph -> ( x e. ( 4 [,] N ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) e. ( ( 4 [,] N ) -cn-> RR ) )
220 174 a1i 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> 4 e. NN0 )
221 39 220 reexpcld 
 |-  ( ( ph /\ x e. ( 4 [,] N ) ) -> ( ( 2 logb x ) ^ 4 ) e. RR )
222 221 fmpttd 
 |-  ( ph -> ( x e. ( 4 [,] N ) |-> ( ( 2 logb x ) ^ 4 ) ) : ( 4 [,] N ) --> RR )
223 104 resmptd 
 |-  ( ph -> ( ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) |` ( 4 [,] N ) ) = ( x e. ( 4 [,] N ) |-> ( ( 2 logb x ) ^ 4 ) ) )
224 48 176 sselid 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( 2 logb x ) ^ 4 ) e. CC )
225 224 fmpttd 
 |-  ( ph -> ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) : ( 3 (,) ( N + 1 ) ) --> CC )
226 84 225 154 3jca 
 |-  ( ph -> ( RR C_ CC /\ ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) : ( 3 (,) ( N + 1 ) ) --> CC /\ ( 3 (,) ( N + 1 ) ) C_ RR ) )
227 10 a1i 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 4 e. RR )
228 156 175 reexpcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( log ` 2 ) ^ 4 ) e. RR )
229 4z 
 |-  4 e. ZZ
230 229 a1i 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> 4 e. ZZ )
231 162 169 230 expne0d 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( log ` 2 ) ^ 4 ) =/= 0 )
232 227 228 231 redivcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( 4 / ( ( log ` 2 ) ^ 4 ) ) e. RR )
233 4m1e3 
 |-  ( 4 - 1 ) = 3
234 3nn0 
 |-  3 e. NN0
235 233 234 eqeltri 
 |-  ( 4 - 1 ) e. NN0
236 235 a1i 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( 4 - 1 ) e. NN0 )
237 191 236 reexpcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( log ` x ) ^ ( 4 - 1 ) ) e. RR )
238 237 110 180 redivcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( ( log ` x ) ^ ( 4 - 1 ) ) / x ) e. RR )
239 232 238 remulcld 
 |-  ( ( ph /\ x e. ( 3 (,) ( N + 1 ) ) ) -> ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ ( 4 - 1 ) ) / x ) ) e. RR )
240 239 ralrimiva 
 |-  ( ph -> A. x e. ( 3 (,) ( N + 1 ) ) ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ ( 4 - 1 ) ) / x ) ) e. RR )
241 201 fnmptf 
 |-  ( A. x e. ( 3 (,) ( N + 1 ) ) ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ ( 4 - 1 ) ) / x ) ) e. RR -> ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ ( 4 - 1 ) ) / x ) ) ) Fn ( 3 (,) ( N + 1 ) ) )
242 240 241 syl 
 |-  ( ph -> ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ ( 4 - 1 ) ) / x ) ) ) Fn ( 3 (,) ( N + 1 ) ) )
243 113 a1i 
 |-  ( ph -> 0 < 3 )
244 eqid 
 |-  ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) = ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) )
245 eqid 
 |-  ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ ( 4 - 1 ) ) / x ) ) ) = ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ ( 4 - 1 ) ) / x ) ) )
246 eqid 
 |-  ( 4 / ( ( log ` 2 ) ^ 4 ) ) = ( 4 / ( ( log ` 2 ) ^ 4 ) )
247 4nn 
 |-  4 e. NN
248 247 a1i 
 |-  ( ph -> 4 e. NN )
249 9 87 243 206 244 245 246 248 dvrelogpow2b 
 |-  ( ph -> ( RR _D ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) ) = ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ ( 4 - 1 ) ) / x ) ) ) )
250 249 fneq1d 
 |-  ( ph -> ( ( RR _D ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) ) Fn ( 3 (,) ( N + 1 ) ) <-> ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ ( 4 - 1 ) ) / x ) ) ) Fn ( 3 (,) ( N + 1 ) ) ) )
251 242 250 mpbird 
 |-  ( ph -> ( RR _D ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) ) Fn ( 3 (,) ( N + 1 ) ) )
252 251 fndmd 
 |-  ( ph -> dom ( RR _D ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) ) = ( 3 (,) ( N + 1 ) ) )
253 dvcn 
 |-  ( ( ( RR C_ CC /\ ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) : ( 3 (,) ( N + 1 ) ) --> CC /\ ( 3 (,) ( N + 1 ) ) C_ RR ) /\ dom ( RR _D ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) ) = ( 3 (,) ( N + 1 ) ) ) -> ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) e. ( ( 3 (,) ( N + 1 ) ) -cn-> CC ) )
254 226 252 253 syl2anc 
 |-  ( ph -> ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) e. ( ( 3 (,) ( N + 1 ) ) -cn-> CC ) )
255 rescncf 
 |-  ( ( 4 [,] N ) C_ ( 3 (,) ( N + 1 ) ) -> ( ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) e. ( ( 3 (,) ( N + 1 ) ) -cn-> CC ) -> ( ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) |` ( 4 [,] N ) ) e. ( ( 4 [,] N ) -cn-> CC ) ) )
256 104 255 syl 
 |-  ( ph -> ( ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) e. ( ( 3 (,) ( N + 1 ) ) -cn-> CC ) -> ( ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) |` ( 4 [,] N ) ) e. ( ( 4 [,] N ) -cn-> CC ) ) )
257 254 256 mpd 
 |-  ( ph -> ( ( x e. ( 3 (,) ( N + 1 ) ) |-> ( ( 2 logb x ) ^ 4 ) ) |` ( 4 [,] N ) ) e. ( ( 4 [,] N ) -cn-> CC ) )
258 223 257 eqeltrrd 
 |-  ( ph -> ( x e. ( 4 [,] N ) |-> ( ( 2 logb x ) ^ 4 ) ) e. ( ( 4 [,] N ) -cn-> CC ) )
259 cncffvrn 
 |-  ( ( RR C_ CC /\ ( x e. ( 4 [,] N ) |-> ( ( 2 logb x ) ^ 4 ) ) e. ( ( 4 [,] N ) -cn-> CC ) ) -> ( ( x e. ( 4 [,] N ) |-> ( ( 2 logb x ) ^ 4 ) ) e. ( ( 4 [,] N ) -cn-> RR ) <-> ( x e. ( 4 [,] N ) |-> ( ( 2 logb x ) ^ 4 ) ) : ( 4 [,] N ) --> RR ) )
260 84 258 259 syl2anc 
 |-  ( ph -> ( ( x e. ( 4 [,] N ) |-> ( ( 2 logb x ) ^ 4 ) ) e. ( ( 4 [,] N ) -cn-> RR ) <-> ( x e. ( 4 [,] N ) |-> ( ( 2 logb x ) ^ 4 ) ) : ( 4 [,] N ) --> RR ) )
261 222 260 mpbird 
 |-  ( ph -> ( x e. ( 4 [,] N ) |-> ( ( 2 logb x ) ^ 4 ) ) e. ( ( 4 [,] N ) -cn-> RR ) )
262 11 12 15 4 aks4d1p1p6 
 |-  ( ph -> ( RR _D ( x e. ( 4 (,) N ) |-> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) ) ) = ( x e. ( 4 (,) N ) |-> ( ( 2 x. ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) ) ) ) )
263 29 a1i 
 |-  ( ph -> 0 < 4 )
264 eqid 
 |-  ( x e. ( 4 (,) N ) |-> ( ( 2 logb x ) ^ 4 ) ) = ( x e. ( 4 (,) N ) |-> ( ( 2 logb x ) ^ 4 ) )
265 eqid 
 |-  ( x e. ( 4 (,) N ) |-> ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ ( 4 - 1 ) ) / x ) ) ) = ( x e. ( 4 (,) N ) |-> ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ ( 4 - 1 ) ) / x ) ) )
266 11 12 263 4 264 265 246 248 dvrelogpow2b 
 |-  ( ph -> ( RR _D ( x e. ( 4 (,) N ) |-> ( ( 2 logb x ) ^ 4 ) ) ) = ( x e. ( 4 (,) N ) |-> ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ ( 4 - 1 ) ) / x ) ) ) )
267 233 a1i 
 |-  ( ( ph /\ x e. ( 4 (,) N ) ) -> ( 4 - 1 ) = 3 )
268 267 oveq2d 
 |-  ( ( ph /\ x e. ( 4 (,) N ) ) -> ( ( log ` x ) ^ ( 4 - 1 ) ) = ( ( log ` x ) ^ 3 ) )
269 268 oveq1d 
 |-  ( ( ph /\ x e. ( 4 (,) N ) ) -> ( ( ( log ` x ) ^ ( 4 - 1 ) ) / x ) = ( ( ( log ` x ) ^ 3 ) / x ) )
270 269 oveq2d 
 |-  ( ( ph /\ x e. ( 4 (,) N ) ) -> ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ ( 4 - 1 ) ) / x ) ) = ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ 3 ) / x ) ) )
271 270 mpteq2dva 
 |-  ( ph -> ( x e. ( 4 (,) N ) |-> ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ ( 4 - 1 ) ) / x ) ) ) = ( x e. ( 4 (,) N ) |-> ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ 3 ) / x ) ) ) )
272 266 271 eqtrd 
 |-  ( ph -> ( RR _D ( x e. ( 4 (,) N ) |-> ( ( 2 logb x ) ^ 4 ) ) ) = ( x e. ( 4 (,) N ) |-> ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ 3 ) / x ) ) ) )
273 elioore 
 |-  ( x e. ( 4 (,) N ) -> x e. RR )
274 273 adantl 
 |-  ( ( ph /\ x e. ( 4 (,) N ) ) -> x e. RR )
275 10 a1i 
 |-  ( ( ph /\ x e. ( 4 (,) N ) ) -> 4 e. RR )
276 eliooord 
 |-  ( x e. ( 4 (,) N ) -> ( 4 < x /\ x < N ) )
277 276 simpld 
 |-  ( x e. ( 4 (,) N ) -> 4 < x )
278 277 adantl 
 |-  ( ( ph /\ x e. ( 4 (,) N ) ) -> 4 < x )
279 275 274 278 ltled 
 |-  ( ( ph /\ x e. ( 4 (,) N ) ) -> 4 <_ x )
280 274 279 aks4d1p1p7 
 |-  ( ( ph /\ x e. ( 4 (,) N ) ) -> ( ( 2 x. ( ( 1 / ( ( ( ( 2 logb x ) ^ 5 ) + 1 ) x. ( log ` 2 ) ) ) x. ( ( ( 5 x. ( ( 2 logb x ) ^ 4 ) ) x. ( 1 / ( x x. ( log ` 2 ) ) ) ) + 0 ) ) ) + ( ( 2 / ( ( log ` 2 ) ^ 2 ) ) x. ( ( ( log ` x ) ^ ( 2 - 1 ) ) / x ) ) ) <_ ( ( 4 / ( ( log ` 2 ) ^ 4 ) ) x. ( ( ( log ` x ) ^ 3 ) / x ) ) )
281 oveq2 
 |-  ( x = 4 -> ( 2 logb x ) = ( 2 logb 4 ) )
282 281 oveq1d 
 |-  ( x = 4 -> ( ( 2 logb x ) ^ 5 ) = ( ( 2 logb 4 ) ^ 5 ) )
283 282 oveq1d 
 |-  ( x = 4 -> ( ( ( 2 logb x ) ^ 5 ) + 1 ) = ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) )
284 283 oveq2d 
 |-  ( x = 4 -> ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) = ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) )
285 284 oveq2d 
 |-  ( x = 4 -> ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) = ( 2 x. ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) ) )
286 281 oveq1d 
 |-  ( x = 4 -> ( ( 2 logb x ) ^ 2 ) = ( ( 2 logb 4 ) ^ 2 ) )
287 285 286 oveq12d 
 |-  ( x = 4 -> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) = ( ( 2 x. ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb 4 ) ^ 2 ) ) )
288 281 oveq1d 
 |-  ( x = 4 -> ( ( 2 logb x ) ^ 4 ) = ( ( 2 logb 4 ) ^ 4 ) )
289 oveq2 
 |-  ( x = N -> ( 2 logb x ) = ( 2 logb N ) )
290 289 oveq1d 
 |-  ( x = N -> ( ( 2 logb x ) ^ 5 ) = ( ( 2 logb N ) ^ 5 ) )
291 290 oveq1d 
 |-  ( x = N -> ( ( ( 2 logb x ) ^ 5 ) + 1 ) = ( ( ( 2 logb N ) ^ 5 ) + 1 ) )
292 291 oveq2d 
 |-  ( x = N -> ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) = ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) )
293 292 oveq2d 
 |-  ( x = N -> ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) = ( 2 x. ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) )
294 5 a1i 
 |-  ( x = N -> C = ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) )
295 294 oveq2d 
 |-  ( x = N -> ( 2 x. C ) = ( 2 x. ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) )
296 295 eqcomd 
 |-  ( x = N -> ( 2 x. ( 2 logb ( ( ( 2 logb N ) ^ 5 ) + 1 ) ) ) = ( 2 x. C ) )
297 293 296 eqtrd 
 |-  ( x = N -> ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) = ( 2 x. C ) )
298 289 oveq1d 
 |-  ( x = N -> ( ( 2 logb x ) ^ 2 ) = ( ( 2 logb N ) ^ 2 ) )
299 6 a1i 
 |-  ( x = N -> D = ( ( 2 logb N ) ^ 2 ) )
300 299 eqcomd 
 |-  ( x = N -> ( ( 2 logb N ) ^ 2 ) = D )
301 298 300 eqtrd 
 |-  ( x = N -> ( ( 2 logb x ) ^ 2 ) = D )
302 297 301 oveq12d 
 |-  ( x = N -> ( ( 2 x. ( 2 logb ( ( ( 2 logb x ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb x ) ^ 2 ) ) = ( ( 2 x. C ) + D ) )
303 289 oveq1d 
 |-  ( x = N -> ( ( 2 logb x ) ^ 4 ) = ( ( 2 logb N ) ^ 4 ) )
304 7 a1i 
 |-  ( x = N -> E = ( ( 2 logb N ) ^ 4 ) )
305 304 eqcomd 
 |-  ( x = N -> ( ( 2 logb N ) ^ 4 ) = E )
306 303 305 eqtrd 
 |-  ( x = N -> ( ( 2 logb x ) ^ 4 ) = E )
307 sq2 
 |-  ( 2 ^ 2 ) = 4
308 307 oveq2i 
 |-  ( 2 logb ( 2 ^ 2 ) ) = ( 2 logb 4 )
309 308 a1i 
 |-  ( ph -> ( 2 logb ( 2 ^ 2 ) ) = ( 2 logb 4 ) )
310 309 eqcomd 
 |-  ( ph -> ( 2 logb 4 ) = ( 2 logb ( 2 ^ 2 ) ) )
311 135 a1i 
 |-  ( ph -> 2 e. RR+ )
312 56 a1i 
 |-  ( ph -> 2 e. ZZ )
313 relogbexp 
 |-  ( ( 2 e. RR+ /\ 2 =/= 1 /\ 2 e. ZZ ) -> ( 2 logb ( 2 ^ 2 ) ) = 2 )
314 311 37 312 313 syl3anc 
 |-  ( ph -> ( 2 logb ( 2 ^ 2 ) ) = 2 )
315 310 314 eqtrd 
 |-  ( ph -> ( 2 logb 4 ) = 2 )
316 315 oveq1d 
 |-  ( ph -> ( ( 2 logb 4 ) ^ 5 ) = ( 2 ^ 5 ) )
317 316 oveq1d 
 |-  ( ph -> ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) = ( ( 2 ^ 5 ) + 1 ) )
318 317 oveq2d 
 |-  ( ph -> ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) = ( 2 logb ( ( 2 ^ 5 ) + 1 ) ) )
319 17 a1i 
 |-  ( ph -> 2 e. RR )
320 319 leidd 
 |-  ( ph -> 2 <_ 2 )
321 315 319 eqeltrd 
 |-  ( ph -> ( 2 logb 4 ) e. RR )
322 40 a1i 
 |-  ( ph -> 5 e. NN0 )
323 321 322 reexpcld 
 |-  ( ph -> ( ( 2 logb 4 ) ^ 5 ) e. RR )
324 316 323 eqeltrrd 
 |-  ( ph -> ( 2 ^ 5 ) e. RR )
325 324 33 readdcld 
 |-  ( ph -> ( ( 2 ^ 5 ) + 1 ) e. RR )
326 322 nn0zd 
 |-  ( ph -> 5 e. ZZ )
327 19 a1i 
 |-  ( ph -> 0 < 2 )
328 327 315 breqtrrd 
 |-  ( ph -> 0 < ( 2 logb 4 ) )
329 321 326 328 3jca 
 |-  ( ph -> ( ( 2 logb 4 ) e. RR /\ 5 e. ZZ /\ 0 < ( 2 logb 4 ) ) )
330 expgt0 
 |-  ( ( ( 2 logb 4 ) e. RR /\ 5 e. ZZ /\ 0 < ( 2 logb 4 ) ) -> 0 < ( ( 2 logb 4 ) ^ 5 ) )
331 329 330 syl 
 |-  ( ph -> 0 < ( ( 2 logb 4 ) ^ 5 ) )
332 331 316 breqtrd 
 |-  ( ph -> 0 < ( 2 ^ 5 ) )
333 324 ltp1d 
 |-  ( ph -> ( 2 ^ 5 ) < ( ( 2 ^ 5 ) + 1 ) )
334 26 324 325 332 333 lttrd 
 |-  ( ph -> 0 < ( ( 2 ^ 5 ) + 1 ) )
335 6nn0 
 |-  6 e. NN0
336 335 a1i 
 |-  ( ph -> 6 e. NN0 )
337 319 336 reexpcld 
 |-  ( ph -> ( 2 ^ 6 ) e. RR )
338 336 nn0zd 
 |-  ( ph -> 6 e. ZZ )
339 expgt0 
 |-  ( ( 2 e. RR /\ 6 e. ZZ /\ 0 < 2 ) -> 0 < ( 2 ^ 6 ) )
340 319 338 327 339 syl3anc 
 |-  ( ph -> 0 < ( 2 ^ 6 ) )
341 324 324 readdcld 
 |-  ( ph -> ( ( 2 ^ 5 ) + ( 2 ^ 5 ) ) e. RR )
342 33 319 35 ltled 
 |-  ( ph -> 1 <_ 2 )
343 319 322 342 expge1d 
 |-  ( ph -> 1 <_ ( 2 ^ 5 ) )
344 33 324 324 343 leadd2dd 
 |-  ( ph -> ( ( 2 ^ 5 ) + 1 ) <_ ( ( 2 ^ 5 ) + ( 2 ^ 5 ) ) )
345 341 leidd 
 |-  ( ph -> ( ( 2 ^ 5 ) + ( 2 ^ 5 ) ) <_ ( ( 2 ^ 5 ) + ( 2 ^ 5 ) ) )
346 df-6 
 |-  6 = ( 5 + 1 )
347 346 a1i 
 |-  ( ph -> 6 = ( 5 + 1 ) )
348 347 oveq2d 
 |-  ( ph -> ( 2 ^ 6 ) = ( 2 ^ ( 5 + 1 ) ) )
349 2cn 
 |-  2 e. CC
350 349 a1i 
 |-  ( ph -> 2 e. CC )
351 193 a1i 
 |-  ( ph -> 1 e. NN0 )
352 350 351 322 expaddd 
 |-  ( ph -> ( 2 ^ ( 5 + 1 ) ) = ( ( 2 ^ 5 ) x. ( 2 ^ 1 ) ) )
353 348 352 eqtrd 
 |-  ( ph -> ( 2 ^ 6 ) = ( ( 2 ^ 5 ) x. ( 2 ^ 1 ) ) )
354 350 exp1d 
 |-  ( ph -> ( 2 ^ 1 ) = 2 )
355 354 oveq2d 
 |-  ( ph -> ( ( 2 ^ 5 ) x. ( 2 ^ 1 ) ) = ( ( 2 ^ 5 ) x. 2 ) )
356 353 355 eqtrd 
 |-  ( ph -> ( 2 ^ 6 ) = ( ( 2 ^ 5 ) x. 2 ) )
357 48 324 sselid 
 |-  ( ph -> ( 2 ^ 5 ) e. CC )
358 357 times2d 
 |-  ( ph -> ( ( 2 ^ 5 ) x. 2 ) = ( ( 2 ^ 5 ) + ( 2 ^ 5 ) ) )
359 356 358 eqtrd 
 |-  ( ph -> ( 2 ^ 6 ) = ( ( 2 ^ 5 ) + ( 2 ^ 5 ) ) )
360 359 eqcomd 
 |-  ( ph -> ( ( 2 ^ 5 ) + ( 2 ^ 5 ) ) = ( 2 ^ 6 ) )
361 345 360 breqtrd 
 |-  ( ph -> ( ( 2 ^ 5 ) + ( 2 ^ 5 ) ) <_ ( 2 ^ 6 ) )
362 325 341 337 344 361 letrd 
 |-  ( ph -> ( ( 2 ^ 5 ) + 1 ) <_ ( 2 ^ 6 ) )
363 312 320 325 334 337 340 362 logblebd 
 |-  ( ph -> ( 2 logb ( ( 2 ^ 5 ) + 1 ) ) <_ ( 2 logb ( 2 ^ 6 ) ) )
364 311 37 338 relogbexpd 
 |-  ( ph -> ( 2 logb ( 2 ^ 6 ) ) = 6 )
365 363 364 breqtrd 
 |-  ( ph -> ( 2 logb ( ( 2 ^ 5 ) + 1 ) ) <_ 6 )
366 318 365 eqbrtrd 
 |-  ( ph -> ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) <_ 6 )
367 6t2e12 
 |-  ( 6 x. 2 ) = ; 1 2
368 6cn 
 |-  6 e. CC
369 368 a1i 
 |-  ( ph -> 6 e. CC )
370 2nn 
 |-  2 e. NN
371 193 370 decnncl 
 |-  ; 1 2 e. NN
372 371 a1i 
 |-  ( ph -> ; 1 2 e. NN )
373 372 nnred 
 |-  ( ph -> ; 1 2 e. RR )
374 373 recnd 
 |-  ( ph -> ; 1 2 e. CC )
375 26 327 gtned 
 |-  ( ph -> 2 =/= 0 )
376 369 350 374 375 ldiv 
 |-  ( ph -> ( ( 6 x. 2 ) = ; 1 2 <-> 6 = ( ; 1 2 / 2 ) ) )
377 367 376 mpbii 
 |-  ( ph -> 6 = ( ; 1 2 / 2 ) )
378 366 377 breqtrd 
 |-  ( ph -> ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) <_ ( ; 1 2 / 2 ) )
379 323 33 readdcld 
 |-  ( ph -> ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) e. RR )
380 26 33 readdcld 
 |-  ( ph -> ( 0 + 1 ) e. RR )
381 26 ltp1d 
 |-  ( ph -> 0 < ( 0 + 1 ) )
382 26 323 33 331 ltadd1dd 
 |-  ( ph -> ( 0 + 1 ) < ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) )
383 26 380 379 381 382 lttrd 
 |-  ( ph -> 0 < ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) )
384 319 327 379 383 37 relogbcld 
 |-  ( ph -> ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) e. RR )
385 384 373 311 lemuldiv2d 
 |-  ( ph -> ( ( 2 x. ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) ) <_ ; 1 2 <-> ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) <_ ( ; 1 2 / 2 ) ) )
386 378 385 mpbird 
 |-  ( ph -> ( 2 x. ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) ) <_ ; 1 2 )
387 315 oveq1d 
 |-  ( ph -> ( ( 2 logb 4 ) ^ 2 ) = ( 2 ^ 2 ) )
388 387 307 eqtrdi 
 |-  ( ph -> ( ( 2 logb 4 ) ^ 2 ) = 4 )
389 388 oveq2d 
 |-  ( ph -> ( ; 1 6 - ( ( 2 logb 4 ) ^ 2 ) ) = ( ; 1 6 - 4 ) )
390 2nn0 
 |-  2 e. NN0
391 eqid 
 |-  ; 1 2 = ; 1 2
392 4cn 
 |-  4 e. CC
393 4p2e6 
 |-  ( 4 + 2 ) = 6
394 392 349 393 addcomli 
 |-  ( 2 + 4 ) = 6
395 193 390 174 391 394 decaddi 
 |-  ( ; 1 2 + 4 ) = ; 1 6
396 392 a1i 
 |-  ( ph -> 4 e. CC )
397 6nn 
 |-  6 e. NN
398 193 397 decnncl 
 |-  ; 1 6 e. NN
399 398 a1i 
 |-  ( ph -> ; 1 6 e. NN )
400 399 nnred 
 |-  ( ph -> ; 1 6 e. RR )
401 48 400 sselid 
 |-  ( ph -> ; 1 6 e. CC )
402 374 396 401 addlsub 
 |-  ( ph -> ( ( ; 1 2 + 4 ) = ; 1 6 <-> ; 1 2 = ( ; 1 6 - 4 ) ) )
403 395 402 mpbii 
 |-  ( ph -> ; 1 2 = ( ; 1 6 - 4 ) )
404 389 403 eqtr4d 
 |-  ( ph -> ( ; 1 6 - ( ( 2 logb 4 ) ^ 2 ) ) = ; 1 2 )
405 404 eqcomd 
 |-  ( ph -> ; 1 2 = ( ; 1 6 - ( ( 2 logb 4 ) ^ 2 ) ) )
406 386 405 breqtrd 
 |-  ( ph -> ( 2 x. ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) ) <_ ( ; 1 6 - ( ( 2 logb 4 ) ^ 2 ) ) )
407 319 384 remulcld 
 |-  ( ph -> ( 2 x. ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) ) e. RR )
408 321 resqcld 
 |-  ( ph -> ( ( 2 logb 4 ) ^ 2 ) e. RR )
409 leaddsub 
 |-  ( ( ( 2 x. ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) ) e. RR /\ ( ( 2 logb 4 ) ^ 2 ) e. RR /\ ; 1 6 e. RR ) -> ( ( ( 2 x. ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb 4 ) ^ 2 ) ) <_ ; 1 6 <-> ( 2 x. ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) ) <_ ( ; 1 6 - ( ( 2 logb 4 ) ^ 2 ) ) ) )
410 407 408 400 409 syl3anc 
 |-  ( ph -> ( ( ( 2 x. ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb 4 ) ^ 2 ) ) <_ ; 1 6 <-> ( 2 x. ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) ) <_ ( ; 1 6 - ( ( 2 logb 4 ) ^ 2 ) ) ) )
411 406 410 mpbird 
 |-  ( ph -> ( ( 2 x. ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb 4 ) ^ 2 ) ) <_ ; 1 6 )
412 315 oveq1d 
 |-  ( ph -> ( ( 2 logb 4 ) ^ 4 ) = ( 2 ^ 4 ) )
413 2exp4 
 |-  ( 2 ^ 4 ) = ; 1 6
414 412 413 eqtrdi 
 |-  ( ph -> ( ( 2 logb 4 ) ^ 4 ) = ; 1 6 )
415 414 eqcomd 
 |-  ( ph -> ; 1 6 = ( ( 2 logb 4 ) ^ 4 ) )
416 411 415 breqtrd 
 |-  ( ph -> ( ( 2 x. ( 2 logb ( ( ( 2 logb 4 ) ^ 5 ) + 1 ) ) ) + ( ( 2 logb 4 ) ^ 2 ) ) <_ ( ( 2 logb 4 ) ^ 4 ) )
417 11 12 219 261 262 272 280 287 288 302 306 416 4 dvle2 
 |-  ( ph -> ( ( 2 x. C ) + D ) <_ E )
418 1 2 3 16 5 6 7 417 aks4d1p1p4 
 |-  ( ph -> A < ( 2 ^ B ) )