MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bposlem9 Unicode version

Theorem bposlem9 20526
Description: Lemma for bpos 20527. Derive a contradiction. (Contributed by Mario Carneiro, 14-Mar-2014.)
Hypotheses
Ref Expression
bposlem7.1  |-  F  =  ( n  e.  NN  |->  ( ( ( ( sqr `  2 )  x.  ( G `  ( sqr `  n ) ) )  +  ( ( 9  /  4
)  x.  ( G `
 ( n  / 
2 ) ) ) )  +  ( ( log `  2 )  /  ( sqr `  (
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
Ref Expression
bposlem9  |-  ( ph  ->  ps )
Distinct variable groups:    n, N    n, G    ph, n    N, p    x, N
Dummy variable  q is distinct from all other variables.
Allowed substitution hints:    ph( x, p)    ps( x, n, p)    F( x, n, p)    G( x, p)

Proof of Theorem bposlem9
StepHypRef Expression
1 bposlem9.4 . . . 4  |-  ( ph  -> ; 6
4  <  N )
2 bposlem7.1 . . . . 5  |-  F  =  ( n  e.  NN  |->  ( ( ( ( sqr `  2 )  x.  ( G `  ( sqr `  n ) ) )  +  ( ( 9  /  4
)  x.  ( G `
 ( n  / 
2 ) ) ) )  +  ( ( log `  2 )  /  ( sqr `  (
2  x.  n ) ) ) ) )
3 bposlem7.2 . . . . 5  |-  G  =  ( x  e.  RR+  |->  ( ( log `  x
)  /  x ) )
4 6nn0 9982 . . . . . . 7  |-  6  e.  NN0
5 4nn 9875 . . . . . . 7  |-  4  e.  NN
64, 5decnncl 10133 . . . . . 6  |- ; 6 4  e.  NN
76a1i 12 . . . . 5  |-  ( ph  -> ; 6
4  e.  NN )
8 bposlem9.3 . . . . 5  |-  ( ph  ->  N  e.  NN )
9 ere 12365 . . . . . . . . 9  |-  _e  e.  RR
10 8re 9820 . . . . . . . . 9  |-  8  e.  RR
11 egt2lt3 12479 . . . . . . . . . . 11  |-  ( 2  <  _e  /\  _e  <  3 )
1211simpri 450 . . . . . . . . . 10  |-  _e  <  3
13 3lt8 9907 . . . . . . . . . 10  |-  3  <  8
14 3re 9813 . . . . . . . . . . 11  |-  3  e.  RR
159, 14, 10lttri 8941 . . . . . . . . . 10  |-  ( ( _e  <  3  /\  3  <  8 )  ->  _e  <  8
)
1612, 13, 15mp2an 655 . . . . . . . . 9  |-  _e  <  8
179, 10, 16ltleii 8937 . . . . . . . 8  |-  _e  <_  8
18 0re 8834 . . . . . . . . . 10  |-  0  e.  RR
19 epos 12480 . . . . . . . . . 10  |-  0  <  _e
2018, 9, 19ltleii 8937 . . . . . . . . 9  |-  0  <_  _e
21 8pos 9832 . . . . . . . . . 10  |-  0  <  8
2218, 10, 21ltleii 8937 . . . . . . . . 9  |-  0  <_  8
23 le2sq 11173 . . . . . . . . 9  |-  ( ( ( _e  e.  RR  /\  0  <_  _e )  /\  ( 8  e.  RR  /\  0  <_  8 ) )  ->  ( _e  <_  8  <->  ( _e ^
2 )  <_  (
8 ^ 2 ) ) )
249, 20, 10, 22, 23mp4an 656 . . . . . . . 8  |-  ( _e 
<_  8  <->  ( _e ^
2 )  <_  (
8 ^ 2 ) )
2517, 24mpbi 201 . . . . . . 7  |-  ( _e
^ 2 )  <_ 
( 8 ^ 2 )
2610recni 8845 . . . . . . . . 9  |-  8  e.  CC
2726sqvali 11178 . . . . . . . 8  |-  ( 8 ^ 2 )  =  ( 8  x.  8 )
28 8t8e64 10214 . . . . . . . 8  |-  ( 8  x.  8 )  = ; 6
4
2927, 28eqtri 2305 . . . . . . 7  |-  ( 8 ^ 2 )  = ; 6
4
3025, 29breqtri 4048 . . . . . 6  |-  ( _e
^ 2 )  <_ ; 6 4
3130a1i 12 . . . . 5  |-  ( ph  ->  ( _e ^ 2 )  <_ ; 6 4 )
329resqcli 11184 . . . . . . 7  |-  ( _e
^ 2 )  e.  RR
3332a1i 12 . . . . . 6  |-  ( ph  ->  ( _e ^ 2 )  e.  RR )
346nnrei 9751 . . . . . . 7  |- ; 6 4  e.  RR
3534a1i 12 . . . . . 6  |-  ( ph  -> ; 6
4  e.  RR )
368nnred 9757 . . . . . 6  |-  ( ph  ->  N  e.  RR )
37 ltle 8906 . . . . . . . 8  |-  ( (; 6
4  e.  RR  /\  N  e.  RR )  ->  (; 6 4  <  N  -> ; 6
4  <_  N )
)
3834, 36, 37sylancr 646 . . . . . . 7  |-  ( ph  ->  (; 6 4  <  N  -> ; 6
4  <_  N )
)
391, 38mpd 16 . . . . . 6  |-  ( ph  -> ; 6
4  <_  N )
4033, 35, 36, 31, 39letrd 8969 . . . . 5  |-  ( ph  ->  ( _e ^ 2 )  <_  N )
412, 3, 7, 8, 31, 40bposlem7 20524 . . . 4  |-  ( ph  ->  (; 6 4  <  N  ->  ( F `  N
)  <  ( F ` ; 6 4 ) ) )
421, 41mpd 16 . . 3  |-  ( ph  ->  ( F `  N
)  <  ( F ` ; 6 4 ) )
432, 3bposlem8 20525 . . . . . 6  |-  ( ( F ` ; 6 4 )  e.  RR  /\  ( F `
; 6 4 )  < 
( log `  2
) )
4443a1i 12 . . . . 5  |-  ( ph  ->  ( ( F ` ; 6 4 )  e.  RR  /\  ( F ` ; 6 4 )  < 
( log `  2
) ) )
4544simpld 447 . . . 4  |-  ( ph  ->  ( F ` ; 6 4 )  e.  RR )
46 fveq2 5486 . . . . . . . . . . 11  |-  ( n  =  N  ->  ( sqr `  n )  =  ( sqr `  N
) )
4746fveq2d 5490 . . . . . . . . . 10  |-  ( n  =  N  ->  ( G `  ( sqr `  n ) )  =  ( G `  ( sqr `  N ) ) )
4847oveq2d 5836 . . . . . . . . 9  |-  ( n  =  N  ->  (
( sqr `  2
)  x.  ( G `
 ( sqr `  n
) ) )  =  ( ( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) ) )
49 oveq1 5827 . . . . . . . . . . 11  |-  ( n  =  N  ->  (
n  /  2 )  =  ( N  / 
2 ) )
5049fveq2d 5490 . . . . . . . . . 10  |-  ( n  =  N  ->  ( G `  ( n  /  2 ) )  =  ( G `  ( N  /  2
) ) )
5150oveq2d 5836 . . . . . . . . 9  |-  ( n  =  N  ->  (
( 9  /  4
)  x.  ( G `
 ( n  / 
2 ) ) )  =  ( ( 9  /  4 )  x.  ( G `  ( N  /  2 ) ) ) )
5248, 51oveq12d 5838 . . . . . . . 8  |-  ( n  =  N  ->  (
( ( sqr `  2
)  x.  ( G `
 ( sqr `  n
) ) )  +  ( ( 9  / 
4 )  x.  ( G `  ( n  /  2 ) ) ) )  =  ( ( ( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) )  +  ( ( 9  / 
4 )  x.  ( G `  ( N  /  2 ) ) ) ) )
53 oveq2 5828 . . . . . . . . . 10  |-  ( n  =  N  ->  (
2  x.  n )  =  ( 2  x.  N ) )
5453fveq2d 5490 . . . . . . . . 9  |-  ( n  =  N  ->  ( sqr `  ( 2  x.  n ) )  =  ( sqr `  (
2  x.  N ) ) )
5554oveq2d 5836 . . . . . . . 8  |-  ( n  =  N  ->  (
( log `  2
)  /  ( sqr `  ( 2  x.  n
) ) )  =  ( ( log `  2
)  /  ( sqr `  ( 2  x.  N
) ) ) )
5652, 55oveq12d 5838 . . . . . . 7  |-  ( n  =  N  ->  (
( ( ( sqr `  2 )  x.  ( G `  ( sqr `  n ) ) )  +  ( ( 9  /  4 )  x.  ( G `  ( n  /  2
) ) ) )  +  ( ( log `  2 )  / 
( sqr `  (
2  x.  n ) ) ) )  =  ( ( ( ( sqr `  2 )  x.  ( G `  ( sqr `  N ) ) )  +  ( ( 9  /  4
)  x.  ( G `
 ( N  / 
2 ) ) ) )  +  ( ( log `  2 )  /  ( sqr `  (
2  x.  N ) ) ) ) )
57 ovex 5845 . . . . . . 7  |-  ( ( ( ( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) )  +  ( ( 9  / 
4 )  x.  ( G `  ( N  /  2 ) ) ) )  +  ( ( log `  2
)  /  ( sqr `  ( 2  x.  N
) ) ) )  e.  _V
5856, 2, 57fvmpt 5564 . . . . . 6  |-  ( N  e.  NN  ->  ( F `  N )  =  ( ( ( ( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) )  +  ( ( 9  / 
4 )  x.  ( G `  ( N  /  2 ) ) ) )  +  ( ( log `  2
)  /  ( sqr `  ( 2  x.  N
) ) ) ) )
598, 58syl 17 . . . . 5  |-  ( ph  ->  ( F `  N
)  =  ( ( ( ( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) )  +  ( ( 9  / 
4 )  x.  ( G `  ( N  /  2 ) ) ) )  +  ( ( log `  2
)  /  ( sqr `  ( 2  x.  N
) ) ) ) )
60 sqr2re 12523 . . . . . . . 8  |-  ( sqr `  2 )  e.  RR
618nnrpd 10385 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  RR+ )
6261rpsqrcld 11889 . . . . . . . . . 10  |-  ( ph  ->  ( sqr `  N
)  e.  RR+ )
63 fveq2 5486 . . . . . . . . . . . 12  |-  ( x  =  ( sqr `  N
)  ->  ( log `  x )  =  ( log `  ( sqr `  N ) ) )
64 id 21 . . . . . . . . . . . 12  |-  ( x  =  ( sqr `  N
)  ->  x  =  ( sqr `  N ) )
6563, 64oveq12d 5838 . . . . . . . . . . 11  |-  ( x  =  ( sqr `  N
)  ->  ( ( log `  x )  /  x )  =  ( ( log `  ( sqr `  N ) )  /  ( sqr `  N
) ) )
66 ovex 5845 . . . . . . . . . . 11  |-  ( ( log `  ( sqr `  N ) )  / 
( sqr `  N
) )  e.  _V
6765, 3, 66fvmpt 5564 . . . . . . . . . 10  |-  ( ( sqr `  N )  e.  RR+  ->  ( G `
 ( sqr `  N
) )  =  ( ( log `  ( sqr `  N ) )  /  ( sqr `  N
) ) )
6862, 67syl 17 . . . . . . . . 9  |-  ( ph  ->  ( G `  ( sqr `  N ) )  =  ( ( log `  ( sqr `  N
) )  /  ( sqr `  N ) ) )
6962relogcld 19969 . . . . . . . . . 10  |-  ( ph  ->  ( log `  ( sqr `  N ) )  e.  RR )
7069, 62rerpdivcld 10413 . . . . . . . . 9  |-  ( ph  ->  ( ( log `  ( sqr `  N ) )  /  ( sqr `  N
) )  e.  RR )
7168, 70eqeltrd 2359 . . . . . . . 8  |-  ( ph  ->  ( G `  ( sqr `  N ) )  e.  RR )
72 remulcl 8818 . . . . . . . 8  |-  ( ( ( sqr `  2
)  e.  RR  /\  ( G `  ( sqr `  N ) )  e.  RR )  ->  (
( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) )  e.  RR )
7360, 71, 72sylancr 646 . . . . . . 7  |-  ( ph  ->  ( ( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) )  e.  RR )
74 9re 9821 . . . . . . . . 9  |-  9  e.  RR
75 4re 9815 . . . . . . . . 9  |-  4  e.  RR
765nnne0i 9776 . . . . . . . . 9  |-  4  =/=  0
7774, 75, 76redivcli 9523 . . . . . . . 8  |-  ( 9  /  4 )  e.  RR
7861rphalfcld 10398 . . . . . . . . . 10  |-  ( ph  ->  ( N  /  2
)  e.  RR+ )
79 fveq2 5486 . . . . . . . . . . . 12  |-  ( x  =  ( N  / 
2 )  ->  ( log `  x )  =  ( log `  ( N  /  2 ) ) )
80 id 21 . . . . . . . . . . . 12  |-  ( x  =  ( N  / 
2 )  ->  x  =  ( N  / 
2 ) )
8179, 80oveq12d 5838 . . . . . . . . . . 11  |-  ( x  =  ( N  / 
2 )  ->  (
( log `  x
)  /  x )  =  ( ( log `  ( N  /  2
) )  /  ( N  /  2 ) ) )
82 ovex 5845 . . . . . . . . . . 11  |-  ( ( log `  ( N  /  2 ) )  /  ( N  / 
2 ) )  e. 
_V
8381, 3, 82fvmpt 5564 . . . . . . . . . 10  |-  ( ( N  /  2 )  e.  RR+  ->  ( G `
 ( N  / 
2 ) )  =  ( ( log `  ( N  /  2 ) )  /  ( N  / 
2 ) ) )
8478, 83syl 17 . . . . . . . . 9  |-  ( ph  ->  ( G `  ( N  /  2 ) )  =  ( ( log `  ( N  /  2
) )  /  ( N  /  2 ) ) )
8578relogcld 19969 . . . . . . . . . 10  |-  ( ph  ->  ( log `  ( N  /  2 ) )  e.  RR )
8685, 78rerpdivcld 10413 . . . . . . . . 9  |-  ( ph  ->  ( ( log `  ( N  /  2 ) )  /  ( N  / 
2 ) )  e.  RR )
8784, 86eqeltrd 2359 . . . . . . . 8  |-  ( ph  ->  ( G `  ( N  /  2 ) )  e.  RR )
88 remulcl 8818 . . . . . . . 8  |-  ( ( ( 9  /  4
)  e.  RR  /\  ( G `  ( N  /  2 ) )  e.  RR )  -> 
( ( 9  / 
4 )  x.  ( G `  ( N  /  2 ) ) )  e.  RR )
8977, 87, 88sylancr 646 . . . . . . 7  |-  ( ph  ->  ( ( 9  / 
4 )  x.  ( G `  ( N  /  2 ) ) )  e.  RR )
9073, 89readdcld 8858 . . . . . 6  |-  ( ph  ->  ( ( ( sqr `  2 )  x.  ( G `  ( sqr `  N ) ) )  +  ( ( 9  /  4 )  x.  ( G `  ( N  /  2
) ) ) )  e.  RR )
91 2rp 10355 . . . . . . . 8  |-  2  e.  RR+
92 relogcl 19927 . . . . . . . 8  |-  ( 2  e.  RR+  ->  ( log `  2 )  e.  RR )
9391, 92ax-mp 10 . . . . . . 7  |-  ( log `  2 )  e.  RR
94 rpmulcl 10371 . . . . . . . . 9  |-  ( ( 2  e.  RR+  /\  N  e.  RR+ )  ->  (
2  x.  N )  e.  RR+ )
9591, 61, 94sylancr 646 . . . . . . . 8  |-  ( ph  ->  ( 2  x.  N
)  e.  RR+ )
9695rpsqrcld 11889 . . . . . . 7  |-  ( ph  ->  ( sqr `  (
2  x.  N ) )  e.  RR+ )
97 rerpdivcl 10377 . . . . . . 7  |-  ( ( ( log `  2
)  e.  RR  /\  ( sqr `  ( 2  x.  N ) )  e.  RR+ )  ->  (
( log `  2
)  /  ( sqr `  ( 2  x.  N
) ) )  e.  RR )
9893, 96, 97sylancr 646 . . . . . 6  |-  ( ph  ->  ( ( log `  2
)  /  ( sqr `  ( 2  x.  N
) ) )  e.  RR )
9990, 98readdcld 8858 . . . . 5  |-  ( ph  ->  ( ( ( ( sqr `  2 )  x.  ( G `  ( sqr `  N ) ) )  +  ( ( 9  /  4
)  x.  ( G `
 ( N  / 
2 ) ) ) )  +  ( ( log `  2 )  /  ( sqr `  (
2  x.  N ) ) ) )  e.  RR )
10059, 99eqeltrd 2359 . . . 4  |-  ( ph  ->  ( F `  N
)  e.  RR )
10193a1i 12 . . . . 5  |-  ( ph  ->  ( log `  2
)  e.  RR )
10244simprd 451 . . . . 5  |-  ( ph  ->  ( F ` ; 6 4 )  < 
( log `  2
) )
103 nnrp 10359 . . . . . . . . . . . 12  |-  ( 4  e.  NN  ->  4  e.  RR+ )
1045, 103ax-mp 10 . . . . . . . . . . 11  |-  4  e.  RR+
105 relogcl 19927 . . . . . . . . . . 11  |-  ( 4  e.  RR+  ->  ( log `  4 )  e.  RR )
106104, 105ax-mp 10 . . . . . . . . . 10  |-  ( log `  4 )  e.  RR
107 remulcl 8818 . . . . . . . . . 10  |-  ( ( N  e.  RR  /\  ( log `  4 )  e.  RR )  -> 
( N  x.  ( log `  4 ) )  e.  RR )
10836, 106, 107sylancl 645 . . . . . . . . 9  |-  ( ph  ->  ( N  x.  ( log `  4 ) )  e.  RR )
10961relogcld 19969 . . . . . . . . 9  |-  ( ph  ->  ( log `  N
)  e.  RR )
110108, 109resubcld 9207 . . . . . . . 8  |-  ( ph  ->  ( ( N  x.  ( log `  4 ) )  -  ( log `  N ) )  e.  RR )
111 rpre 10356 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  N )  e.  RR+  ->  ( 2  x.  N )  e.  RR )
112 rpge0 10362 . . . . . . . . . . . . . 14  |-  ( ( 2  x.  N )  e.  RR+  ->  0  <_ 
( 2  x.  N
) )
113111, 112resqrcld 11895 . . . . . . . . . . . . 13  |-  ( ( 2  x.  N )  e.  RR+  ->  ( sqr `  ( 2  x.  N
) )  e.  RR )
11495, 113syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( sqr `  (
2  x.  N ) )  e.  RR )
115 3nn 9874 . . . . . . . . . . . 12  |-  3  e.  NN
116 nndivre 9777 . . . . . . . . . . . 12  |-  ( ( ( sqr `  (
2  x.  N ) )  e.  RR  /\  3  e.  NN )  ->  ( ( sqr `  (
2  x.  N ) )  /  3 )  e.  RR )
117114, 115, 116sylancl 645 . . . . . . . . . . 11  |-  ( ph  ->  ( ( sqr `  (
2  x.  N ) )  /  3 )  e.  RR )
118 2re 9811 . . . . . . . . . . 11  |-  2  e.  RR
119 readdcl 8816 . . . . . . . . . . 11  |-  ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  e.  RR  /\  2  e.  RR )  ->  (
( ( sqr `  (
2  x.  N ) )  /  3 )  +  2 )  e.  RR )
120117, 118, 119sylancl 645 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  +  2 )  e.  RR )
12195relogcld 19969 . . . . . . . . . 10  |-  ( ph  ->  ( log `  (
2  x.  N ) )  e.  RR )
122120, 121remulcld 8859 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 )  x.  ( log `  ( 2  x.  N ) ) )  e.  RR )
123 remulcl 8818 . . . . . . . . . . . . 13  |-  ( ( 4  e.  RR  /\  N  e.  RR )  ->  ( 4  x.  N
)  e.  RR )
12475, 36, 123sylancr 646 . . . . . . . . . . . 12  |-  ( ph  ->  ( 4  x.  N
)  e.  RR )
125 nndivre 9777 . . . . . . . . . . . 12  |-  ( ( ( 4  x.  N
)  e.  RR  /\  3  e.  NN )  ->  ( ( 4  x.  N )  /  3
)  e.  RR )
126124, 115, 125sylancl 645 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 4  x.  N )  /  3
)  e.  RR )
127 5re 9817 . . . . . . . . . . 11  |-  5  e.  RR
128 resubcl 9107 . . . . . . . . . . 11  |-  ( ( ( ( 4  x.  N )  /  3
)  e.  RR  /\  5  e.  RR )  ->  ( ( ( 4  x.  N )  / 
3 )  -  5 )  e.  RR )
129126, 127, 128sylancl 645 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( 4  x.  N )  / 
3 )  -  5 )  e.  RR )
130 remulcl 8818 . . . . . . . . . 10  |-  ( ( ( ( ( 4  x.  N )  / 
3 )  -  5 )  e.  RR  /\  ( log `  2 )  e.  RR )  -> 
( ( ( ( 4  x.  N )  /  3 )  - 
5 )  x.  ( log `  2 ) )  e.  RR )
131129, 93, 130sylancl 645 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( 4  x.  N )  /  3 )  - 
5 )  x.  ( log `  2 ) )  e.  RR )
132122, 131readdcld 8858 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  +  2 )  x.  ( log `  (
2  x.  N ) ) )  +  ( ( ( ( 4  x.  N )  / 
3 )  -  5 )  x.  ( log `  2 ) ) )  e.  RR )
133 remulcl 8818 . . . . . . . . . 10  |-  ( ( ( ( 4  x.  N )  /  3
)  e.  RR  /\  ( log `  2 )  e.  RR )  -> 
( ( ( 4  x.  N )  / 
3 )  x.  ( log `  2 ) )  e.  RR )
134126, 93, 133sylancl 645 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 4  x.  N )  / 
3 )  x.  ( log `  2 ) )  e.  RR )
135134, 109resubcld 9207 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( 4  x.  N )  /  3 )  x.  ( log `  2
) )  -  ( log `  N ) )  e.  RR )
1368nnzd 10112 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ZZ )
137 df-5 9803 . . . . . . . . . . . . 13  |-  5  =  ( 4  +  1 )
13875a1i 12 . . . . . . . . . . . . . . 15  |-  ( ph  ->  4  e.  RR )
139 6nn 9877 . . . . . . . . . . . . . . . . 17  |-  6  e.  NN
140 4nn0 9980 . . . . . . . . . . . . . . . . 17  |-  4  e.  NN0
141 4lt10 9923 . . . . . . . . . . . . . . . . 17  |-  4  <  10
142139, 140, 140, 141declti 10145 . . . . . . . . . . . . . . . 16  |-  4  < ; 6
4
143142a1i 12 . . . . . . . . . . . . . . 15  |-  ( ph  ->  4  < ; 6 4 )
144138, 35, 36, 143, 1lttrd 8973 . . . . . . . . . . . . . 14  |-  ( ph  ->  4  <  N )
1455nnzi 10043 . . . . . . . . . . . . . . 15  |-  4  e.  ZZ
146 zltp1le 10063 . . . . . . . . . . . . . . 15  |-  ( ( 4  e.  ZZ  /\  N  e.  ZZ )  ->  ( 4  <  N  <->  ( 4  +  1 )  <_  N ) )
147145, 136, 146sylancr 646 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 4  <  N  <->  ( 4  +  1 )  <_  N ) )
148144, 147mpbid 203 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 4  +  1 )  <_  N )
149137, 148syl5eqbr 4058 . . . . . . . . . . . 12  |-  ( ph  ->  5  <_  N )
150 5nn 9876 . . . . . . . . . . . . . 14  |-  5  e.  NN
151150nnzi 10043 . . . . . . . . . . . . 13  |-  5  e.  ZZ
152151eluz1i 10233 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  5
)  <->  ( N  e.  ZZ  /\  5  <_  N ) )
153136, 149, 152sylanbrc 647 . . . . . . . . . . 11  |-  ( ph  ->  N  e.  ( ZZ>= ` 
5 ) )
154 bposlem9.5 . . . . . . . . . . . 12  |-  ( ph  ->  -.  E. p  e. 
Prime  ( N  <  p  /\  p  <_  ( 2  x.  N ) ) )
155 breq2 4029 . . . . . . . . . . . . . 14  |-  ( p  =  q  ->  ( N  <  p  <->  N  <  q ) )
156 breq1 4028 . . . . . . . . . . . . . 14  |-  ( p  =  q  ->  (
p  <_  ( 2  x.  N )  <->  q  <_  ( 2  x.  N ) ) )
157155, 156anbi12d 693 . . . . . . . . . . . . 13  |-  ( p  =  q  ->  (
( N  <  p  /\  p  <_  ( 2  x.  N ) )  <-> 
( N  <  q  /\  q  <_  ( 2  x.  N ) ) ) )
158157cbvrexv 2767 . . . . . . . . . . . 12  |-  ( E. p  e.  Prime  ( N  <  p  /\  p  <_  ( 2  x.  N
) )  <->  E. q  e.  Prime  ( N  < 
q  /\  q  <_  ( 2  x.  N ) ) )
159154, 158sylnib 297 . . . . . . . . . . 11  |-  ( ph  ->  -.  E. q  e. 
Prime  ( N  <  q  /\  q  <_  ( 2  x.  N ) ) )
160 eqid 2285 . . . . . . . . . . 11  |-  ( 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 ) )
161 eqid 2285 . . . . . . . . . . 11  |-  ( |_
`  ( ( 2  x.  N )  / 
3 ) )  =  ( |_ `  (
( 2  x.  N
)  /  3 ) )
162 eqid 2285 . . . . . . . . . . 11  |-  ( |_
`  ( sqr `  (
2  x.  N ) ) )  =  ( |_ `  ( sqr `  ( 2  x.  N
) ) )
163153, 159, 160, 161, 162bposlem6 20523 . . . . . . . . . 10  |-  ( ph  ->  ( ( 4 ^ N )  /  N
)  <  ( (
( 2  x.  N
)  ^ c  ( ( ( sqr `  (
2  x.  N ) )  /  3 )  +  2 ) )  x.  ( 2  ^ c  ( ( ( 4  x.  N )  /  3 )  - 
5 ) ) ) )
164 reexplog 19943 . . . . . . . . . . . . 13  |-  ( ( 4  e.  RR+  /\  N  e.  ZZ )  ->  (
4 ^ N )  =  ( exp `  ( N  x.  ( log `  4 ) ) ) )
165104, 136, 164sylancr 646 . . . . . . . . . . . 12  |-  ( ph  ->  ( 4 ^ N
)  =  ( exp `  ( N  x.  ( log `  4 ) ) ) )
16661reeflogd 19970 . . . . . . . . . . . . 13  |-  ( ph  ->  ( exp `  ( log `  N ) )  =  N )
167166eqcomd 2290 . . . . . . . . . . . 12  |-  ( ph  ->  N  =  ( exp `  ( log `  N
) ) )
168165, 167oveq12d 5838 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 4 ^ N )  /  N
)  =  ( ( exp `  ( N  x.  ( log `  4
) ) )  / 
( exp `  ( log `  N ) ) ) )
169108recnd 8857 . . . . . . . . . . . 12  |-  ( ph  ->  ( N  x.  ( log `  4 ) )  e.  CC )
170109recnd 8857 . . . . . . . . . . . 12  |-  ( ph  ->  ( log `  N
)  e.  CC )
171 efsub 12375 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) )
172169, 170, 171syl2anc 644 . . . . . . . . . . 11  |-  ( ph  ->  ( exp `  (
( N  x.  ( log `  4 ) )  -  ( log `  N
) ) )  =  ( ( exp `  ( N  x.  ( log `  4 ) ) )  /  ( exp `  ( log `  N ) ) ) )
173168, 172eqtr4d 2320 . . . . . . . . . 10  |-  ( ph  ->  ( ( 4 ^ N )  /  N
)  =  ( exp `  ( ( N  x.  ( log `  4 ) )  -  ( log `  N ) ) ) )
17495rpcnd 10388 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2  x.  N
)  e.  CC )
17595rpne0d 10391 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2  x.  N
)  =/=  0 )
176120recnd 8857 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  +  2 )  e.  CC )
177174, 175, 176cxpefd 20054 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 2  x.  N )  ^ c 
( ( ( sqr `  ( 2  x.  N
) )  /  3
)  +  2 ) )  =  ( exp `  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 )  x.  ( log `  ( 2  x.  N ) ) ) ) )
178129recnd 8857 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 4  x.  N )  / 
3 )  -  5 )  e.  CC )
179 2cn 9812 . . . . . . . . . . . . . 14  |-  2  e.  CC
180 2ne0 9825 . . . . . . . . . . . . . 14  |-  2  =/=  0
181 cxpef 20007 . . . . . . . . . . . . . 14  |-  ( ( 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
) ) ) )
182179, 180, 181mp3an12 1269 . . . . . . . . . . . . 13  |-  ( ( ( ( 4  x.  N )  /  3
)  -  5 )  e.  CC  ->  (
2  ^ c  ( ( ( 4  x.  N )  /  3
)  -  5 ) )  =  ( exp `  ( ( ( ( 4  x.  N )  /  3 )  - 
5 )  x.  ( log `  2 ) ) ) )
183178, 182syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2  ^ c 
( ( ( 4  x.  N )  / 
3 )  -  5 ) )  =  ( exp `  ( ( ( ( 4  x.  N )  /  3
)  -  5 )  x.  ( log `  2
) ) ) )
184177, 183oveq12d 5838 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( 2  x.  N )  ^ c  ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 ) )  x.  ( 2  ^ c 
( ( ( 4  x.  N )  / 
3 )  -  5 ) ) )  =  ( ( exp `  (
( ( ( sqr `  ( 2  x.  N
) )  /  3
)  +  2 )  x.  ( log `  (
2  x.  N ) ) ) )  x.  ( exp `  (
( ( ( 4  x.  N )  / 
3 )  -  5 )  x.  ( log `  2 ) ) ) ) )
185122recnd 8857 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 )  x.  ( log `  ( 2  x.  N ) ) )  e.  CC )
186131recnd 8857 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( 4  x.  N )  /  3 )  - 
5 )  x.  ( log `  2 ) )  e.  CC )
187 efadd 12370 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 )  x.  ( log `  ( 2  x.  N ) ) )  e.  CC  /\  (
( ( ( 4  x.  N )  / 
3 )  -  5 )  x.  ( log `  2 ) )  e.  CC )  -> 
( exp `  (
( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 )  x.  ( log `  ( 2  x.  N ) ) )  +  ( ( ( ( 4  x.  N
)  /  3 )  -  5 )  x.  ( log `  2
) ) ) )  =  ( ( exp `  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 )  x.  ( log `  ( 2  x.  N ) ) ) )  x.  ( exp `  ( ( ( ( 4  x.  N )  /  3 )  - 
5 )  x.  ( log `  2 ) ) ) ) )
188185, 186, 187syl2anc 644 . . . . . . . . . . 11  |-  ( ph  ->  ( exp `  (
( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 )  x.  ( log `  ( 2  x.  N ) ) )  +  ( ( ( ( 4  x.  N
)  /  3 )  -  5 )  x.  ( log `  2
) ) ) )  =  ( ( exp `  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 )  x.  ( log `  ( 2  x.  N ) ) ) )  x.  ( exp `  ( ( ( ( 4  x.  N )  /  3 )  - 
5 )  x.  ( log `  2 ) ) ) ) )
189184, 188eqtr4d 2320 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( 2  x.  N )  ^ c  ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 ) )  x.  ( 2  ^ c 
( ( ( 4  x.  N )  / 
3 )  -  5 ) ) )  =  ( exp `  (
( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 )  x.  ( log `  ( 2  x.  N ) ) )  +  ( ( ( ( 4  x.  N
)  /  3 )  -  5 )  x.  ( log `  2
) ) ) ) )
190163, 173, 1893brtr3d 4054 . . . . . . . . 9  |-  ( ph  ->  ( exp `  (
( N  x.  ( log `  4 ) )  -  ( log `  N
) ) )  < 
( exp `  (
( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 )  x.  ( log `  ( 2  x.  N ) ) )  +  ( ( ( ( 4  x.  N
)  /  3 )  -  5 )  x.  ( log `  2
) ) ) ) )
191 eflt 12392 . . . . . . . . . 10  |-  ( ( ( ( N  x.  ( log `  4 ) )  -  ( log `  N ) )  e.  RR  /\  ( ( ( ( ( sqr `  ( 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
) )  <  (
( ( ( ( sqr `  ( 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 `  (
( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 )  x.  ( log `  ( 2  x.  N ) ) )  +  ( ( ( ( 4  x.  N
)  /  3 )  -  5 )  x.  ( log `  2
) ) ) ) ) )
192110, 132, 191syl2anc 644 . . . . . . . . 9  |-  ( ph  ->  ( ( ( N  x.  ( log `  4
) )  -  ( log `  N ) )  <  ( ( ( ( ( sqr `  (
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 `  (
( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 )  x.  ( log `  ( 2  x.  N ) ) )  +  ( ( ( ( 4  x.  N
)  /  3 )  -  5 )  x.  ( log `  2
) ) ) ) ) )
193190, 192mpbird 225 . . . . . . . 8  |-  ( ph  ->  ( ( N  x.  ( log `  4 ) )  -  ( log `  N ) )  < 
( ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  +  2 )  x.  ( log `  (
2  x.  N ) ) )  +  ( ( ( ( 4  x.  N )  / 
3 )  -  5 )  x.  ( log `  2 ) ) ) )
194110, 132, 135, 193ltsub1dd 9380 . . . . . . 7  |-  ( ph  ->  ( ( ( N  x.  ( log `  4
) )  -  ( log `  N ) )  -  ( ( ( ( 4  x.  N
)  /  3 )  x.  ( log `  2
) )  -  ( log `  N ) ) )  <  ( ( ( ( ( ( sqr `  ( 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 ) ) ) )
19536recnd 8857 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  CC )
196 mulcom 8819 . . . . . . . . . . . 12  |-  ( ( 2  e.  CC  /\  N  e.  CC )  ->  ( 2  x.  N
)  =  ( N  x.  2 ) )
197179, 195, 196sylancr 646 . . . . . . . . . . 11  |-  ( ph  ->  ( 2  x.  N
)  =  ( N  x.  2 ) )
198197oveq1d 5835 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2  x.  N )  x.  ( log `  2 ) )  =  ( ( N  x.  2 )  x.  ( log `  2
) ) )
19993recni 8845 . . . . . . . . . . . . 13  |-  ( log `  2 )  e.  CC
200 mulass 8821 . . . . . . . . . . . . 13  |-  ( ( N  e.  CC  /\  2  e.  CC  /\  ( log `  2 )  e.  CC )  ->  (
( N  x.  2 )  x.  ( log `  2 ) )  =  ( N  x.  ( 2  x.  ( log `  2 ) ) ) )
201179, 199, 200mp3an23 1271 . . . . . . . . . . . 12  |-  ( N  e.  CC  ->  (
( N  x.  2 )  x.  ( log `  2 ) )  =  ( N  x.  ( 2  x.  ( log `  2 ) ) ) )
202195, 201syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( ( N  x.  2 )  x.  ( log `  2 ) )  =  ( N  x.  ( 2  x.  ( log `  2 ) ) ) )
2031992timesi 9841 . . . . . . . . . . . . 13  |-  ( 2  x.  ( log `  2
) )  =  ( ( log `  2
)  +  ( log `  2 ) )
204 relogmul 19940 . . . . . . . . . . . . . 14  |-  ( ( 2  e.  RR+  /\  2  e.  RR+ )  ->  ( log `  ( 2  x.  2 ) )  =  ( ( log `  2
)  +  ( log `  2 ) ) )
20591, 91, 204mp2an 655 . . . . . . . . . . . . 13  |-  ( log `  ( 2  x.  2 ) )  =  ( ( log `  2
)  +  ( log `  2 ) )
206 2t2e4 9867 . . . . . . . . . . . . . 14  |-  ( 2  x.  2 )  =  4
207206fveq2i 5489 . . . . . . . . . . . . 13  |-  ( log `  ( 2  x.  2 ) )  =  ( log `  4 )
208203, 205, 2073eqtr2i 2311 . . . . . . . . . . . 12  |-  ( 2  x.  ( log `  2
) )  =  ( log `  4 )
209208oveq2i 5831 . . . . . . . . . . 11  |-  ( N  x.  ( 2  x.  ( log `  2
) ) )  =  ( N  x.  ( log `  4 ) )
210202, 209syl6eq 2333 . . . . . . . . . 10  |-  ( ph  ->  ( ( N  x.  2 )  x.  ( log `  2 ) )  =  ( N  x.  ( log `  4 ) ) )
211198, 210eqtrd 2317 . . . . . . . . 9  |-  ( ph  ->  ( ( 2  x.  N )  x.  ( log `  2 ) )  =  ( N  x.  ( log `  4 ) ) )
212211oveq1d 5835 . . . . . . . 8  |-  ( 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
) ) ) )
213 4p2e6 9853 . . . . . . . . . . . . . . . 16  |-  ( 4  +  2 )  =  6
214213oveq1i 5830 . . . . . . . . . . . . . . 15  |-  ( ( 4  +  2 )  x.  N )  =  ( 6  x.  N
)
2155nncni 9752 . . . . . . . . . . . . . . . . 17  |-  4  e.  CC
216 adddir 8826 . . . . . . . . . . . . . . . . 17  |-  ( ( 4  e.  CC  /\  2  e.  CC  /\  N  e.  CC )  ->  (
( 4  +  2 )  x.  N )  =  ( ( 4  x.  N )  +  ( 2  x.  N
) ) )
217215, 179, 216mp3an12 1269 . . . . . . . . . . . . . . . 16  |-  ( N  e.  CC  ->  (
( 4  +  2 )  x.  N )  =  ( ( 4  x.  N )  +  ( 2  x.  N
) ) )
218195, 217syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 4  +  2 )  x.  N
)  =  ( ( 4  x.  N )  +  ( 2  x.  N ) ) )
219214, 218syl5eqr 2331 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 6  x.  N
)  =  ( ( 4  x.  N )  +  ( 2  x.  N ) ) )
220219oveq1d 5835 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 6  x.  N )  /  3
)  =  ( ( ( 4  x.  N
)  +  ( 2  x.  N ) )  /  3 ) )
221139nncni 9752 . . . . . . . . . . . . . . . 16  |-  6  e.  CC
222 3cn 9814 . . . . . . . . . . . . . . . . 17  |-  3  e.  CC
223 3ne0 9827 . . . . . . . . . . . . . . . . 17  |-  3  =/=  0
224222, 223pm3.2i 443 . . . . . . . . . . . . . . . 16  |-  ( 3  e.  CC  /\  3  =/=  0 )
225 div23 9439 . . . . . . . . . . . . . . . 16  |-  ( ( 6  e.  CC  /\  N  e.  CC  /\  (
3  e.  CC  /\  3  =/=  0 ) )  ->  ( ( 6  x.  N )  / 
3 )  =  ( ( 6  /  3
)  x.  N ) )
226221, 224, 225mp3an13 1270 . . . . . . . . . . . . . . 15  |-  ( N  e.  CC  ->  (
( 6  x.  N
)  /  3 )  =  ( ( 6  /  3 )  x.  N ) )
227195, 226syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 6  x.  N )  /  3
)  =  ( ( 6  /  3 )  x.  N ) )
228 3t2e6 9868 . . . . . . . . . . . . . . . . 17  |-  ( 3  x.  2 )  =  6
229228oveq1i 5830 . . . . . . . . . . . . . . . 16  |-  ( ( 3  x.  2 )  /  3 )  =  ( 6  /  3
)
230179, 222, 223divcan3i 9502 . . . . . . . . . . . . . . . 16  |-  ( ( 3  x.  2 )  /  3 )  =  2
231229, 230eqtr3i 2307 . . . . . . . . . . . . . . 15  |-  ( 6  /  3 )  =  2
232231oveq1i 5830 . . . . . . . . . . . . . 14  |-  ( ( 6  /  3 )  x.  N )  =  ( 2  x.  N
)
233227, 232syl6eq 2333 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 6  x.  N )  /  3
)  =  ( 2  x.  N ) )
234124recnd 8857 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 4  x.  N
)  e.  CC )
235 remulcl 8818 . . . . . . . . . . . . . . . 16  |-  ( ( 2  e.  RR  /\  N  e.  RR )  ->  ( 2  x.  N
)  e.  RR )
236118, 36, 235sylancr 646 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 2  x.  N
)  e.  RR )
237236recnd 8857 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 2  x.  N
)  e.  CC )
238 divdir 9443 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) )
239224, 238mp3an3 1268 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) )
240234, 237, 239syl2anc 644 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 4  x.  N )  +  ( 2  x.  N
) )  /  3
)  =  ( ( ( 4  x.  N
)  /  3 )  +  ( ( 2  x.  N )  / 
3 ) ) )
241220, 233, 2403eqtr3d 2325 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2  x.  N
)  =  ( ( ( 4  x.  N
)  /  3 )  +  ( ( 2  x.  N )  / 
3 ) ) )
242241oveq1d 5835 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2  x.  N )  -  (
( 4  x.  N
)  /  3 ) )  =  ( ( ( ( 4  x.  N )  /  3
)  +  ( ( 2  x.  N )  /  3 ) )  -  ( ( 4  x.  N )  / 
3 ) ) )
243126recnd 8857 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 4  x.  N )  /  3
)  e.  CC )
244 nnrp 10359 . . . . . . . . . . . . . . 15  |-  ( 3  e.  NN  ->  3  e.  RR+ )
245115, 244ax-mp 10 . . . . . . . . . . . . . 14  |-  3  e.  RR+
246 rpdivcl 10372 . . . . . . . . . . . . . 14  |-  ( ( ( 2  x.  N
)  e.  RR+  /\  3  e.  RR+ )  ->  (
( 2  x.  N
)  /  3 )  e.  RR+ )
24795, 245, 246sylancl 645 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 2  x.  N )  /  3
)  e.  RR+ )
248247rpcnd 10388 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 2  x.  N )  /  3
)  e.  CC )
249243, 248pncan2d 9155 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( 4  x.  N )  /  3 )  +  ( ( 2  x.  N )  /  3
) )  -  (
( 4  x.  N
)  /  3 ) )  =  ( ( 2  x.  N )  /  3 ) )
250242, 249eqtrd 2317 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2  x.  N )  -  (
( 4  x.  N
)  /  3 ) )  =  ( ( 2  x.  N )  /  3 ) )
251250oveq1d 5835 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 2  x.  N )  -  ( ( 4  x.  N )  /  3
) )  x.  ( log `  2 ) )  =  ( ( ( 2  x.  N )  /  3 )  x.  ( log `  2
) ) )
252101recnd 8857 . . . . . . . . . 10  |-  ( ph  ->  ( log `  2
)  e.  CC )
253237, 243, 252subdird 9232 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 2  x.  N )  -  ( ( 4  x.  N )  /  3
) )  x.  ( log `  2 ) )  =  ( ( ( 2  x.  N )  x.  ( log `  2
) )  -  (
( ( 4  x.  N )  /  3
)  x.  ( log `  2 ) ) ) )
254251, 253eqtr3d 2319 . . . . . . . 8  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  ( log `  2 ) )  =  ( ( ( 2  x.  N )  x.  ( log `  2
) )  -  (
( ( 4  x.  N )  /  3
)  x.  ( log `  2 ) ) ) )
255134recnd 8857 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 4  x.  N )  / 
3 )  x.  ( log `  2 ) )  e.  CC )
256169, 255, 170nnncan2d 9188 . . . . . . . 8  |-  ( 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
) ) ) )
257212, 254, 2563eqtr4d 2327 . . . . . . 7  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  ( log `  2 ) )  =  ( ( ( N  x.  ( log `  4 ) )  -  ( log `  N
) )  -  (
( ( ( 4  x.  N )  / 
3 )  x.  ( log `  2 ) )  -  ( log `  N
) ) ) )
258117recnd 8857 . . . . . . . . . . 11  |-  ( ph  ->  ( ( sqr `  (
2  x.  N ) )  /  3 )  e.  CC )
259179a1i 12 . . . . . . . . . . 11  |-  ( ph  ->  2  e.  CC )
260121recnd 8857 . . . . . . . . . . 11  |-  ( ph  ->  ( log `  (
2  x.  N ) )  e.  CC )
261258, 259, 260adddird 8856 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 )  x.  ( log `  ( 2  x.  N ) ) )  =  ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  (
2  x.  N ) ) )  +  ( 2  x.  ( log `  ( 2  x.  N
) ) ) ) )
262 relogmul 19940 . . . . . . . . . . . . . 14  |-  ( ( 2  e.  RR+  /\  N  e.  RR+ )  ->  ( log `  ( 2  x.  N ) )  =  ( ( log `  2
)  +  ( log `  N ) ) )
26391, 61, 262sylancr 646 . . . . . . . . . . . . 13  |-  ( ph  ->  ( log `  (
2  x.  N ) )  =  ( ( log `  2 )  +  ( log `  N
) ) )
264263oveq2d 5836 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2  x.  ( log `  ( 2  x.  N ) ) )  =  ( 2  x.  ( ( log `  2
)  +  ( log `  N ) ) ) )
265259, 252, 170adddid 8855 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2  x.  (
( log `  2
)  +  ( log `  N ) ) )  =  ( ( 2  x.  ( log `  2
) )  +  ( 2  x.  ( log `  N ) ) ) )
266264, 265eqtrd 2317 . . . . . . . . . . 11  |-  ( ph  ->  ( 2  x.  ( log `  ( 2  x.  N ) ) )  =  ( ( 2  x.  ( log `  2
) )  +  ( 2  x.  ( log `  N ) ) ) )
267266oveq2d 5836 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( log `  (
2  x.  N ) ) )  +  ( 2  x.  ( log `  ( 2  x.  N
) ) ) )  =  ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  (
2  x.  N ) ) )  +  ( ( 2  x.  ( log `  2 ) )  +  ( 2  x.  ( log `  N
) ) ) ) )
268261, 267eqtrd 2317 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 )  x.  ( log `  ( 2  x.  N ) ) )  =  ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  (
2  x.  N ) ) )  +  ( ( 2  x.  ( log `  2 ) )  +  ( 2  x.  ( log `  N
) ) ) ) )
269150nncni 9752 . . . . . . . . . . . . 13  |-  5  e.  CC
270269a1i 12 . . . . . . . . . . . 12  |-  ( ph  ->  5  e.  CC )
271243, 270, 252subdird 9232 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( 4  x.  N )  /  3 )  - 
5 )  x.  ( log `  2 ) )  =  ( ( ( ( 4  x.  N
)  /  3 )  x.  ( log `  2
) )  -  (
5  x.  ( log `  2 ) ) ) )
272271oveq1d 5835 . . . . . . . . . 10  |-  ( 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
) ) ) )
273269, 199mulcli 8838 . . . . . . . . . . . 12  |-  ( 5  x.  ( log `  2
) )  e.  CC
274273a1i 12 . . . . . . . . . . 11  |-  ( ph  ->  ( 5  x.  ( log `  2 ) )  e.  CC )
275255, 274, 170nnncan1d 9187 . . . . . . . . . 10  |-  ( 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
) ) ) )
276272, 275eqtrd 2317 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( ( 4  x.  N
)  /  3 )  -  5 )  x.  ( log `  2
) )  -  (
( ( ( 4  x.  N )  / 
3 )  x.  ( log `  2 ) )  -  ( log `  N
) ) )  =  ( ( log `  N
)  -  ( 5  x.  ( log `  2
) ) ) )
277268, 276oveq12d 5838 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( ( sqr `  (
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 ) ) ) )  =  ( ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( log `  (
2  x.  N ) ) )  +  ( ( 2  x.  ( log `  2 ) )  +  ( 2  x.  ( log `  N
) ) ) )  +  ( ( log `  N )  -  (
5  x.  ( log `  2 ) ) ) ) )
278135recnd 8857 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( 4  x.  N )  /  3 )  x.  ( log `  2
) )  -  ( log `  N ) )  e.  CC )
279185, 186, 278addsubassd 9173 . . . . . . . 8  |-  ( ph  ->  ( ( ( ( ( ( sqr `  (
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
) ) )  =  ( ( ( ( ( sqr `  (
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 ) ) ) ) )
280269, 222, 199subdiri 9225 . . . . . . . . . . . . . 14  |-  ( ( 5  -  3 )  x.  ( log `  2
) )  =  ( ( 5  x.  ( log `  2 ) )  -  ( 3  x.  ( log `  2
) ) )
281 3p2e5 9851 . . . . . . . . . . . . . . . . 17  |-  ( 3  +  2 )  =  5
282281oveq1i 5830 . . . . . . . . . . . . . . . 16  |-  ( ( 3  +  2 )  -  3 )  =  ( 5  -  3 )
283 pncan2 9054 . . . . . . . . . . . . . . . . 17  |-  ( ( 3  e.  CC  /\  2  e.  CC )  ->  ( ( 3  +  2 )  -  3 )  =  2 )
284222, 179, 283mp2an 655 . . . . . . . . . . . . . . . 16  |-  ( ( 3  +  2 )  -  3 )  =  2
285282, 284eqtr3i 2307 . . . . . . . . . . . . . . 15  |-  ( 5  -  3 )  =  2
286285oveq1i 5830 . . . . . . . . . . . . . 14  |-  ( ( 5  -  3 )  x.  ( log `  2
) )  =  ( 2  x.  ( log `  2 ) )
287280, 286eqtr3i 2307 . . . . . . . . . . . . 13  |-  ( ( 5  x.  ( log `  2 ) )  -  ( 3  x.  ( log `  2
) ) )  =  ( 2  x.  ( log `  2 ) )
288287a1i 12 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 5  x.  ( log `  2
) )  -  (
3  x.  ( log `  2 ) ) )  =  ( 2  x.  ( log `  2
) ) )
289 df-3 9801 . . . . . . . . . . . . . . . . 17  |-  3  =  ( 2  +  1 )
290289oveq1i 5830 . . . . . . . . . . . . . . . 16  |-  ( 3  x.  ( log `  N
) )  =  ( ( 2  +  1 )  x.  ( log `  N ) )
291 ax-1cn 8791 . . . . . . . . . . . . . . . . . 18  |-  1  e.  CC
292291a1i 12 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  CC )
293259, 292, 170adddird 8856 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 2  +  1 )  x.  ( log `  N ) )  =  ( ( 2  x.  ( log `  N
) )  +  ( 1  x.  ( log `  N ) ) ) )
294290, 293syl5eq 2329 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 3  x.  ( log `  N ) )  =  ( ( 2  x.  ( log `  N
) )  +  ( 1  x.  ( log `  N ) ) ) )
295170mulid2d 8849 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1  x.  ( log `  N ) )  =  ( log `  N
) )
296295oveq2d 5836 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 2  x.  ( log `  N
) )  +  ( 1  x.  ( log `  N ) ) )  =  ( ( 2  x.  ( log `  N
) )  +  ( log `  N ) ) )
297294, 296eqtrd 2317 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 3  x.  ( log `  N ) )  =  ( ( 2  x.  ( log `  N
) )  +  ( log `  N ) ) )
298297oveq1d 5835 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 3  x.  ( log `  N
) )  -  (
5  x.  ( log `  2 ) ) )  =  ( ( ( 2  x.  ( log `  N ) )  +  ( log `  N
) )  -  (
5  x.  ( log `  2 ) ) ) )
299 mulcl 8817 . . . . . . . . . . . . . . 15  |-  ( ( 2  e.  CC  /\  ( log `  N )  e.  CC )  -> 
( 2  x.  ( log `  N ) )  e.  CC )
300179, 170, 299sylancr 646 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 2  x.  ( log `  N ) )  e.  CC )
301300, 170, 274addsubassd 9173 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 2  x.  ( log `  N
) )  +  ( log `  N ) )  -  ( 5  x.  ( log `  2
) ) )  =  ( ( 2  x.  ( log `  N
) )  +  ( ( log `  N
)  -  ( 5  x.  ( log `  2
) ) ) ) )
302298, 301eqtrd 2317 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 3  x.  ( log `  N
) )  -  (
5  x.  ( log `  2 ) ) )  =  ( ( 2  x.  ( log `  N ) )  +  ( ( log `  N
)  -  ( 5  x.  ( log `  2
) ) ) ) )
303288, 302oveq12d 5838 . . . . . . . . . . 11  |-  ( 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
) ) ) ) ) )
304 relogdiv 19941 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  RR+  /\  2  e.  RR+ )  ->  ( log `  ( N  / 
2 ) )  =  ( ( log `  N
)  -  ( log `  2 ) ) )
30561, 91, 304sylancl 645 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( log `  ( N  /  2 ) )  =  ( ( log `  N )  -  ( log `  2 ) ) )
306305oveq2d 5836 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 3  x.  ( log `  ( N  / 
2 ) ) )  =  ( 3  x.  ( ( log `  N
)  -  ( log `  2 ) ) ) )
307 subdi 9209 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) ) ) )
308222, 199, 307mp3an13 1270 . . . . . . . . . . . . . 14  |-  ( ( log `  N )  e.  CC  ->  (
3  x.  ( ( log `  N )  -  ( log `  2
) ) )  =  ( ( 3  x.  ( log `  N
) )  -  (
3  x.  ( log `  2 ) ) ) )
309170, 308syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 3  x.  (
( log `  N
)  -  ( log `  2 ) ) )  =  ( ( 3  x.  ( log `  N ) )  -  ( 3  x.  ( log `  2 ) ) ) )
310306, 309eqtrd 2317 . . . . . . . . . . . 12  |-  ( ph  ->  ( 3  x.  ( log `  ( N  / 
2 ) ) )  =  ( ( 3  x.  ( log `  N
) )  -  (
3  x.  ( log `  2 ) ) ) )
311 div23 9439 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  e.  CC  /\  N  e.  CC  /\  (
3  e.  CC  /\  3  =/=  0 ) )  ->  ( ( 2  x.  N )  / 
3 )  =  ( ( 2  /  3
)  x.  N ) )
312179, 224, 311mp3an13 1270 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  CC  ->  (
( 2  x.  N
)  /  3 )  =  ( ( 2  /  3 )  x.  N ) )
313195, 312syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 2  x.  N )  /  3
)  =  ( ( 2  /  3 )  x.  N ) )
314222, 179, 222, 179, 180, 180divmuldivi 9516 . . . . . . . . . . . . . . . . . 18  |-  ( ( 3  /  2 )  x.  ( 3  / 
2 ) )  =  ( ( 3  x.  3 )  /  (
2  x.  2 ) )
315 3t3e9 9869 . . . . . . . . . . . . . . . . . . 19  |-  ( 3  x.  3 )  =  9
316315, 206oveq12i 5832 . . . . . . . . . . . . . . . . . 18  |-  ( ( 3  x.  3 )  /  ( 2  x.  2 ) )  =  ( 9  /  4
)
317314, 316eqtr2i 2306 . . . . . . . . . . . . . . . . 17  |-  ( 9  /  4 )  =  ( ( 3  / 
2 )  x.  (
3  /  2 ) )
318317a1i 12 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 9  /  4
)  =  ( ( 3  /  2 )  x.  ( 3  / 
2 ) ) )
319313, 318oveq12d 5838 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  (
9  /  4 ) )  =  ( ( ( 2  /  3
)  x.  N )  x.  ( ( 3  /  2 )  x.  ( 3  /  2
) ) ) )
320179, 222, 223divcli 9498 . . . . . . . . . . . . . . . 16  |-  ( 2  /  3 )  e.  CC
321222, 179, 180divcli 9498 . . . . . . . . . . . . . . . . 17  |-  ( 3  /  2 )  e.  CC
322 mul4 8977 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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
) ) ) )
323321, 321, 322mpanr12 668 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
) ) ) )
324320, 195, 323sylancr 646 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( 2  /  3 )  x.  N )  x.  (
( 3  /  2
)  x.  ( 3  /  2 ) ) )  =  ( ( ( 2  /  3
)  x.  ( 3  /  2 ) )  x.  ( N  x.  ( 3  /  2
) ) ) )
325 divcan6 9463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 2  e.  CC  /\  2  =/=  0 )  /\  ( 3  e.  CC  /\  3  =/=  0 ) )  -> 
( ( 2  / 
3 )  x.  (
3  /  2 ) )  =  1 )
326179, 180, 222, 223, 325mp4an 656 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2  /  3 )  x.  ( 3  / 
2 ) )  =  1
327326oveq1i 5830 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 2  /  3
)  x.  ( 3  /  2 ) )  x.  ( N  x.  ( 3  /  2
) ) )  =  ( 1  x.  ( N  x.  ( 3  /  2 ) ) )
328 mulcl 8817 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  e.  CC  /\  ( 3  /  2
)  e.  CC )  ->  ( N  x.  ( 3  /  2
) )  e.  CC )
329195, 321, 328sylancl 645 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( N  x.  (
3  /  2 ) )  e.  CC )
330329mulid2d 8849 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1  x.  ( N  x.  ( 3  /  2 ) ) )  =  ( N  x.  ( 3  / 
2 ) ) )
331327, 330syl5eq 2329 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( 2  /  3 )  x.  ( 3  /  2
) )  x.  ( N  x.  ( 3  /  2 ) ) )  =  ( N  x.  ( 3  / 
2 ) ) )
332179, 180pm3.2i 443 . . . . . . . . . . . . . . . . . 18  |-  ( 2  e.  CC  /\  2  =/=  0 )
333 div12 9442 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  e.  CC  /\  3  e.  CC  /\  (
2  e.  CC  /\  2  =/=  0 ) )  ->  ( N  x.  ( 3  /  2
) )  =  ( 3  x.  ( N  /  2 ) ) )
334222, 332, 333mp3an23 1271 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  CC  ->  ( N  x.  ( 3  /  2 ) )  =  ( 3  x.  ( N  /  2
) ) )
335195, 334syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  x.  (
3  /  2 ) )  =  ( 3  x.  ( N  / 
2 ) ) )
336331, 335eqtrd 2317 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( 2  /  3 )  x.  ( 3  /  2
) )  x.  ( N  x.  ( 3  /  2 ) ) )  =  ( 3  x.  ( N  / 
2 ) ) )
337319, 324, 3363eqtrd 2321 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  (
9  /  4 ) )  =  ( 3  x.  ( N  / 
2 ) ) )
338337, 84oveq12d 5838 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( 2  x.  N )  /  3 )  x.  ( 9  /  4
) )  x.  ( G `  ( N  /  2 ) ) )  =  ( ( 3  x.  ( N  /  2 ) )  x.  ( ( log `  ( N  /  2
) )  /  ( N  /  2 ) ) ) )
33977recni 8845 . . . . . . . . . . . . . . 15  |-  ( 9  /  4 )  e.  CC
340339a1i 12 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 9  /  4
)  e.  CC )
34187recnd 8857 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( G `  ( N  /  2 ) )  e.  CC )
342248, 340, 341mulassd 8854 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( 2  x.  N )  /  3 )  x.  ( 9  /  4
) )  x.  ( G `  ( N  /  2 ) ) )  =  ( ( ( 2  x.  N
)  /  3 )  x.  ( ( 9  /  4 )  x.  ( G `  ( N  /  2 ) ) ) ) )
343222a1i 12 . . . . . . . . . . . . . . 15  |-  ( ph  ->  3  e.  CC )
34478rpcnd 10388 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( N  /  2
)  e.  CC )
34585recnd 8857 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( log `  ( N  /  2 ) )  e.  CC )
34678rpne0d 10391 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  /  2
)  =/=  0 )
347345, 344, 346divcld 9532 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( log `  ( N  /  2 ) )  /  ( N  / 
2 ) )  e.  CC )
348343, 344, 347mulassd 8854 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 3  x.  ( N  /  2
) )  x.  (
( log `  ( N  /  2 ) )  /  ( N  / 
2 ) ) )  =  ( 3  x.  ( ( N  / 
2 )  x.  (
( log `  ( N  /  2 ) )  /  ( N  / 
2 ) ) ) ) )
349345, 344, 346divcan2d 9534 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( N  / 
2 )  x.  (
( log `  ( N  /  2 ) )  /  ( N  / 
2 ) ) )  =  ( log `  ( N  /  2 ) ) )
350349oveq2d 5836 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 3  x.  (
( N  /  2
)  x.  ( ( log `  ( N  /  2 ) )  /  ( N  / 
2 ) ) ) )  =  ( 3  x.  ( log `  ( N  /  2 ) ) ) )
351348, 350eqtrd 2317 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 3  x.  ( N  /  2
) )  x.  (
( log `  ( N  /  2 ) )  /  ( N  / 
2 ) ) )  =  ( 3  x.  ( log `  ( N  /  2 ) ) ) )
352338, 342, 3513eqtr3d 2325 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  (
( 9  /  4
)  x.  ( G `
 ( N  / 
2 ) ) ) )  =  ( 3  x.  ( log `  ( N  /  2 ) ) ) )
353222, 199mulcli 8838 . . . . . . . . . . . . . 14  |-  ( 3  x.  ( log `  2
) )  e.  CC
354353a1i 12 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 3  x.  ( log `  2 ) )  e.  CC )
355 mulcl 8817 . . . . . . . . . . . . . 14  |-  ( ( 3  e.  CC  /\  ( log `  N )  e.  CC )  -> 
( 3  x.  ( log `  N ) )  e.  CC )
356222, 170, 355sylancr 646 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 3  x.  ( log `  N ) )  e.  CC )
357274, 354, 356npncan3d 9189 . . . . . . . . . . . 12  |-  ( 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
) ) ) )
358310, 352, 3573eqtr4d 2327 . . . . . . . . . . 11  |-  ( 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 ) ) ) ) )
359118, 93remulcli 8847 . . . . . . . . . . . . . 14  |-  ( 2  x.  ( log `  2
) )  e.  RR
360359recni 8845 . . . . . . . . . . . . 13  |-  ( 2  x.  ( log `  2
) )  e.  CC
361360a1i 12 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2  x.  ( log `  2 ) )  e.  CC )
362 subcl 9047 . . . . . . . . . . . . 13  |-  ( ( ( log `  N
)  e.  CC  /\  ( 5  x.  ( log `  2 ) )  e.  CC )  -> 
( ( log `  N
)  -  ( 5  x.  ( log `  2
) ) )  e.  CC )
363170, 273, 362sylancl 645 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( log `  N
)  -  ( 5  x.  ( log `  2
) ) )  e.  CC )
364361, 300, 363addassd 8853 . . . . . . . . . . 11  |-  ( 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
) ) ) ) ) )
365303, 358, 3643eqtr4d 2327 . . . . . . . . . 10  |-  ( 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
) ) ) ) )
366365oveq2d 5836 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( log `  (
2  x.  N ) ) )  +  ( ( ( 2  x.  N )  /  3
)  x.  ( ( 9  /  4 )  x.  ( G `  ( N  /  2
) ) ) ) )  =  ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  (
2  x.  N ) ) )  +  ( ( ( 2  x.  ( log `  2
) )  +  ( 2  x.  ( log `  N ) ) )  +  ( ( log `  N )  -  (
5  x.  ( log `  2 ) ) ) ) ) )
367 mulcl 8817 . . . . . . . . . . . 12  |-  ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  e.  CC  /\  ( log `  2 )  e.  CC )  ->  (
( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  2
) )  e.  CC )
368258, 199, 367sylancl 645 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( log `  2 ) )  e.  CC )
369258, 170mulcld 8851 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( log `  N ) )  e.  CC )
37089recnd 8857 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 9  / 
4 )  x.  ( G `  ( N  /  2 ) ) )  e.  CC )
371248, 370mulcld 8851 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  (
( 9  /  4
)  x.  ( G `
 ( N  / 
2 ) ) ) )  e.  CC )
372368, 369, 371addassd 8853 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  2
) )  +  ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  N
) ) )  +  ( ( ( 2  x.  N )  / 
3 )  x.  (
( 9  /  4
)  x.  ( G `
 ( N  / 
2 ) ) ) ) )  =  ( ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( log `  2 ) )  +  ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  N
) )  +  ( ( ( 2  x.  N )  /  3
)  x.  ( ( 9  /  4 )  x.  ( G `  ( N  /  2
) ) ) ) ) ) )
373263oveq2d 5836 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( log `  ( 2  x.  N
) ) )  =  ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( ( log `  2 )  +  ( log `  N
) ) ) )
374258, 252, 170adddid 8855 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( ( log `  2 )  +  ( log `  N
) ) )  =  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( log `  2
) )  +  ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  N
) ) ) )
375373, 374eqtrd 2317 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( log `  ( 2  x.  N
) ) )  =  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( log `  2
) )  +  ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  N
) ) ) )
376375oveq1d 5835 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( log `  (
2  x.  N ) ) )  +  ( ( ( 2  x.  N )  /  3
)  x.  ( ( 9  /  4 )  x.  ( G `  ( N  /  2
) ) ) ) )  =  ( ( ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( log `  2 ) )  +  ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( log `  N
) ) )  +  ( ( ( 2  x.  N )  / 
3 )  x.  (
( 9  /  4
)  x.  ( G `
 ( N  / 
2 ) ) ) ) ) )
37759oveq2d 5836 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  ( F `  N )
)  =  ( ( ( 2  x.  N
)  /  3 )  x.  ( ( ( ( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) )  +  ( ( 9  / 
4 )  x.  ( G `  ( N  /  2 ) ) ) )  +  ( ( log `  2
)  /  ( sqr `  ( 2  x.  N
) ) ) ) ) )
37890recnd 8857 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( sqr `  2 )  x.  ( G `  ( sqr `  N ) ) )  +  ( ( 9  /  4 )  x.  ( G `  ( N  /  2
) ) ) )  e.  CC )
37998recnd 8857 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( log `  2
)  /  ( sqr `  ( 2  x.  N
) ) )  e.  CC )
380248, 378, 379adddid 8855 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  (
( ( ( sqr `  2 )  x.  ( G `  ( sqr `  N ) ) )  +  ( ( 9  /  4 )  x.  ( G `  ( N  /  2
) ) ) )  +  ( ( log `  2 )  / 
( sqr `  (
2  x.  N ) ) ) ) )  =  ( ( ( ( 2  x.  N
)  /  3 )  x.  ( ( ( sqr `  2 )  x.  ( G `  ( sqr `  N ) ) )  +  ( ( 9  /  4
)  x.  ( G `
 ( N  / 
2 ) ) ) ) )  +  ( ( ( 2  x.  N )  /  3
)  x.  ( ( log `  2 )  /  ( sqr `  (
2  x.  N ) ) ) ) ) )
381377, 380eqtrd 2317 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  ( F `  N )
)  =  ( ( ( ( 2  x.  N )  /  3
)  x.  ( ( ( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) )  +  ( ( 9  / 
4 )  x.  ( G `  ( N  /  2 ) ) ) ) )  +  ( ( ( 2  x.  N )  / 
3 )  x.  (
( log `  2
)  /  ( sqr `  ( 2  x.  N
) ) ) ) ) )
38273recnd 8857 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) )  e.  CC )
383248, 382, 370adddid 8855 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  (
( ( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) )  +  ( ( 9  / 
4 )  x.  ( G `  ( N  /  2 ) ) ) ) )  =  ( ( ( ( 2  x.  N )  /  3 )  x.  ( ( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) ) )  +  ( ( ( 2  x.  N )  /  3 )  x.  ( ( 9  / 
4 )  x.  ( G `  ( N  /  2 ) ) ) ) ) )
38495rpge0d 10390 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  <_  ( 2  x.  N ) )
385 remsqsqr 11737 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 2  x.  N
)  e.  RR  /\  0  <_  ( 2  x.  N ) )  -> 
( ( sqr `  (
2  x.  N ) )  x.  ( sqr `  ( 2  x.  N
) ) )  =  ( 2  x.  N
) )
386236, 384, 385syl2anc 644 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( sqr `  (
2  x.  N ) )  x.  ( sqr `  ( 2  x.  N
) ) )  =  ( 2  x.  N
) )
387386oveq1d 5835 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( sqr `  ( 2  x.  N
) )  x.  ( sqr `  ( 2  x.  N ) ) )  /  3 )  =  ( ( 2  x.  N )  /  3
) )
388114recnd 8857 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( sqr `  (
2  x.  N ) )  e.  CC )
389223a1i 12 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  3  =/=  0 )
390388, 388, 343, 389div23d 9569 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( sqr `  ( 2  x.  N
) )  x.  ( sqr `  ( 2  x.  N ) ) )  /  3 )  =  ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( sqr `  ( 2  x.  N
) ) ) )
391387, 390eqtr3d 2319 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 2  x.  N )  /  3
)  =  ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( sqr `  (
2  x.  N ) ) ) )
392391oveq1d 5835 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  (
( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) ) )  =  ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( sqr `  (
2  x.  N ) ) )  x.  (
( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) ) ) )
393258, 388, 382mulassd 8854 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( sqr `  (
2  x.  N ) ) )  x.  (
( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) ) )  =  ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( ( sqr `  (
2  x.  N ) )  x.  ( ( sqr `  2 )  x.  ( G `  ( sqr `  N ) ) ) ) ) )
394 2pos 9824 . . . . . . . . . . . . . . . . . . . . 21  |-  0  <  2
39518, 118, 394ltleii 8937 . . . . . . . . . . . . . . . . . . . 20  |-  0  <_  2
396118, 395pm3.2i 443 . . . . . . . . . . . . . . . . . . 19  |-  ( 2  e.  RR  /\  0  <_  2 )
39761rprege0d 10393 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( N  e.  RR  /\  0  <_  N )
)
398 sqrmul 11740 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 2  e.  RR  /\  0  <_  2 )  /\  ( N  e.  RR  /\  0  <_  N ) )  -> 
( sqr `  (
2  x.  N ) )  =  ( ( sqr `  2 )  x.  ( sqr `  N
) ) )
399396, 397, 398sylancr 646 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( sqr `  (
2  x.  N ) )  =  ( ( sqr `  2 )  x.  ( sqr `  N
) ) )
400399oveq1d 5835 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( sqr `  (
2  x.  N ) )  x.  ( ( sqr `  2 )  x.  ( G `  ( sqr `  N ) ) ) )  =  ( ( ( sqr `  2 )  x.  ( sqr `  N
) )  x.  (
( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) ) ) )
40160recni 8845 . . . . . . . . . . . . . . . . . . 19  |-  ( sqr `  2 )  e.  CC
402401a1i 12 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( sqr `  2
)  e.  CC )
40362rpcnd 10388 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( sqr `  N
)  e.  CC )
40471recnd 8857 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( G `  ( sqr `  N ) )  e.  CC )
405402, 403, 402, 404mul4d 9020 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( sqr `  2 )  x.  ( sqr `  N
) )  x.  (
( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) ) )  =  ( ( ( sqr `  2 )  x.  ( sqr `  2
) )  x.  (
( sqr `  N
)  x.  ( G `
 ( sqr `  N
) ) ) ) )
406 remsqsqr 11737 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2  e.  RR  /\  0  <_  2 )  -> 
( ( sqr `  2
)  x.  ( sqr `  2 ) )  =  2 )
407118, 395, 406mp2an 655 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( sqr `  2 )  x.  ( sqr `  2
) )  =  2
408407a1i 12 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( sqr `  2
)  x.  ( sqr `  2 ) )  =  2 )
40968oveq2d 5836 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( sqr `  N
)  x.  ( G `
 ( sqr `  N
) ) )  =  ( ( sqr `  N
)  x.  ( ( log `  ( sqr `  N ) )  / 
( sqr `  N
) ) ) )
41069recnd 8857 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( log `  ( sqr `  N ) )  e.  CC )
41162rpne0d 10391 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( sqr `  N
)  =/=  0 )
412410, 403, 411divcan2d 9534 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( sqr `  N
)  x.  ( ( log `  ( sqr `  N ) )  / 
( sqr `  N
) ) )  =  ( log `  ( sqr `  N ) ) )
413409, 412eqtrd 2317 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( sqr `  N
)  x.  ( G `
 ( sqr `  N
) ) )  =  ( log `  ( sqr `  N ) ) )
414408, 413oveq12d 5838 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( sqr `  2 )  x.  ( sqr `  2
) )  x.  (
( sqr `  N
)  x.  ( G `
 ( sqr `  N
) ) ) )  =  ( 2  x.  ( log `  ( sqr `  N ) ) ) )
4154102timesd 9950 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 2  x.  ( log `  ( sqr `  N
) ) )  =  ( ( log `  ( sqr `  N ) )  +  ( log `  ( sqr `  N ) ) ) )
41662, 62relogmuld 19971 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( log `  (
( sqr `  N
)  x.  ( sqr `  N ) ) )  =  ( ( log `  ( sqr `  N
) )  +  ( log `  ( sqr `  N ) ) ) )
417 remsqsqr 11737 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  e.  RR  /\  0  <_  N )  -> 
( ( sqr `  N
)  x.  ( sqr `  N ) )  =  N )
418397, 417syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( sqr `  N
)  x.  ( sqr `  N ) )  =  N )
419418fveq2d 5490 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( log `  (
( sqr `  N
)  x.  ( sqr `  N ) ) )  =  ( log `  N
) )
420416, 419eqtr3d 2319 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( log `  ( sqr `  N ) )  +  ( log `  ( sqr `  N ) ) )  =  ( log `  N ) )
421414, 415, 4203eqtrd 2321 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( sqr `  2 )  x.  ( sqr `  2
) )  x.  (
( sqr `  N
)  x.  ( G `
 ( sqr `  N
) ) ) )  =  ( log `  N
) )
422400, 405, 4213eqtrd 2321 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( sqr `  (
2  x.  N ) )  x.  ( ( sqr `  2 )  x.  ( G `  ( sqr `  N ) ) ) )  =  ( log `  N
) )
423422oveq2d 5836 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( ( sqr `  ( 2  x.  N ) )  x.  ( ( sqr `  2 )  x.  ( G `  ( sqr `  N ) ) ) ) )  =  ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( log `  N ) ) )
424392, 393, 4233eqtrd 2321 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  (
( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) ) )  =  ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( log `  N
) ) )
425424oveq1d 5835 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( 2  x.  N )  /  3 )  x.  ( ( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) ) )  +  ( ( ( 2  x.  N )  /  3 )  x.  ( ( 9  / 
4 )  x.  ( G `  ( N  /  2 ) ) ) ) )  =  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( log `  N
) )  +  ( ( ( 2  x.  N )  /  3
)  x.  ( ( 9  /  4 )  x.  ( G `  ( N  /  2
) ) ) ) ) )
426383, 425eqtrd 2317 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  (
( ( sqr `  2
)  x.  ( G `
 ( sqr `  N
) ) )  +  ( ( 9  / 
4 )  x.  ( G `  ( N  /  2 ) ) ) ) )  =  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( log `  N
) )  +  ( ( ( 2  x.  N )  /  3
)  x.  ( ( 9  /  4 )  x.  ( G `  ( N  /  2
) ) ) ) ) )
427391oveq1d 5835 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  (
( log `  2
)  /  ( sqr `  ( 2  x.  N
) ) ) )  =  ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( sqr `  (
2  x.  N ) ) )  x.  (
( log `  2
)  /  ( sqr `  ( 2  x.  N
) ) ) ) )
428258, 388, 379mulassd 8854 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( sqr `  (
2  x.  N ) ) )  x.  (
( log `  2
)  /  ( sqr `  ( 2  x.  N
) ) ) )  =  ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( ( sqr `  (
2  x.  N ) )  x.  ( ( log `  2 )  /  ( sqr `  (
2  x.  N ) ) ) ) ) )
42996rpne0d 10391 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( sqr `  (
2  x.  N ) )  =/=  0 )
430252, 388, 429divcan2d 9534 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( sqr `  (
2  x.  N ) )  x.  ( ( log `  2 )  /  ( sqr `  (
2  x.  N ) ) ) )  =  ( log `  2
) )
431430oveq2d 5836 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( ( sqr `  ( 2  x.  N ) )  x.  ( ( log `  2 )  / 
( sqr `  (
2  x.  N ) ) ) ) )  =  ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( log `  2
) ) )
432427, 428, 4313eqtrd 2321 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  (
( log `  2
)  /  ( sqr `  ( 2  x.  N
) ) ) )  =  ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( log `  2
) ) )
433426, 432oveq12d 5838 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( 2  x.  N )  /  3 )  x.  ( ( ( sqr `  2 )  x.  ( G `  ( sqr `  N ) ) )  +  ( ( 9  /  4 )  x.  ( G `  ( N  /  2
) ) ) ) )  +  ( ( ( 2  x.  N
)  /  3 )  x.  ( ( log `  2 )  / 
( sqr `  (
2  x.  N ) ) ) ) )  =  ( ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  N
) )  +  ( ( ( 2  x.  N )  /  3
)  x.  ( ( 9  /  4 )  x.  ( G `  ( N  /  2
) ) ) ) )  +  ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  2
) ) ) )
434369, 371addcld 8850 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( log `  N
) )  +  ( ( ( 2  x.  N )  /  3
)  x.  ( ( 9  /  4 )  x.  ( G `  ( N  /  2
) ) ) ) )  e.  CC )
435434, 368addcomd 9010 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  N
) )  +  ( ( ( 2  x.  N )  /  3
)  x.  ( ( 9  /  4 )  x.  ( G `  ( N  /  2
) ) ) ) )  +  ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  2
) ) )  =  ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  x.  ( log `  2
) )  +  ( ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( log `  N ) )  +  ( ( ( 2  x.  N )  / 
3 )  x.  (
( 9  /  4
)  x.  ( G `
 ( N  / 
2 ) ) ) ) ) ) )
436381, 433, 4353eqtrd 2321 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  ( F `  N )
)  =  ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  2
) )  +  ( ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( log `  N ) )  +  ( ( ( 2  x.  N )  / 
3 )  x.  (
( 9  /  4
)  x.  ( G `
 ( N  / 
2 ) ) ) ) ) ) )
437372, 376, 4363eqtr4rd 2328 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  ( F `  N )
)  =  ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  (
2  x.  N ) ) )  +  ( ( ( 2  x.  N )  /  3
)  x.  ( ( 9  /  4 )  x.  ( G `  ( N  /  2
) ) ) ) ) )
438258, 260mulcld 8851 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( log `  ( 2  x.  N
) ) )  e.  CC )
439 addcl 8815 . . . . . . . . . . 11  |-  ( ( ( 2  x.  ( log `  2 ) )  e.  CC  /\  (
2  x.  ( log `  N ) )  e.  CC )  ->  (
( 2  x.  ( log `  2 ) )  +  ( 2  x.  ( log `  N
) ) )  e.  CC )
440360, 300, 439sylancr 646 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2  x.  ( log `  2
) )  +  ( 2  x.  ( log `  N ) ) )  e.  CC )
441438, 440, 363addassd 8853 . . . . . . . . 9  |-  ( ph  ->  ( ( ( ( ( sqr `  (
2  x.  N ) )  /  3 )  x.  ( log `  (
2  x.  N ) ) )  +  ( ( 2  x.  ( log `  2 ) )  +  ( 2  x.  ( log `  N
) ) ) )  +  ( ( log `  N )  -  (
5  x.  ( log `  2 ) ) ) )  =  ( ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( log `  ( 2  x.  N
) ) )  +  ( ( ( 2  x.  ( log `  2
) )  +  ( 2  x.  ( log `  N ) ) )  +  ( ( log `  N )  -  (
5  x.  ( log `  2 ) ) ) ) ) )
442366, 437, 4413eqtr4d 2327 . . . . . . . 8  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  ( F `  N )
)  =  ( ( ( ( ( sqr `  ( 2  x.  N
) )  /  3
)  x.  ( log `  ( 2  x.  N
) ) )  +  ( ( 2  x.  ( log `  2
) )  +  ( 2  x.  ( log `  N ) ) ) )  +  ( ( log `  N )  -  ( 5  x.  ( log `  2
) ) ) ) )
443277, 279, 4423eqtr4rd 2328 . . . . . . 7  |-  ( ph  ->  ( ( ( 2  x.  N )  / 
3 )  x.  ( F `  N )
)  =  ( ( ( ( ( ( sqr `  ( 2  x.  N ) )  /  3 )  +  2 )  x.  ( log `