Metamath Proof Explorer

Theorem bposlem9

Description: Lemma for bpos . Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014) (Proof shortened by AV, 15-Sep-2021)

Ref Expression
Hypotheses bposlem7.1 
|- F = ( n e. NN |-> ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` n ) ) ) + ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. n ) ) ) ) )
bposlem7.2 
|- G = ( x e. RR+ |-> ( ( log ` x ) / x ) )
bposlem9.3 
|- ( ph -> N e. NN )
bposlem9.4 
|- ( ph -> ; 6 4 < N )
bposlem9.5 
|- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
Assertion bposlem9 
|- ( ph -> ps )

Proof

Step Hyp Ref Expression
1 bposlem7.1 
 |-  F = ( n e. NN |-> ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` n ) ) ) + ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. n ) ) ) ) )
2 bposlem7.2 
 |-  G = ( x e. RR+ |-> ( ( log ` x ) / x ) )
3 bposlem9.3 
 |-  ( ph -> N e. NN )
4 bposlem9.4 
 |-  ( ph -> ; 6 4 < N )
5 bposlem9.5 
 |-  ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
6 6nn0 
 |-  6 e. NN0
7 4nn 
 |-  4 e. NN
8 6 7 decnncl 
 |-  ; 6 4 e. NN
9 8 a1i 
 |-  ( ph -> ; 6 4 e. NN )
10 ere 
 |-  _e e. RR
11 8re 
 |-  8 e. RR
12 egt2lt3 
 |-  ( 2 < _e /\ _e < 3 )
13 12 simpri 
 |-  _e < 3
14 3lt8 
 |-  3 < 8
15 3re 
 |-  3 e. RR
16 10 15 11 lttri 
 |-  ( ( _e < 3 /\ 3 < 8 ) -> _e < 8 )
17 13 14 16 mp2an 
 |-  _e < 8
18 10 11 17 ltleii 
 |-  _e <_ 8
19 0re 
 |-  0 e. RR
20 epos 
 |-  0 < _e
21 19 10 20 ltleii 
 |-  0 <_ _e
22 8pos 
 |-  0 < 8
23 19 11 22 ltleii 
 |-  0 <_ 8
24 le2sq 
 |-  ( ( ( _e e. RR /\ 0 <_ _e ) /\ ( 8 e. RR /\ 0 <_ 8 ) ) -> ( _e <_ 8 <-> ( _e ^ 2 ) <_ ( 8 ^ 2 ) ) )
25 10 21 11 23 24 mp4an 
 |-  ( _e <_ 8 <-> ( _e ^ 2 ) <_ ( 8 ^ 2 ) )
26 18 25 mpbi 
 |-  ( _e ^ 2 ) <_ ( 8 ^ 2 )
27 11 recni 
 |-  8 e. CC
28 27 sqvali 
 |-  ( 8 ^ 2 ) = ( 8 x. 8 )
29 8t8e64 
 |-  ( 8 x. 8 ) = ; 6 4
30 28 29 eqtri 
 |-  ( 8 ^ 2 ) = ; 6 4
31 26 30 breqtri 
 |-  ( _e ^ 2 ) <_ ; 6 4
32 31 a1i 
 |-  ( ph -> ( _e ^ 2 ) <_ ; 6 4 )
33 10 resqcli 
 |-  ( _e ^ 2 ) e. RR
34 33 a1i 
 |-  ( ph -> ( _e ^ 2 ) e. RR )
35 8 nnrei 
 |-  ; 6 4 e. RR
36 35 a1i 
 |-  ( ph -> ; 6 4 e. RR )
37 3 nnred 
 |-  ( ph -> N e. RR )
38 ltle 
 |-  ( ( ; 6 4 e. RR /\ N e. RR ) -> ( ; 6 4 < N -> ; 6 4 <_ N ) )
39 35 37 38 sylancr 
 |-  ( ph -> ( ; 6 4 < N -> ; 6 4 <_ N ) )
40 4 39 mpd 
 |-  ( ph -> ; 6 4 <_ N )
41 34 36 37 32 40 letrd 
 |-  ( ph -> ( _e ^ 2 ) <_ N )
42 1 2 9 3 32 41 bposlem7 
 |-  ( ph -> ( ; 6 4 < N -> ( F ` N ) < ( F ` ; 6 4 ) ) )
43 4 42 mpd 
 |-  ( ph -> ( F ` N ) < ( F ` ; 6 4 ) )
44 1 2 bposlem8 
 |-  ( ( F ` ; 6 4 ) e. RR /\ ( F ` ; 6 4 ) < ( log ` 2 ) )
45 44 a1i 
 |-  ( ph -> ( ( F ` ; 6 4 ) e. RR /\ ( F ` ; 6 4 ) < ( log ` 2 ) ) )
46 45 simpld 
 |-  ( ph -> ( F ` ; 6 4 ) e. RR )
47 2fveq3 
 |-  ( n = N -> ( G ` ( sqrt ` n ) ) = ( G ` ( sqrt ` N ) ) )
48 47 oveq2d 
 |-  ( n = N -> ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` n ) ) ) = ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) )
49 fvoveq1 
 |-  ( n = N -> ( G ` ( n / 2 ) ) = ( G ` ( N / 2 ) ) )
50 49 oveq2d 
 |-  ( n = N -> ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) = ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) )
51 48 50 oveq12d 
 |-  ( n = N -> ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` n ) ) ) + ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) ) = ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) )
52 oveq2 
 |-  ( n = N -> ( 2 x. n ) = ( 2 x. N ) )
53 52 fveq2d 
 |-  ( n = N -> ( sqrt ` ( 2 x. n ) ) = ( sqrt ` ( 2 x. N ) ) )
54 53 oveq2d 
 |-  ( n = N -> ( ( log ` 2 ) / ( sqrt ` ( 2 x. n ) ) ) = ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) )
55 51 54 oveq12d 
 |-  ( n = N -> ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` n ) ) ) + ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. n ) ) ) ) = ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) )
56 ovex 
 |-  ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) e. _V
57 55 1 56 fvmpt 
 |-  ( N e. NN -> ( F ` N ) = ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) )
58 3 57 syl 
 |-  ( ph -> ( F ` N ) = ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) )
59 sqrt2re 
 |-  ( sqrt ` 2 ) e. RR
60 3 nnrpd 
 |-  ( ph -> N e. RR+ )
61 60 rpsqrtcld 
 |-  ( ph -> ( sqrt ` N ) e. RR+ )
62 fveq2 
 |-  ( x = ( sqrt ` N ) -> ( log ` x ) = ( log ` ( sqrt ` N ) ) )
63 id 
 |-  ( x = ( sqrt ` N ) -> x = ( sqrt ` N ) )
64 62 63 oveq12d 
 |-  ( x = ( sqrt ` N ) -> ( ( log ` x ) / x ) = ( ( log ` ( sqrt ` N ) ) / ( sqrt ` N ) ) )
65 ovex 
 |-  ( ( log ` ( sqrt ` N ) ) / ( sqrt ` N ) ) e. _V
66 64 2 65 fvmpt 
 |-  ( ( sqrt ` N ) e. RR+ -> ( G ` ( sqrt ` N ) ) = ( ( log ` ( sqrt ` N ) ) / ( sqrt ` N ) ) )
67 61 66 syl 
 |-  ( ph -> ( G ` ( sqrt ` N ) ) = ( ( log ` ( sqrt ` N ) ) / ( sqrt ` N ) ) )
68 61 relogcld 
 |-  ( ph -> ( log ` ( sqrt ` N ) ) e. RR )
69 68 61 rerpdivcld 
 |-  ( ph -> ( ( log ` ( sqrt ` N ) ) / ( sqrt ` N ) ) e. RR )
70 67 69 eqeltrd 
 |-  ( ph -> ( G ` ( sqrt ` N ) ) e. RR )
71 remulcl 
 |-  ( ( ( sqrt ` 2 ) e. RR /\ ( G ` ( sqrt ` N ) ) e. RR ) -> ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) e. RR )
72 59 70 71 sylancr 
 |-  ( ph -> ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) e. RR )
73 9re 
 |-  9 e. RR
74 4re 
 |-  4 e. RR
75 4ne0 
 |-  4 =/= 0
76 73 74 75 redivcli 
 |-  ( 9 / 4 ) e. RR
77 60 rphalfcld 
 |-  ( ph -> ( N / 2 ) e. RR+ )
78 fveq2 
 |-  ( x = ( N / 2 ) -> ( log ` x ) = ( log ` ( N / 2 ) ) )
79 id 
 |-  ( x = ( N / 2 ) -> x = ( N / 2 ) )
80 78 79 oveq12d 
 |-  ( x = ( N / 2 ) -> ( ( log ` x ) / x ) = ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) )
81 ovex 
 |-  ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) e. _V
82 80 2 81 fvmpt 
 |-  ( ( N / 2 ) e. RR+ -> ( G ` ( N / 2 ) ) = ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) )
83 77 82 syl 
 |-  ( ph -> ( G ` ( N / 2 ) ) = ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) )
84 77 relogcld 
 |-  ( ph -> ( log ` ( N / 2 ) ) e. RR )
85 84 77 rerpdivcld 
 |-  ( ph -> ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) e. RR )
86 83 85 eqeltrd 
 |-  ( ph -> ( G ` ( N / 2 ) ) e. RR )
87 remulcl 
 |-  ( ( ( 9 / 4 ) e. RR /\ ( G ` ( N / 2 ) ) e. RR ) -> ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) e. RR )
88 76 86 87 sylancr 
 |-  ( ph -> ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) e. RR )
89 72 88 readdcld 
 |-  ( ph -> ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) e. RR )
90 2rp 
 |-  2 e. RR+
91 relogcl 
 |-  ( 2 e. RR+ -> ( log ` 2 ) e. RR )
92 90 91 ax-mp 
 |-  ( log ` 2 ) e. RR
93 rpmulcl 
 |-  ( ( 2 e. RR+ /\ N e. RR+ ) -> ( 2 x. N ) e. RR+ )
94 90 60 93 sylancr 
 |-  ( ph -> ( 2 x. N ) e. RR+ )
95 94 rpsqrtcld 
 |-  ( ph -> ( sqrt ` ( 2 x. N ) ) e. RR+ )
96 rerpdivcl 
 |-  ( ( ( log ` 2 ) e. RR /\ ( sqrt ` ( 2 x. N ) ) e. RR+ ) -> ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) e. RR )
97 92 95 96 sylancr 
 |-  ( ph -> ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) e. RR )
98 89 97 readdcld 
 |-  ( ph -> ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) e. RR )
99 58 98 eqeltrd 
 |-  ( ph -> ( F ` N ) e. RR )
100 92 a1i 
 |-  ( ph -> ( log ` 2 ) e. RR )
101 45 simprd 
 |-  ( ph -> ( F ` ; 6 4 ) < ( log ` 2 ) )
102 nnrp 
 |-  ( 4 e. NN -> 4 e. RR+ )
103 7 102 ax-mp 
 |-  4 e. RR+
104 relogcl 
 |-  ( 4 e. RR+ -> ( log ` 4 ) e. RR )
105 103 104 ax-mp 
 |-  ( log ` 4 ) e. RR
106 remulcl 
 |-  ( ( N e. RR /\ ( log ` 4 ) e. RR ) -> ( N x. ( log ` 4 ) ) e. RR )
107 37 105 106 sylancl 
 |-  ( ph -> ( N x. ( log ` 4 ) ) e. RR )
108 60 relogcld 
 |-  ( ph -> ( log ` N ) e. RR )
109 107 108 resubcld 
 |-  ( ph -> ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) e. RR )
110 rpre 
 |-  ( ( 2 x. N ) e. RR+ -> ( 2 x. N ) e. RR )
111 rpge0 
 |-  ( ( 2 x. N ) e. RR+ -> 0 <_ ( 2 x. N ) )
112 110 111 resqrtcld 
 |-  ( ( 2 x. N ) e. RR+ -> ( sqrt ` ( 2 x. N ) ) e. RR )
113 94 112 syl 
 |-  ( ph -> ( sqrt ` ( 2 x. N ) ) e. RR )
114 3nn 
 |-  3 e. NN
115 nndivre 
 |-  ( ( ( sqrt ` ( 2 x. N ) ) e. RR /\ 3 e. NN ) -> ( ( sqrt ` ( 2 x. N ) ) / 3 ) e. RR )
116 113 114 115 sylancl 
 |-  ( ph -> ( ( sqrt ` ( 2 x. N ) ) / 3 ) e. RR )
117 2re 
 |-  2 e. RR
118 readdcl 
 |-  ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) e. RR /\ 2 e. RR ) -> ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) e. RR )
119 116 117 118 sylancl 
 |-  ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) e. RR )
120 94 relogcld 
 |-  ( ph -> ( log ` ( 2 x. N ) ) e. RR )
121 119 120 remulcld 
 |-  ( ph -> ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) e. RR )
122 remulcl 
 |-  ( ( 4 e. RR /\ N e. RR ) -> ( 4 x. N ) e. RR )
123 74 37 122 sylancr 
 |-  ( ph -> ( 4 x. N ) e. RR )
124 nndivre 
 |-  ( ( ( 4 x. N ) e. RR /\ 3 e. NN ) -> ( ( 4 x. N ) / 3 ) e. RR )
125 123 114 124 sylancl 
 |-  ( ph -> ( ( 4 x. N ) / 3 ) e. RR )
126 5re 
 |-  5 e. RR
127 resubcl 
 |-  ( ( ( ( 4 x. N ) / 3 ) e. RR /\ 5 e. RR ) -> ( ( ( 4 x. N ) / 3 ) - 5 ) e. RR )
128 125 126 127 sylancl 
 |-  ( ph -> ( ( ( 4 x. N ) / 3 ) - 5 ) e. RR )
129 remulcl 
 |-  ( ( ( ( ( 4 x. N ) / 3 ) - 5 ) e. RR /\ ( log ` 2 ) e. RR ) -> ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) e. RR )
130 128 92 129 sylancl 
 |-  ( ph -> ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) e. RR )
131 121 130 readdcld 
 |-  ( ph -> ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) e. RR )
132 remulcl 
 |-  ( ( ( ( 4 x. N ) / 3 ) e. RR /\ ( log ` 2 ) e. RR ) -> ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) e. RR )
133 125 92 132 sylancl 
 |-  ( ph -> ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) e. RR )
134 133 108 resubcld 
 |-  ( ph -> ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) e. RR )
135 3 nnzd 
 |-  ( ph -> N e. ZZ )
136 df-5 
 |-  5 = ( 4 + 1 )
137 74 a1i 
 |-  ( ph -> 4 e. RR )
138 6nn 
 |-  6 e. NN
139 4nn0 
 |-  4 e. NN0
140 4lt10 
 |-  4 < ; 1 0
141 138 139 139 140 declti 
 |-  4 < ; 6 4
142 141 a1i 
 |-  ( ph -> 4 < ; 6 4 )
143 137 36 37 142 4 lttrd 
 |-  ( ph -> 4 < N )
144 4z 
 |-  4 e. ZZ
145 zltp1le 
 |-  ( ( 4 e. ZZ /\ N e. ZZ ) -> ( 4 < N <-> ( 4 + 1 ) <_ N ) )
146 144 135 145 sylancr 
 |-  ( ph -> ( 4 < N <-> ( 4 + 1 ) <_ N ) )
147 143 146 mpbid 
 |-  ( ph -> ( 4 + 1 ) <_ N )
148 136 147 eqbrtrid 
 |-  ( ph -> 5 <_ N )
149 5nn 
 |-  5 e. NN
150 149 nnzi 
 |-  5 e. ZZ
151 150 eluz1i 
 |-  ( N e. ( ZZ>= ` 5 ) <-> ( N e. ZZ /\ 5 <_ N ) )
152 135 148 151 sylanbrc 
 |-  ( ph -> N e. ( ZZ>= ` 5 ) )
153 breq2 
 |-  ( p = q -> ( N < p <-> N < q ) )
154 breq1 
 |-  ( p = q -> ( p <_ ( 2 x. N ) <-> q <_ ( 2 x. N ) ) )
155 153 154 anbi12d 
 |-  ( p = q -> ( ( N < p /\ p <_ ( 2 x. N ) ) <-> ( N < q /\ q <_ ( 2 x. N ) ) ) )
156 155 cbvrexvw 
 |-  ( E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) <-> E. q e. Prime ( N < q /\ q <_ ( 2 x. N ) ) )
157 5 156 sylnib 
 |-  ( ph -> -. E. q e. Prime ( N < q /\ q <_ ( 2 x. N ) ) )
158 eqid 
 |-  ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) ) = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )
159 eqid 
 |-  ( |_ ` ( ( 2 x. N ) / 3 ) ) = ( |_ ` ( ( 2 x. N ) / 3 ) )
160 eqid 
 |-  ( |_ ` ( sqrt ` ( 2 x. N ) ) ) = ( |_ ` ( sqrt ` ( 2 x. N ) ) )
161 152 157 158 159 160 bposlem6 
 |-  ( ph -> ( ( 4 ^ N ) / N ) < ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )
162 reexplog 
 |-  ( ( 4 e. RR+ /\ N e. ZZ ) -> ( 4 ^ N ) = ( exp ` ( N x. ( log ` 4 ) ) ) )
163 103 135 162 sylancr 
 |-  ( ph -> ( 4 ^ N ) = ( exp ` ( N x. ( log ` 4 ) ) ) )
164 60 reeflogd 
 |-  ( ph -> ( exp ` ( log ` N ) ) = N )
165 164 eqcomd 
 |-  ( ph -> N = ( exp ` ( log ` N ) ) )
166 163 165 oveq12d 
 |-  ( ph -> ( ( 4 ^ N ) / N ) = ( ( exp ` ( N x. ( log ` 4 ) ) ) / ( exp ` ( log ` N ) ) ) )
167 107 recnd 
 |-  ( ph -> ( N x. ( log ` 4 ) ) e. CC )
168 108 recnd 
 |-  ( ph -> ( log ` N ) e. CC )
169 efsub 
 |-  ( ( ( N x. ( log ` 4 ) ) e. CC /\ ( log ` N ) e. CC ) -> ( exp ` ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) ) = ( ( exp ` ( N x. ( log ` 4 ) ) ) / ( exp ` ( log ` N ) ) ) )
170 167 168 169 syl2anc 
 |-  ( ph -> ( exp ` ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) ) = ( ( exp ` ( N x. ( log ` 4 ) ) ) / ( exp ` ( log ` N ) ) ) )
171 166 170 eqtr4d 
 |-  ( ph -> ( ( 4 ^ N ) / N ) = ( exp ` ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) ) )
172 94 rpcnd 
 |-  ( ph -> ( 2 x. N ) e. CC )
173 94 rpne0d 
 |-  ( ph -> ( 2 x. N ) =/= 0 )
174 119 recnd 
 |-  ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) e. CC )
175 172 173 174 cxpefd 
 |-  ( ph -> ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) = ( exp ` ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) ) )
176 2cn 
 |-  2 e. CC
177 2ne0 
 |-  2 =/= 0
178 128 recnd 
 |-  ( ph -> ( ( ( 4 x. N ) / 3 ) - 5 ) e. CC )
179 cxpef 
 |-  ( ( 2 e. CC /\ 2 =/= 0 /\ ( ( ( 4 x. N ) / 3 ) - 5 ) e. CC ) -> ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) = ( exp ` ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) )
180 176 177 178 179 mp3an12i 
 |-  ( ph -> ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) = ( exp ` ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) )
181 175 180 oveq12d 
 |-  ( ph -> ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) = ( ( exp ` ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) ) x. ( exp ` ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) ) )
182 121 recnd 
 |-  ( ph -> ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) e. CC )
183 130 recnd 
 |-  ( ph -> ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) e. CC )
184 efadd 
 |-  ( ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) e. CC /\ ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) e. CC ) -> ( exp ` ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) ) = ( ( exp ` ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) ) x. ( exp ` ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) ) )
185 182 183 184 syl2anc 
 |-  ( ph -> ( exp ` ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) ) = ( ( exp ` ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) ) x. ( exp ` ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) ) )
186 181 185 eqtr4d 
 |-  ( ph -> ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) = ( exp ` ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) ) )
187 161 171 186 3brtr3d 
 |-  ( ph -> ( exp ` ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) ) < ( exp ` ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) ) )
188 eflt 
 |-  ( ( ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) e. RR /\ ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) e. RR ) -> ( ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) < ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) <-> ( exp ` ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) ) < ( exp ` ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) ) ) )
189 109 131 188 syl2anc 
 |-  ( ph -> ( ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) < ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) <-> ( exp ` ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) ) < ( exp ` ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) ) ) )
190 187 189 mpbird 
 |-  ( ph -> ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) < ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) )
191 109 131 134 190 ltsub1dd 
 |-  ( ph -> ( ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) - ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) ) < ( ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) - ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) ) )
192 37 recnd 
 |-  ( ph -> N e. CC )
193 mulcom 
 |-  ( ( 2 e. CC /\ N e. CC ) -> ( 2 x. N ) = ( N x. 2 ) )
194 176 192 193 sylancr 
 |-  ( ph -> ( 2 x. N ) = ( N x. 2 ) )
195 194 oveq1d 
 |-  ( ph -> ( ( 2 x. N ) x. ( log ` 2 ) ) = ( ( N x. 2 ) x. ( log ` 2 ) ) )
196 92 recni 
 |-  ( log ` 2 ) e. CC
197 mulass 
 |-  ( ( N e. CC /\ 2 e. CC /\ ( log ` 2 ) e. CC ) -> ( ( N x. 2 ) x. ( log ` 2 ) ) = ( N x. ( 2 x. ( log ` 2 ) ) ) )
198 176 196 197 mp3an23 
 |-  ( N e. CC -> ( ( N x. 2 ) x. ( log ` 2 ) ) = ( N x. ( 2 x. ( log ` 2 ) ) ) )
199 192 198 syl 
 |-  ( ph -> ( ( N x. 2 ) x. ( log ` 2 ) ) = ( N x. ( 2 x. ( log ` 2 ) ) ) )
200 196 2timesi 
 |-  ( 2 x. ( log ` 2 ) ) = ( ( log ` 2 ) + ( log ` 2 ) )
201 relogmul 
 |-  ( ( 2 e. RR+ /\ 2 e. RR+ ) -> ( log ` ( 2 x. 2 ) ) = ( ( log ` 2 ) + ( log ` 2 ) ) )
202 90 90 201 mp2an 
 |-  ( log ` ( 2 x. 2 ) ) = ( ( log ` 2 ) + ( log ` 2 ) )
203 2t2e4 
 |-  ( 2 x. 2 ) = 4
204 203 fveq2i 
 |-  ( log ` ( 2 x. 2 ) ) = ( log ` 4 )
205 200 202 204 3eqtr2i 
 |-  ( 2 x. ( log ` 2 ) ) = ( log ` 4 )
206 205 oveq2i 
 |-  ( N x. ( 2 x. ( log ` 2 ) ) ) = ( N x. ( log ` 4 ) )
207 199 206 eqtrdi 
 |-  ( ph -> ( ( N x. 2 ) x. ( log ` 2 ) ) = ( N x. ( log ` 4 ) ) )
208 195 207 eqtrd 
 |-  ( ph -> ( ( 2 x. N ) x. ( log ` 2 ) ) = ( N x. ( log ` 4 ) ) )
209 208 oveq1d 
 |-  ( ph -> ( ( ( 2 x. N ) x. ( log ` 2 ) ) - ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) ) = ( ( N x. ( log ` 4 ) ) - ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) ) )
210 125 recnd 
 |-  ( ph -> ( ( 4 x. N ) / 3 ) e. CC )
211 3rp 
 |-  3 e. RR+
212 rpdivcl 
 |-  ( ( ( 2 x. N ) e. RR+ /\ 3 e. RR+ ) -> ( ( 2 x. N ) / 3 ) e. RR+ )
213 94 211 212 sylancl 
 |-  ( ph -> ( ( 2 x. N ) / 3 ) e. RR+ )
214 213 rpcnd 
 |-  ( ph -> ( ( 2 x. N ) / 3 ) e. CC )
215 4p2e6 
 |-  ( 4 + 2 ) = 6
216 215 oveq1i 
 |-  ( ( 4 + 2 ) x. N ) = ( 6 x. N )
217 4cn 
 |-  4 e. CC
218 adddir 
 |-  ( ( 4 e. CC /\ 2 e. CC /\ N e. CC ) -> ( ( 4 + 2 ) x. N ) = ( ( 4 x. N ) + ( 2 x. N ) ) )
219 217 176 192 218 mp3an12i 
 |-  ( ph -> ( ( 4 + 2 ) x. N ) = ( ( 4 x. N ) + ( 2 x. N ) ) )
220 216 219 eqtr3id 
 |-  ( ph -> ( 6 x. N ) = ( ( 4 x. N ) + ( 2 x. N ) ) )
221 220 oveq1d 
 |-  ( ph -> ( ( 6 x. N ) / 3 ) = ( ( ( 4 x. N ) + ( 2 x. N ) ) / 3 ) )
222 6cn 
 |-  6 e. CC
223 3cn 
 |-  3 e. CC
224 3ne0 
 |-  3 =/= 0
225 223 224 pm3.2i 
 |-  ( 3 e. CC /\ 3 =/= 0 )
226 div23 
 |-  ( ( 6 e. CC /\ N e. CC /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( ( 6 x. N ) / 3 ) = ( ( 6 / 3 ) x. N ) )
227 222 225 226 mp3an13 
 |-  ( N e. CC -> ( ( 6 x. N ) / 3 ) = ( ( 6 / 3 ) x. N ) )
228 192 227 syl 
 |-  ( ph -> ( ( 6 x. N ) / 3 ) = ( ( 6 / 3 ) x. N ) )
229 3t2e6 
 |-  ( 3 x. 2 ) = 6
230 229 oveq1i 
 |-  ( ( 3 x. 2 ) / 3 ) = ( 6 / 3 )
231 176 223 224 divcan3i 
 |-  ( ( 3 x. 2 ) / 3 ) = 2
232 230 231 eqtr3i 
 |-  ( 6 / 3 ) = 2
233 232 oveq1i 
 |-  ( ( 6 / 3 ) x. N ) = ( 2 x. N )
234 228 233 eqtrdi 
 |-  ( ph -> ( ( 6 x. N ) / 3 ) = ( 2 x. N ) )
235 123 recnd 
 |-  ( ph -> ( 4 x. N ) e. CC )
236 remulcl 
 |-  ( ( 2 e. RR /\ N e. RR ) -> ( 2 x. N ) e. RR )
237 117 37 236 sylancr 
 |-  ( ph -> ( 2 x. N ) e. RR )
238 237 recnd 
 |-  ( ph -> ( 2 x. N ) e. CC )
239 divdir 
 |-  ( ( ( 4 x. N ) e. CC /\ ( 2 x. N ) e. CC /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( ( ( 4 x. N ) + ( 2 x. N ) ) / 3 ) = ( ( ( 4 x. N ) / 3 ) + ( ( 2 x. N ) / 3 ) ) )
240 225 239 mp3an3 
 |-  ( ( ( 4 x. N ) e. CC /\ ( 2 x. N ) e. CC ) -> ( ( ( 4 x. N ) + ( 2 x. N ) ) / 3 ) = ( ( ( 4 x. N ) / 3 ) + ( ( 2 x. N ) / 3 ) ) )
241 235 238 240 syl2anc 
 |-  ( ph -> ( ( ( 4 x. N ) + ( 2 x. N ) ) / 3 ) = ( ( ( 4 x. N ) / 3 ) + ( ( 2 x. N ) / 3 ) ) )
242 221 234 241 3eqtr3d 
 |-  ( ph -> ( 2 x. N ) = ( ( ( 4 x. N ) / 3 ) + ( ( 2 x. N ) / 3 ) ) )
243 210 214 242 mvrladdd 
 |-  ( ph -> ( ( 2 x. N ) - ( ( 4 x. N ) / 3 ) ) = ( ( 2 x. N ) / 3 ) )
244 243 oveq1d 
 |-  ( ph -> ( ( ( 2 x. N ) - ( ( 4 x. N ) / 3 ) ) x. ( log ` 2 ) ) = ( ( ( 2 x. N ) / 3 ) x. ( log ` 2 ) ) )
245 100 recnd 
 |-  ( ph -> ( log ` 2 ) e. CC )
246 238 210 245 subdird 
 |-  ( ph -> ( ( ( 2 x. N ) - ( ( 4 x. N ) / 3 ) ) x. ( log ` 2 ) ) = ( ( ( 2 x. N ) x. ( log ` 2 ) ) - ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) ) )
247 244 246 eqtr3d 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( log ` 2 ) ) = ( ( ( 2 x. N ) x. ( log ` 2 ) ) - ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) ) )
248 133 recnd 
 |-  ( ph -> ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) e. CC )
249 167 248 168 nnncan2d 
 |-  ( ph -> ( ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) - ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) ) = ( ( N x. ( log ` 4 ) ) - ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) ) )
250 209 247 249 3eqtr4d 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( log ` 2 ) ) = ( ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) - ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) ) )
251 116 recnd 
 |-  ( ph -> ( ( sqrt ` ( 2 x. N ) ) / 3 ) e. CC )
252 176 a1i 
 |-  ( ph -> 2 e. CC )
253 120 recnd 
 |-  ( ph -> ( log ` ( 2 x. N ) ) e. CC )
254 251 252 253 adddird 
 |-  ( ph -> ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) = ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) + ( 2 x. ( log ` ( 2 x. N ) ) ) ) )
255 relogmul 
 |-  ( ( 2 e. RR+ /\ N e. RR+ ) -> ( log ` ( 2 x. N ) ) = ( ( log ` 2 ) + ( log ` N ) ) )
256 90 60 255 sylancr 
 |-  ( ph -> ( log ` ( 2 x. N ) ) = ( ( log ` 2 ) + ( log ` N ) ) )
257 256 oveq2d 
 |-  ( ph -> ( 2 x. ( log ` ( 2 x. N ) ) ) = ( 2 x. ( ( log ` 2 ) + ( log ` N ) ) ) )
258 252 245 168 adddid 
 |-  ( ph -> ( 2 x. ( ( log ` 2 ) + ( log ` N ) ) ) = ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) )
259 257 258 eqtrd 
 |-  ( ph -> ( 2 x. ( log ` ( 2 x. N ) ) ) = ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) )
260 259 oveq2d 
 |-  ( ph -> ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) + ( 2 x. ( log ` ( 2 x. N ) ) ) ) = ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) + ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) ) )
261 254 260 eqtrd 
 |-  ( ph -> ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) = ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) + ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) ) )
262 5cn 
 |-  5 e. CC
263 262 a1i 
 |-  ( ph -> 5 e. CC )
264 210 263 245 subdird 
 |-  ( ph -> ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) = ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( 5 x. ( log ` 2 ) ) ) )
265 264 oveq1d 
 |-  ( ph -> ( ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) - ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) ) = ( ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( 5 x. ( log ` 2 ) ) ) - ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) ) )
266 262 196 mulcli 
 |-  ( 5 x. ( log ` 2 ) ) e. CC
267 266 a1i 
 |-  ( ph -> ( 5 x. ( log ` 2 ) ) e. CC )
268 248 267 168 nnncan1d 
 |-  ( ph -> ( ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( 5 x. ( log ` 2 ) ) ) - ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) ) = ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) )
269 265 268 eqtrd 
 |-  ( ph -> ( ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) - ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) ) = ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) )
270 261 269 oveq12d 
 |-  ( ph -> ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) - ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) ) ) = ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) + ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) ) + ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) ) )
271 134 recnd 
 |-  ( ph -> ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) e. CC )
272 182 183 271 addsubassd 
 |-  ( ph -> ( ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) - ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) ) = ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) - ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) ) ) )
273 262 223 196 subdiri 
 |-  ( ( 5 - 3 ) x. ( log ` 2 ) ) = ( ( 5 x. ( log ` 2 ) ) - ( 3 x. ( log ` 2 ) ) )
274 3p2e5 
 |-  ( 3 + 2 ) = 5
275 274 oveq1i 
 |-  ( ( 3 + 2 ) - 3 ) = ( 5 - 3 )
276 pncan2 
 |-  ( ( 3 e. CC /\ 2 e. CC ) -> ( ( 3 + 2 ) - 3 ) = 2 )
277 223 176 276 mp2an 
 |-  ( ( 3 + 2 ) - 3 ) = 2
278 275 277 eqtr3i 
 |-  ( 5 - 3 ) = 2
279 278 oveq1i 
 |-  ( ( 5 - 3 ) x. ( log ` 2 ) ) = ( 2 x. ( log ` 2 ) )
280 273 279 eqtr3i 
 |-  ( ( 5 x. ( log ` 2 ) ) - ( 3 x. ( log ` 2 ) ) ) = ( 2 x. ( log ` 2 ) )
281 280 a1i 
 |-  ( ph -> ( ( 5 x. ( log ` 2 ) ) - ( 3 x. ( log ` 2 ) ) ) = ( 2 x. ( log ` 2 ) ) )
282 mulcl 
 |-  ( ( 2 e. CC /\ ( log ` N ) e. CC ) -> ( 2 x. ( log ` N ) ) e. CC )
283 176 168 282 sylancr 
 |-  ( ph -> ( 2 x. ( log ` N ) ) e. CC )
284 df-3 
 |-  3 = ( 2 + 1 )
285 284 oveq1i 
 |-  ( 3 x. ( log ` N ) ) = ( ( 2 + 1 ) x. ( log ` N ) )
286 1cnd 
 |-  ( ph -> 1 e. CC )
287 252 286 168 adddird 
 |-  ( ph -> ( ( 2 + 1 ) x. ( log ` N ) ) = ( ( 2 x. ( log ` N ) ) + ( 1 x. ( log ` N ) ) ) )
288 285 287 syl5eq 
 |-  ( ph -> ( 3 x. ( log ` N ) ) = ( ( 2 x. ( log ` N ) ) + ( 1 x. ( log ` N ) ) ) )
289 168 mulid2d 
 |-  ( ph -> ( 1 x. ( log ` N ) ) = ( log ` N ) )
290 289 oveq2d 
 |-  ( ph -> ( ( 2 x. ( log ` N ) ) + ( 1 x. ( log ` N ) ) ) = ( ( 2 x. ( log ` N ) ) + ( log ` N ) ) )
291 288 290 eqtrd 
 |-  ( ph -> ( 3 x. ( log ` N ) ) = ( ( 2 x. ( log ` N ) ) + ( log ` N ) ) )
292 291 oveq1d 
 |-  ( ph -> ( ( 3 x. ( log ` N ) ) - ( 5 x. ( log ` 2 ) ) ) = ( ( ( 2 x. ( log ` N ) ) + ( log ` N ) ) - ( 5 x. ( log ` 2 ) ) ) )
293 283 168 267 292 assraddsubd 
 |-  ( ph -> ( ( 3 x. ( log ` N ) ) - ( 5 x. ( log ` 2 ) ) ) = ( ( 2 x. ( log ` N ) ) + ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) ) )
294 281 293 oveq12d 
 |-  ( ph -> ( ( ( 5 x. ( log ` 2 ) ) - ( 3 x. ( log ` 2 ) ) ) + ( ( 3 x. ( log ` N ) ) - ( 5 x. ( log ` 2 ) ) ) ) = ( ( 2 x. ( log ` 2 ) ) + ( ( 2 x. ( log ` N ) ) + ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) ) ) )
295 relogdiv 
 |-  ( ( N e. RR+ /\ 2 e. RR+ ) -> ( log ` ( N / 2 ) ) = ( ( log ` N ) - ( log ` 2 ) ) )
296 60 90 295 sylancl 
 |-  ( ph -> ( log ` ( N / 2 ) ) = ( ( log ` N ) - ( log ` 2 ) ) )
297 296 oveq2d 
 |-  ( ph -> ( 3 x. ( log ` ( N / 2 ) ) ) = ( 3 x. ( ( log ` N ) - ( log ` 2 ) ) ) )
298 subdi 
 |-  ( ( 3 e. CC /\ ( log ` N ) e. CC /\ ( log ` 2 ) e. CC ) -> ( 3 x. ( ( log ` N ) - ( log ` 2 ) ) ) = ( ( 3 x. ( log ` N ) ) - ( 3 x. ( log ` 2 ) ) ) )
299 223 196 298 mp3an13 
 |-  ( ( log ` N ) e. CC -> ( 3 x. ( ( log ` N ) - ( log ` 2 ) ) ) = ( ( 3 x. ( log ` N ) ) - ( 3 x. ( log ` 2 ) ) ) )
300 168 299 syl 
 |-  ( ph -> ( 3 x. ( ( log ` N ) - ( log ` 2 ) ) ) = ( ( 3 x. ( log ` N ) ) - ( 3 x. ( log ` 2 ) ) ) )
301 297 300 eqtrd 
 |-  ( ph -> ( 3 x. ( log ` ( N / 2 ) ) ) = ( ( 3 x. ( log ` N ) ) - ( 3 x. ( log ` 2 ) ) ) )
302 div23 
 |-  ( ( 2 e. CC /\ N e. CC /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( ( 2 x. N ) / 3 ) = ( ( 2 / 3 ) x. N ) )
303 176 225 302 mp3an13 
 |-  ( N e. CC -> ( ( 2 x. N ) / 3 ) = ( ( 2 / 3 ) x. N ) )
304 192 303 syl 
 |-  ( ph -> ( ( 2 x. N ) / 3 ) = ( ( 2 / 3 ) x. N ) )
305 223 176 223 176 177 177 divmuldivi 
 |-  ( ( 3 / 2 ) x. ( 3 / 2 ) ) = ( ( 3 x. 3 ) / ( 2 x. 2 ) )
306 3t3e9 
 |-  ( 3 x. 3 ) = 9
307 306 203 oveq12i 
 |-  ( ( 3 x. 3 ) / ( 2 x. 2 ) ) = ( 9 / 4 )
308 305 307 eqtr2i 
 |-  ( 9 / 4 ) = ( ( 3 / 2 ) x. ( 3 / 2 ) )
309 308 a1i 
 |-  ( ph -> ( 9 / 4 ) = ( ( 3 / 2 ) x. ( 3 / 2 ) ) )
310 304 309 oveq12d 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( 9 / 4 ) ) = ( ( ( 2 / 3 ) x. N ) x. ( ( 3 / 2 ) x. ( 3 / 2 ) ) ) )
311 176 223 224 divcli 
 |-  ( 2 / 3 ) e. CC
312 223 176 177 divcli 
 |-  ( 3 / 2 ) e. CC
313 mul4 
 |-  ( ( ( ( 2 / 3 ) e. CC /\ N e. CC ) /\ ( ( 3 / 2 ) e. CC /\ ( 3 / 2 ) e. CC ) ) -> ( ( ( 2 / 3 ) x. N ) x. ( ( 3 / 2 ) x. ( 3 / 2 ) ) ) = ( ( ( 2 / 3 ) x. ( 3 / 2 ) ) x. ( N x. ( 3 / 2 ) ) ) )
314 312 312 313 mpanr12 
 |-  ( ( ( 2 / 3 ) e. CC /\ N e. CC ) -> ( ( ( 2 / 3 ) x. N ) x. ( ( 3 / 2 ) x. ( 3 / 2 ) ) ) = ( ( ( 2 / 3 ) x. ( 3 / 2 ) ) x. ( N x. ( 3 / 2 ) ) ) )
315 311 192 314 sylancr 
 |-  ( ph -> ( ( ( 2 / 3 ) x. N ) x. ( ( 3 / 2 ) x. ( 3 / 2 ) ) ) = ( ( ( 2 / 3 ) x. ( 3 / 2 ) ) x. ( N x. ( 3 / 2 ) ) ) )
316 divcan6 
 |-  ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( 3 e. CC /\ 3 =/= 0 ) ) -> ( ( 2 / 3 ) x. ( 3 / 2 ) ) = 1 )
317 176 177 223 224 316 mp4an 
 |-  ( ( 2 / 3 ) x. ( 3 / 2 ) ) = 1
318 317 oveq1i 
 |-  ( ( ( 2 / 3 ) x. ( 3 / 2 ) ) x. ( N x. ( 3 / 2 ) ) ) = ( 1 x. ( N x. ( 3 / 2 ) ) )
319 mulcl 
 |-  ( ( N e. CC /\ ( 3 / 2 ) e. CC ) -> ( N x. ( 3 / 2 ) ) e. CC )
320 192 312 319 sylancl 
 |-  ( ph -> ( N x. ( 3 / 2 ) ) e. CC )
321 320 mulid2d 
 |-  ( ph -> ( 1 x. ( N x. ( 3 / 2 ) ) ) = ( N x. ( 3 / 2 ) ) )
322 318 321 syl5eq 
 |-  ( ph -> ( ( ( 2 / 3 ) x. ( 3 / 2 ) ) x. ( N x. ( 3 / 2 ) ) ) = ( N x. ( 3 / 2 ) ) )
323 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
324 div12 
 |-  ( ( N e. CC /\ 3 e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( N x. ( 3 / 2 ) ) = ( 3 x. ( N / 2 ) ) )
325 223 323 324 mp3an23 
 |-  ( N e. CC -> ( N x. ( 3 / 2 ) ) = ( 3 x. ( N / 2 ) ) )
326 192 325 syl 
 |-  ( ph -> ( N x. ( 3 / 2 ) ) = ( 3 x. ( N / 2 ) ) )
327 322 326 eqtrd 
 |-  ( ph -> ( ( ( 2 / 3 ) x. ( 3 / 2 ) ) x. ( N x. ( 3 / 2 ) ) ) = ( 3 x. ( N / 2 ) ) )
328 310 315 327 3eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( 9 / 4 ) ) = ( 3 x. ( N / 2 ) ) )
329 328 83 oveq12d 
 |-  ( ph -> ( ( ( ( 2 x. N ) / 3 ) x. ( 9 / 4 ) ) x. ( G ` ( N / 2 ) ) ) = ( ( 3 x. ( N / 2 ) ) x. ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) ) )
330 76 recni 
 |-  ( 9 / 4 ) e. CC
331 330 a1i 
 |-  ( ph -> ( 9 / 4 ) e. CC )
332 86 recnd 
 |-  ( ph -> ( G ` ( N / 2 ) ) e. CC )
333 214 331 332 mulassd 
 |-  ( ph -> ( ( ( ( 2 x. N ) / 3 ) x. ( 9 / 4 ) ) x. ( G ` ( N / 2 ) ) ) = ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) )
334 223 a1i 
 |-  ( ph -> 3 e. CC )
335 77 rpcnd 
 |-  ( ph -> ( N / 2 ) e. CC )
336 84 recnd 
 |-  ( ph -> ( log ` ( N / 2 ) ) e. CC )
337 77 rpne0d 
 |-  ( ph -> ( N / 2 ) =/= 0 )
338 336 335 337 divcld 
 |-  ( ph -> ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) e. CC )
339 334 335 338 mulassd 
 |-  ( ph -> ( ( 3 x. ( N / 2 ) ) x. ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) ) = ( 3 x. ( ( N / 2 ) x. ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) ) ) )
340 336 335 337 divcan2d 
 |-  ( ph -> ( ( N / 2 ) x. ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) ) = ( log ` ( N / 2 ) ) )
341 340 oveq2d 
 |-  ( ph -> ( 3 x. ( ( N / 2 ) x. ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) ) ) = ( 3 x. ( log ` ( N / 2 ) ) ) )
342 339 341 eqtrd 
 |-  ( ph -> ( ( 3 x. ( N / 2 ) ) x. ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) ) = ( 3 x. ( log ` ( N / 2 ) ) ) )
343 329 333 342 3eqtr3d 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) = ( 3 x. ( log ` ( N / 2 ) ) ) )
344 223 196 mulcli 
 |-  ( 3 x. ( log ` 2 ) ) e. CC
345 344 a1i 
 |-  ( ph -> ( 3 x. ( log ` 2 ) ) e. CC )
346 mulcl 
 |-  ( ( 3 e. CC /\ ( log ` N ) e. CC ) -> ( 3 x. ( log ` N ) ) e. CC )
347 223 168 346 sylancr 
 |-  ( ph -> ( 3 x. ( log ` N ) ) e. CC )
348 267 345 347 npncan3d 
 |-  ( ph -> ( ( ( 5 x. ( log ` 2 ) ) - ( 3 x. ( log ` 2 ) ) ) + ( ( 3 x. ( log ` N ) ) - ( 5 x. ( log ` 2 ) ) ) ) = ( ( 3 x. ( log ` N ) ) - ( 3 x. ( log ` 2 ) ) ) )
349 301 343 348 3eqtr4d 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) = ( ( ( 5 x. ( log ` 2 ) ) - ( 3 x. ( log ` 2 ) ) ) + ( ( 3 x. ( log ` N ) ) - ( 5 x. ( log ` 2 ) ) ) ) )
350 117 92 remulcli 
 |-  ( 2 x. ( log ` 2 ) ) e. RR
351 350 recni 
 |-  ( 2 x. ( log ` 2 ) ) e. CC
352 351 a1i 
 |-  ( ph -> ( 2 x. ( log ` 2 ) ) e. CC )
353 subcl 
 |-  ( ( ( log ` N ) e. CC /\ ( 5 x. ( log ` 2 ) ) e. CC ) -> ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) e. CC )
354 168 266 353 sylancl 
 |-  ( ph -> ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) e. CC )
355 352 283 354 addassd 
 |-  ( ph -> ( ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) + ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) ) = ( ( 2 x. ( log ` 2 ) ) + ( ( 2 x. ( log ` N ) ) + ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) ) ) )
356 294 349 355 3eqtr4d 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) = ( ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) + ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) ) )
357 356 oveq2d 
 |-  ( ph -> ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) = ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) + ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) ) ) )
358 mulcl 
 |-  ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) e. CC /\ ( log ` 2 ) e. CC ) -> ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` 2 ) ) e. CC )
359 251 196 358 sylancl 
 |-  ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` 2 ) ) e. CC )
360 251 168 mulcld 
 |-  ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) e. CC )
361 88 recnd 
 |-  ( ph -> ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) e. CC )
362 214 361 mulcld 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) e. CC )
363 359 360 362 addassd 
 |-  ( ph -> ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` 2 ) ) + ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) = ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` 2 ) ) + ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) ) )
364 256 oveq2d 
 |-  ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) = ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( ( log ` 2 ) + ( log ` N ) ) ) )
365 251 245 168 adddid 
 |-  ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( ( log ` 2 ) + ( log ` N ) ) ) = ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` 2 ) ) + ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) ) )
366 364 365 eqtrd 
 |-  ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) = ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` 2 ) ) + ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) ) )
367 366 oveq1d 
 |-  ( ph -> ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) = ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` 2 ) ) + ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) )
368 58 oveq2d 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( F ` N ) ) = ( ( ( 2 x. N ) / 3 ) x. ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) ) )
369 89 recnd 
 |-  ( ph -> ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) e. CC )
370 97 recnd 
 |-  ( ph -> ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) e. CC )
371 214 369 370 adddid 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) ) = ( ( ( ( 2 x. N ) / 3 ) x. ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) ) )
372 368 371 eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( F ` N ) ) = ( ( ( ( 2 x. N ) / 3 ) x. ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) ) )
373 72 recnd 
 |-  ( ph -> ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) e. CC )
374 214 373 361 adddid 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) = ( ( ( ( 2 x. N ) / 3 ) x. ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) )
375 94 rpge0d 
 |-  ( ph -> 0 <_ ( 2 x. N ) )
376 remsqsqrt 
 |-  ( ( ( 2 x. N ) e. RR /\ 0 <_ ( 2 x. N ) ) -> ( ( sqrt ` ( 2 x. N ) ) x. ( sqrt ` ( 2 x. N ) ) ) = ( 2 x. N ) )
377 237 375 376 syl2anc 
 |-  ( ph -> ( ( sqrt ` ( 2 x. N ) ) x. ( sqrt ` ( 2 x. N ) ) ) = ( 2 x. N ) )
378 377 oveq1d 
 |-  ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) x. ( sqrt ` ( 2 x. N ) ) ) / 3 ) = ( ( 2 x. N ) / 3 ) )
379 113 recnd 
 |-  ( ph -> ( sqrt ` ( 2 x. N ) ) e. CC )
380 224 a1i 
 |-  ( ph -> 3 =/= 0 )
381 379 379 334 380 div23d 
 |-  ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) x. ( sqrt ` ( 2 x. N ) ) ) / 3 ) = ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( sqrt ` ( 2 x. N ) ) ) )
382 378 381 eqtr3d 
 |-  ( ph -> ( ( 2 x. N ) / 3 ) = ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( sqrt ` ( 2 x. N ) ) ) )
383 382 oveq1d 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) ) = ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( sqrt ` ( 2 x. N ) ) ) x. ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) ) )
384 251 379 373 mulassd 
 |-  ( ph -> ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( sqrt ` ( 2 x. N ) ) ) x. ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) ) = ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( ( sqrt ` ( 2 x. N ) ) x. ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) ) ) )
385 0le2 
 |-  0 <_ 2
386 117 385 pm3.2i 
 |-  ( 2 e. RR /\ 0 <_ 2 )
387 60 rprege0d 
 |-  ( ph -> ( N e. RR /\ 0 <_ N ) )
388 sqrtmul 
 |-  ( ( ( 2 e. RR /\ 0 <_ 2 ) /\ ( N e. RR /\ 0 <_ N ) ) -> ( sqrt ` ( 2 x. N ) ) = ( ( sqrt ` 2 ) x. ( sqrt ` N ) ) )
389 386 387 388 sylancr 
 |-  ( ph -> ( sqrt ` ( 2 x. N ) ) = ( ( sqrt ` 2 ) x. ( sqrt ` N ) ) )
390 389 oveq1d 
 |-  ( ph -> ( ( sqrt ` ( 2 x. N ) ) x. ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) ) = ( ( ( sqrt ` 2 ) x. ( sqrt ` N ) ) x. ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) ) )
391 59 recni 
 |-  ( sqrt ` 2 ) e. CC
392 391 a1i 
 |-  ( ph -> ( sqrt ` 2 ) e. CC )
393 61 rpcnd 
 |-  ( ph -> ( sqrt ` N ) e. CC )
394 70 recnd 
 |-  ( ph -> ( G ` ( sqrt ` N ) ) e. CC )
395 392 393 392 394 mul4d 
 |-  ( ph -> ( ( ( sqrt ` 2 ) x. ( sqrt ` N ) ) x. ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) ) = ( ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) x. ( ( sqrt ` N ) x. ( G ` ( sqrt ` N ) ) ) ) )
396 remsqsqrt 
 |-  ( ( 2 e. RR /\ 0 <_ 2 ) -> ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) = 2 )
397 117 385 396 mp2an 
 |-  ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) = 2
398 397 a1i 
 |-  ( ph -> ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) = 2 )
399 67 oveq2d 
 |-  ( ph -> ( ( sqrt ` N ) x. ( G ` ( sqrt ` N ) ) ) = ( ( sqrt ` N ) x. ( ( log ` ( sqrt ` N ) ) / ( sqrt ` N ) ) ) )
400 68 recnd 
 |-  ( ph -> ( log ` ( sqrt ` N ) ) e. CC )
401 61 rpne0d 
 |-  ( ph -> ( sqrt ` N ) =/= 0 )
402 400 393 401 divcan2d 
 |-  ( ph -> ( ( sqrt ` N ) x. ( ( log ` ( sqrt ` N ) ) / ( sqrt ` N ) ) ) = ( log ` ( sqrt ` N ) ) )
403 399 402 eqtrd 
 |-  ( ph -> ( ( sqrt ` N ) x. ( G ` ( sqrt ` N ) ) ) = ( log ` ( sqrt ` N ) ) )
404 398 403 oveq12d 
 |-  ( ph -> ( ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) x. ( ( sqrt ` N ) x. ( G ` ( sqrt ` N ) ) ) ) = ( 2 x. ( log ` ( sqrt ` N ) ) ) )
405 400 2timesd 
 |-  ( ph -> ( 2 x. ( log ` ( sqrt ` N ) ) ) = ( ( log ` ( sqrt ` N ) ) + ( log ` ( sqrt ` N ) ) ) )
406 61 61 relogmuld 
 |-  ( ph -> ( log ` ( ( sqrt ` N ) x. ( sqrt ` N ) ) ) = ( ( log ` ( sqrt ` N ) ) + ( log ` ( sqrt ` N ) ) ) )
407 remsqsqrt 
 |-  ( ( N e. RR /\ 0 <_ N ) -> ( ( sqrt ` N ) x. ( sqrt ` N ) ) = N )
408 387 407 syl 
 |-  ( ph -> ( ( sqrt ` N ) x. ( sqrt ` N ) ) = N )
409 408 fveq2d 
 |-  ( ph -> ( log ` ( ( sqrt ` N ) x. ( sqrt ` N ) ) ) = ( log ` N ) )
410 406 409 eqtr3d 
 |-  ( ph -> ( ( log ` ( sqrt ` N ) ) + ( log ` ( sqrt ` N ) ) ) = ( log ` N ) )
411 404 405 410 3eqtrd 
 |-  ( ph -> ( ( ( sqrt ` 2 ) x. ( sqrt ` 2 ) ) x. ( ( sqrt ` N ) x. ( G ` ( sqrt ` N ) ) ) ) = ( log ` N ) )
412 390 395 411 3eqtrd 
 |-  ( ph -> ( ( sqrt ` ( 2 x. N ) ) x. ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) ) = ( log ` N ) )
413 412 oveq2d 
 |-  ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( ( sqrt ` ( 2 x. N ) ) x. ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) ) ) = ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) )
414 383 384 413 3eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) ) = ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) )
415 414 oveq1d 
 |-  ( ph -> ( ( ( ( 2 x. N ) / 3 ) x. ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) = ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) )
416 374 415 eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) = ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) )
417 382 oveq1d 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) = ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( sqrt ` ( 2 x. N ) ) ) x. ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) )
418 251 379 370 mulassd 
 |-  ( ph -> ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( sqrt ` ( 2 x. N ) ) ) x. ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) = ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( ( sqrt ` ( 2 x. N ) ) x. ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) ) )
419 95 rpne0d 
 |-  ( ph -> ( sqrt ` ( 2 x. N ) ) =/= 0 )
420 245 379 419 divcan2d 
 |-  ( ph -> ( ( sqrt ` ( 2 x. N ) ) x. ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) = ( log ` 2 ) )
421 420 oveq2d 
 |-  ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( ( sqrt ` ( 2 x. N ) ) x. ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) ) = ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` 2 ) ) )
422 417 418 421 3eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) = ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` 2 ) ) )
423 416 422 oveq12d 
 |-  ( ph -> ( ( ( ( 2 x. N ) / 3 ) x. ( ( ( sqrt ` 2 ) x. ( G ` ( sqrt ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( log ` 2 ) / ( sqrt ` ( 2 x. N ) ) ) ) ) = ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) + ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` 2 ) ) ) )
424 360 362 addcld 
 |-  ( ph -> ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) e. CC )
425 424 359 addcomd 
 |-  ( ph -> ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) + ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` 2 ) ) ) = ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` 2 ) ) + ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) ) )
426 372 423 425 3eqtrd 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( F ` N ) ) = ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` 2 ) ) + ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) ) )
427 363 367 426 3eqtr4rd 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( F ` N ) ) = ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) )
428 251 253 mulcld 
 |-  ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) e. CC )
429 addcl 
 |-  ( ( ( 2 x. ( log ` 2 ) ) e. CC /\ ( 2 x. ( log ` N ) ) e. CC ) -> ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) e. CC )
430 351 283 429 sylancr 
 |-  ( ph -> ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) e. CC )
431 428 430 354 addassd 
 |-  ( ph -> ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) + ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) ) + ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) ) = ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) + ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) ) ) )
432 357 427 431 3eqtr4d 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( F ` N ) ) = ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) + ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) ) + ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) ) )
433 270 272 432 3eqtr4rd 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( F ` N ) ) = ( ( ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) - ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) ) )
434 191 250 433 3brtr4d 
 |-  ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( log ` 2 ) ) < ( ( ( 2 x. N ) / 3 ) x. ( F ` N ) ) )
435 100 99 213 ltmul2d 
 |-  ( ph -> ( ( log ` 2 ) < ( F ` N ) <-> ( ( ( 2 x. N ) / 3 ) x. ( log ` 2 ) ) < ( ( ( 2 x. N ) / 3 ) x. ( F ` N ) ) ) )
436 434 435 mpbird 
 |-  ( ph -> ( log ` 2 ) < ( F ` N ) )
437 46 100 99 101 436 lttrd 
 |-  ( ph -> ( F ` ; 6 4 ) < ( F ` N ) )
438 46 99 437 ltnsymd 
 |-  ( ph -> -. ( F ` N ) < ( F ` ; 6 4 ) )
439 43 438 pm2.21dd 
 |-  ( ph -> ps )