Theorem bposlem9 16248

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

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   ph, x   N, p   x, N

Allowed substitution hints:   ph( p)   ps( x, n, p)   F( x, n, p)   G( x, p)

Proof of Theorem bposlem9

Dummy variable q is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bposlem9.4	. . 3 |- ( ph -> ; 6 4 < N )
2		bposlem7.1	. . . 4 |- 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	. . . 4 |- G = ( x e. RR+ |-> ( ( log ` x ) / x ) )
4		6nn0 9589	. . . . . 6 |- 6 e. NN0
5		4nn 9473	. . . . . 6 |- 4 e. NN
6	4, 5	decnncl 9805	. . . . 5 |- ; 6 4 e. NN
7	6	a1i 9	. . . 4 |- ( ph -> ; 6 4 e. NN )
8		bposlem9.3	. . . 4 |- ( ph -> N e. NN )
9		ere 12456	. . . . . . . 8 |- _e e. RR
10		8re 9392	. . . . . . . 8 |- 8 e. RR
11		egt2lt3 12566	. . . . . . . . . 10 |- ( 2 < _e /\ _e < 3 )
12	11	simpri 113	. . . . . . . . 9 |- _e < 3
13		3lt8 9504	. . . . . . . . 9 |- 3 < 8
14		3re 9381	. . . . . . . . . 10 |- 3 e. RR
15	9, 14, 10	lttri 8432	. . . . . . . . 9 |- ( ( _e < 3 /\ 3 < 8 ) -> _e < 8 )
16	12, 13, 15	mp2an 430	. . . . . . . 8 |- _e < 8
17	9, 10, 16	ltleii 8430	. . . . . . 7 |- _e <_ 8
18		0re 8327	. . . . . . . . 9 |- 0 e. RR
19		epos 12567	. . . . . . . . 9 |- 0 < _e
20	18, 9, 19	ltleii 8430	. . . . . . . 8 |- 0 <_ _e
21		8pos 9410	. . . . . . . . 9 |- 0 < 8
22	18, 10, 21	ltleii 8430	. . . . . . . 8 |- 0 <_ 8
23		le2sq 11066	. . . . . . . 8 |- ( ( ( _e e. RR /\ 0 <_ _e ) /\ ( 8 e. RR /\ 0 <_ 8 ) ) -> ( _e <_ 8 <-> ( _e ^ 2 ) <_ ( 8 ^ 2 ) ) )
24	9, 20, 10, 22, 23	mp4an 431	. . . . . . 7 |- ( _e <_ 8 <-> ( _e ^ 2 ) <_ ( 8 ^ 2 ) )
25	17, 24	mpbi 145	. . . . . 6 |- ( _e ^ 2 ) <_ ( 8 ^ 2 )
26	10	recni 8339	. . . . . . . 8 |- 8 e. CC
27	26	sqvali 11071	. . . . . . 7 |- ( 8 ^ 2 ) = ( 8 x. 8 )
28		8t8e64 9907	. . . . . . 7 |- ( 8 x. 8 ) = ; 6 4
29	27, 28	eqtri 2259	. . . . . 6 |- ( 8 ^ 2 ) = ; 6 4
30	25, 29	breqtri 4155	. . . . 5 |- ( _e ^ 2 ) <_ ; 6 4
31	30	a1i 9	. . . 4 |- ( ph -> ( _e ^ 2 ) <_ ; 6 4 )
32	9	resqcli 11076	. . . . . 6 |- ( _e ^ 2 ) e. RR
33	32	a1i 9	. . . . 5 |- ( ph -> ( _e ^ 2 ) e. RR )
34	6	nnrei 9316	. . . . . 6 |- ; 6 4 e. RR
35	34	a1i 9	. . . . 5 |- ( ph -> ; 6 4 e. RR )
36	8	nnred 9320	. . . . 5 |- ( ph -> N e. RR )
37		ltle 8414	. . . . . . 7 |- ( (; 6 4 e. RR /\ N e. RR ) -> (; 6 4 < N -> ; 6 4 <_ N ) )
38	34, 36, 37	sylancr 418	. . . . . 6 |- ( ph -> (; 6 4 < N -> ; 6 4 <_ N ) )
39	1, 38	mpd 13	. . . . 5 |- ( ph -> ; 6 4 <_ N )
40	33, 35, 36, 31, 39	letrd 8452	. . . 4 |- ( ph -> ( _e ^ 2 ) <_ N )
41	2, 3, 7, 8, 31, 40	bposlem7 16246	. . 3 |- ( ph -> (; 6 4 < N -> ( F ` N ) < ( F ` ; 6 4 ) ) )
42	1, 41	mpd 13	. 2 |- ( ph -> ( F ` N ) < ( F ` ; 6 4 ) )
43	2, 3	bposlem8 16247	. . . . 5 |- ( ( F ` ; 6 4 ) e. RR /\ ( F ` ; 6 4 ) < ( log ` 2 ) )
44	43	a1i 9	. . . 4 |- ( ph -> ( ( F ` ; 6 4 ) e. RR /\ ( F ` ; 6 4 ) < ( log ` 2 ) ) )
45	44	simpld 112	. . 3 |- ( ph -> ( F ` ; 6 4 ) e. RR )
46		2fveq3 5700	. . . . . . . 8 |- ( n = N -> ( G ` ( sqr ` n ) ) = ( G ` ( sqr ` N ) ) )
47	46	oveq2d 6101	. . . . . . 7 |- ( n = N -> ( ( sqr ` 2 ) x. ( G ` ( sqr ` n ) ) ) = ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) )
48		fvoveq1 6108	. . . . . . . 8 |- ( n = N -> ( G ` ( n / 2 ) ) = ( G ` ( N / 2 ) ) )
49	48	oveq2d 6101	. . . . . . 7 |- ( n = N -> ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) = ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) )
50	47, 49	oveq12d 6103	. . . . . 6 |- ( 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 ) ) ) ) )
51		oveq2 6093	. . . . . . . 8 |- ( n = N -> ( 2 x. n ) = ( 2 x. N ) )
52	51	fveq2d 5699	. . . . . . 7 |- ( n = N -> ( sqr ` ( 2 x. n ) ) = ( sqr ` ( 2 x. N ) ) )
53	52	oveq2d 6101	. . . . . 6 |- ( n = N -> ( ( log ` 2 ) / ( sqr ` ( 2 x. n ) ) ) = ( ( log ` 2 ) / ( sqr ` ( 2 x. N ) ) ) )
54	50, 53	oveq12d 6103	. . . . 5 |- ( 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 ) ) ) ) )
55		sqrt2re 12961	. . . . . . . . 9 |- ( sqr ` 2 ) e. RR
56	55	a1i 9	. . . . . . . 8 |- ( ph -> ( sqr ` 2 ) e. RR )
57		relogcl 16023	. . . . . . . . . . . 12 |- ( x e. RR+ -> ( log ` x ) e. RR )
58	57	adantl 277	. . . . . . . . . . 11 |- ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR )
59		simpr 110	. . . . . . . . . . 11 |- ( ( ph /\ x e. RR+ ) -> x e. RR+ )
60	58, 59	rerpdivcld 10140	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) / x ) e. RR )
61	60, 3	fmptd 5862	. . . . . . . . 9 |- ( ph -> G : RR+ --> RR )
62	8	nnrpd 10106	. . . . . . . . . 10 |- ( ph -> N e. RR+ )
63	62	rpsqrtcld 11941	. . . . . . . . 9 |- ( ph -> ( sqr ` N ) e. RR+ )
64	61, 63	ffvelcdmd 5844	. . . . . . . 8 |- ( ph -> ( G ` ( sqr ` N ) ) e. RR )
65	56, 64	remulcld 8357	. . . . . . 7 |- ( ph -> ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) e. RR )
66		9nn 9478	. . . . . . . . . . . 12 |- 9 e. NN
67	66	nnzi 9670	. . . . . . . . . . 11 |- 9 e. ZZ
68		znq 10034	. . . . . . . . . . 11 |- ( ( 9 e. ZZ /\ 4 e. NN ) -> ( 9 / 4 ) e. QQ )
69	67, 5, 68	mp2an 430	. . . . . . . . . 10 |- ( 9 / 4 ) e. QQ
70		qre 10035	. . . . . . . . . 10 |- ( ( 9 / 4 ) e. QQ -> ( 9 / 4 ) e. RR )
71	69, 70	ax-mp 5	. . . . . . . . 9 |- ( 9 / 4 ) e. RR
72	71	a1i 9	. . . . . . . 8 |- ( ph -> ( 9 / 4 ) e. RR )
73	62	rphalfcld 10121	. . . . . . . . 9 |- ( ph -> ( N / 2 ) e. RR+ )
74	61, 73	ffvelcdmd 5844	. . . . . . . 8 |- ( ph -> ( G ` ( N / 2 ) ) e. RR )
75	72, 74	remulcld 8357	. . . . . . 7 |- ( ph -> ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) e. RR )
76	65, 75	readdcld 8356	. . . . . 6 |- ( ph -> ( ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) e. RR )
77		2rp 10070	. . . . . . . . 9 |- 2 e. RR+
78		relogcl 16023	. . . . . . . . 9 |- ( 2 e. RR+ -> ( log ` 2 ) e. RR )
79	77, 78	ax-mp 5	. . . . . . . 8 |- ( log ` 2 ) e. RR
80	79	a1i 9	. . . . . . 7 |- ( ph -> ( log ` 2 ) e. RR )
81		rpmulcl 10090	. . . . . . . . 9 |- ( ( 2 e. RR+ /\ N e. RR+ ) -> ( 2 x. N ) e. RR+ )
82	77, 62, 81	sylancr 418	. . . . . . . 8 |- ( ph -> ( 2 x. N ) e. RR+ )
83	82	rpsqrtcld 11941	. . . . . . 7 |- ( ph -> ( sqr ` ( 2 x. N ) ) e. RR+ )
84	80, 83	rerpdivcld 10140	. . . . . 6 |- ( ph -> ( ( log ` 2 ) / ( sqr ` ( 2 x. N ) ) ) e. RR )
85	76, 84	readdcld 8356	. . . . 5 |- ( ph -> ( ( ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqr ` ( 2 x. N ) ) ) ) e. RR )
86	2, 54, 8, 85	fvmptd3 5799	. . . 4 |- ( ph -> ( F ` N ) = ( ( ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) + ( ( log ` 2 ) / ( sqr ` ( 2 x. N ) ) ) ) )
87	86, 85	eqeltrd 2315	. . 3 |- ( ph -> ( F ` N ) e. RR )
88	44	simprd 114	. . . 4 |- ( ph -> ( F ` ; 6 4 ) < ( log ` 2 ) )
89		nnrp 10075	. . . . . . . . . . 11 |- ( 4 e. NN -> 4 e. RR+ )
90	5, 89	ax-mp 5	. . . . . . . . . 10 |- 4 e. RR+
91		relogcl 16023	. . . . . . . . . 10 |- ( 4 e. RR+ -> ( log ` 4 ) e. RR )
92	90, 91	ax-mp 5	. . . . . . . . 9 |- ( log ` 4 ) e. RR
93		remulcl 8308	. . . . . . . . 9 |- ( ( N e. RR /\ ( log ` 4 ) e. RR ) -> ( N x. ( log ` 4 ) ) e. RR )
94	36, 92, 93	sylancl 417	. . . . . . . 8 |- ( ph -> ( N x. ( log ` 4 ) ) e. RR )
95	62	relogcld 16044	. . . . . . . 8 |- ( ph -> ( log ` N ) e. RR )
96	94, 95	resubcld 8710	. . . . . . 7 |- ( ph -> ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) e. RR )
97		rpre 10072	. . . . . . . . . . . . 13 |- ( ( 2 x. N ) e. RR+ -> ( 2 x. N ) e. RR )
98		rpge0 10078	. . . . . . . . . . . . 13 |- ( ( 2 x. N ) e. RR+ -> 0 <_ ( 2 x. N ) )
99	97, 98	resqrtcld 11946	. . . . . . . . . . . 12 |- ( ( 2 x. N ) e. RR+ -> ( sqr ` ( 2 x. N ) ) e. RR )
100	82, 99	syl 14	. . . . . . . . . . 11 |- ( ph -> ( sqr ` ( 2 x. N ) ) e. RR )
101		3nn 9472	. . . . . . . . . . 11 |- 3 e. NN
102		nndivre 9343	. . . . . . . . . . 11 |- ( ( ( sqr ` ( 2 x. N ) ) e. RR /\ 3 e. NN ) -> ( ( sqr ` ( 2 x. N ) ) / 3 ) e. RR )
103	100, 101, 102	sylancl 417	. . . . . . . . . 10 |- ( ph -> ( ( sqr ` ( 2 x. N ) ) / 3 ) e. RR )
104		2re 9377	. . . . . . . . . 10 |- 2 e. RR
105		readdcl 8306	. . . . . . . . . 10 |- ( ( ( ( sqr ` ( 2 x. N ) ) / 3 ) e. RR /\ 2 e. RR ) -> ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) e. RR )
106	103, 104, 105	sylancl 417	. . . . . . . . 9 |- ( ph -> ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) e. RR )
107	82	relogcld 16044	. . . . . . . . 9 |- ( ph -> ( log ` ( 2 x. N ) ) e. RR )
108	106, 107	remulcld 8357	. . . . . . . 8 |- ( ph -> ( ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) e. RR )
109		4re 9384	. . . . . . . . . . . 12 |- 4 e. RR
110		remulcl 8308	. . . . . . . . . . . 12 |- ( ( 4 e. RR /\ N e. RR ) -> ( 4 x. N ) e. RR )
111	109, 36, 110	sylancr 418	. . . . . . . . . . 11 |- ( ph -> ( 4 x. N ) e. RR )
112		nndivre 9343	. . . . . . . . . . 11 |- ( ( ( 4 x. N ) e. RR /\ 3 e. NN ) -> ( ( 4 x. N ) / 3 ) e. RR )
113	111, 101, 112	sylancl 417	. . . . . . . . . 10 |- ( ph -> ( ( 4 x. N ) / 3 ) e. RR )
114		5re 9386	. . . . . . . . . 10 |- 5 e. RR
115		resubcl 8592	. . . . . . . . . 10 |- ( ( ( ( 4 x. N ) / 3 ) e. RR /\ 5 e. RR ) -> ( ( ( 4 x. N ) / 3 ) - 5 ) e. RR )
116	113, 114, 115	sylancl 417	. . . . . . . . 9 |- ( ph -> ( ( ( 4 x. N ) / 3 ) - 5 ) e. RR )
117		remulcl 8308	. . . . . . . . 9 |- ( ( ( ( ( 4 x. N ) / 3 ) - 5 ) e. RR /\ ( log ` 2 ) e. RR ) -> ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) e. RR )
118	116, 79, 117	sylancl 417	. . . . . . . 8 |- ( ph -> ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) e. RR )
119	108, 118	readdcld 8356	. . . . . . 7 |- ( ph -> ( ( ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) + ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) e. RR )
120		remulcl 8308	. . . . . . . . 9 |- ( ( ( ( 4 x. N ) / 3 ) e. RR /\ ( log ` 2 ) e. RR ) -> ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) e. RR )
121	113, 79, 120	sylancl 417	. . . . . . . 8 |- ( ph -> ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) e. RR )
122	121, 95	resubcld 8710	. . . . . . 7 |- ( ph -> ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) e. RR )
123	8	nnzd 9772	. . . . . . . . . . 11 |- ( ph -> N e. ZZ )
124		df-5 9369	. . . . . . . . . . . 12 |- 5 = ( 4 + 1 )
125	109	a1i 9	. . . . . . . . . . . . . 14 |- ( ph -> 4 e. RR )
126		6nn 9475	. . . . . . . . . . . . . . . 16 |- 6 e. NN
127		4nn0 9587	. . . . . . . . . . . . . . . 16 |- 4 e. NN0
128		4lt10 9922	. . . . . . . . . . . . . . . 16 |- 4 < ; 1 0
129	126, 127, 127, 128	declti 9824	. . . . . . . . . . . . . . 15 |- 4 < ; 6 4
130	129	a1i 9	. . . . . . . . . . . . . 14 |- ( ph -> 4 < ; 6 4 )
131	125, 35, 36, 130, 1	lttrd 8454	. . . . . . . . . . . . 13 |- ( ph -> 4 < N )
132		4z 9679	. . . . . . . . . . . . . 14 |- 4 e. ZZ
133		zltp1le 9704	. . . . . . . . . . . . . 14 |- ( ( 4 e. ZZ /\ N e. ZZ ) -> ( 4 < N <-> ( 4 + 1 ) <_ N ) )
134	132, 123, 133	sylancr 418	. . . . . . . . . . . . 13 |- ( ph -> ( 4 < N <-> ( 4 + 1 ) <_ N ) )
135	131, 134	mpbid 147	. . . . . . . . . . . 12 |- ( ph -> ( 4 + 1 ) <_ N )
136	124, 135	eqbrtrid 4165	. . . . . . . . . . 11 |- ( ph -> 5 <_ N )
137		5nn 9474	. . . . . . . . . . . . 13 |- 5 e. NN
138	137	nnzi 9670	. . . . . . . . . . . 12 |- 5 e. ZZ
139	138	eluz1i 9939	. . . . . . . . . . 11 |- ( N e. ( ZZ>= ` 5 ) <-> ( N e. ZZ /\ 5 <_ N ) )
140	123, 136, 139	sylanbrc 421	. . . . . . . . . 10 |- ( ph -> N e. ( ZZ>= ` 5 ) )
141		bposlem9.5	. . . . . . . . . . 11 |- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
142		breq2 4134	. . . . . . . . . . . . 13 |- ( p = q -> ( N < p <-> N < q ) )
143		breq1 4133	. . . . . . . . . . . . 13 |- ( p = q -> ( p <_ ( 2 x. N ) <-> q <_ ( 2 x. N ) ) )
144	142, 143	anbi12d 477	. . . . . . . . . . . 12 |- ( p = q -> ( ( N < p /\ p <_ ( 2 x. N ) ) <-> ( N < q /\ q <_ ( 2 x. N ) ) ) )
145	144	cbvrexvw 2791	. . . . . . . . . . 11 |- ( E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) <-> E. q e. Prime ( N < q /\ q <_ ( 2 x. N ) ) )
146	141, 145	sylnib 687	. . . . . . . . . 10 |- ( ph -> -. E. q e. Prime ( N < q /\ q <_ ( 2 x. N ) ) )
147		eqid 2238	. . . . . . . . . 10 |- ( 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 ) )
148		eqid 2238	. . . . . . . . . 10 |- ( |_ ` ( ( 2 x. N ) / 3 ) ) = ( |_ ` ( ( 2 x. N ) / 3 ) )
149		eqid 2238	. . . . . . . . . 10 |- ( |_ ` ( sqr ` ( 2 x. N ) ) ) = ( |_ ` ( sqr ` ( 2 x. N ) ) )
150	140, 146, 147, 148, 149	bposlem6 16245	. . . . . . . . 9 |- ( ph -> ( ( 4 ^ N ) / N ) < ( ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )
151		reexplog 16033	. . . . . . . . . . . 12 |- ( ( 4 e. RR+ /\ N e. ZZ ) -> ( 4 ^ N ) = ( exp ` ( N x. ( log ` 4 ) ) ) )
152	90, 123, 151	sylancr 418	. . . . . . . . . . 11 |- ( ph -> ( 4 ^ N ) = ( exp ` ( N x. ( log ` 4 ) ) ) )
153	62	reeflogd 16045	. . . . . . . . . . . 12 |- ( ph -> ( exp ` ( log ` N ) ) = N )
154	153	eqcomd 2244	. . . . . . . . . . 11 |- ( ph -> N = ( exp ` ( log ` N ) ) )
155	152, 154	oveq12d 6103	. . . . . . . . . 10 |- ( ph -> ( ( 4 ^ N ) / N ) = ( ( exp ` ( N x. ( log ` 4 ) ) ) / ( exp ` ( log ` N ) ) ) )
156	94	recnd 8355	. . . . . . . . . . 11 |- ( ph -> ( N x. ( log ` 4 ) ) e. CC )
157	95	recnd 8355	. . . . . . . . . . 11 |- ( ph -> ( log ` N ) e. CC )
158		efsub 12467	. . . . . . . . . . 11 |- ( ( ( 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 ) ) ) )
159	156, 157, 158	syl2anc 415	. . . . . . . . . 10 |- ( ph -> ( exp ` ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) ) = ( ( exp ` ( N x. ( log ` 4 ) ) ) / ( exp ` ( log ` N ) ) ) )
160	155, 159	eqtr4d 2274	. . . . . . . . 9 |- ( ph -> ( ( 4 ^ N ) / N ) = ( exp ` ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) ) )
161	106	recnd 8355	. . . . . . . . . . . 12 |- ( ph -> ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) e. CC )
162		rpcxpef 16059	. . . . . . . . . . . 12 |- ( ( ( 2 x. N ) e. RR+ /\ ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) e. CC ) -> ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) = ( exp ` ( ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) ) )
163	82, 161, 162	syl2anc 415	. . . . . . . . . . 11 |- ( ph -> ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) = ( exp ` ( ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) ) )
164	116	recnd 8355	. . . . . . . . . . . 12 |- ( ph -> ( ( ( 4 x. N ) / 3 ) - 5 ) e. CC )
165		rpcxpef 16059	. . . . . . . . . . . 12 |- ( ( 2 e. RR+ /\ ( ( ( 4 x. N ) / 3 ) - 5 ) e. CC ) -> ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) = ( exp ` ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) )
166	77, 164, 165	sylancr 418	. . . . . . . . . . 11 |- ( ph -> ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) = ( exp ` ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) )
167	163, 166	oveq12d 6103	. . . . . . . . . 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 ) ) ) ) x. ( exp ` ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) ) ) )
168	108	recnd 8355	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) e. CC )
169	118	recnd 8355	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) e. CC )
170		efadd 12461	. . . . . . . . . . 11 |- ( ( ( ( ( ( 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 ) ) ) ) )
171	168, 169, 170	syl2anc 415	. . . . . . . . . 10 |- ( 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 ) ) ) ) )
172	167, 171	eqtr4d 2274	. . . . . . . . 9 |- ( 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 ) ) ) ) )
173	150, 160, 172	3brtr3d 4161	. . . . . . . 8 |- ( 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 ) ) ) ) )
174		eflt 15935	. . . . . . . . 9 |- ( ( ( ( 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 ) ) ) ) ) )
175	96, 119, 174	syl2anc 415	. . . . . . . 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 ) ) ) <-> ( 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 ) ) ) ) ) )
176	173, 175	mpbird 167	. . . . . . 7 |- ( 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 ) ) ) )
177	96, 119, 122, 176	ltsub1dd 8887	. . . . . 6 |- ( 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 ) ) ) )
178		2cn 9378	. . . . . . . . . . 11 |- 2 e. CC
179	36	recnd 8355	. . . . . . . . . . 11 |- ( ph -> N e. CC )
180		mulcom 8309	. . . . . . . . . . 11 |- ( ( 2 e. CC /\ N e. CC ) -> ( 2 x. N ) = ( N x. 2 ) )
181	178, 179, 180	sylancr 418	. . . . . . . . . 10 |- ( ph -> ( 2 x. N ) = ( N x. 2 ) )
182	181	oveq1d 6100	. . . . . . . . 9 |- ( ph -> ( ( 2 x. N ) x. ( log ` 2 ) ) = ( ( N x. 2 ) x. ( log ` 2 ) ) )
183	79	recni 8339	. . . . . . . . . . . 12 |- ( log ` 2 ) e. CC
184		mulass 8311	. . . . . . . . . . . 12 |- ( ( N e. CC /\ 2 e. CC /\ ( log ` 2 ) e. CC ) -> ( ( N x. 2 ) x. ( log ` 2 ) ) = ( N x. ( 2 x. ( log ` 2 ) ) ) )
185	178, 183, 184	mp3an23 1370	. . . . . . . . . . 11 |- ( N e. CC -> ( ( N x. 2 ) x. ( log ` 2 ) ) = ( N x. ( 2 x. ( log ` 2 ) ) ) )
186	179, 185	syl 14	. . . . . . . . . 10 |- ( ph -> ( ( N x. 2 ) x. ( log ` 2 ) ) = ( N x. ( 2 x. ( log ` 2 ) ) ) )
187	183	2timesi 9437	. . . . . . . . . . . 12 |- ( 2 x. ( log ` 2 ) ) = ( ( log ` 2 ) + ( log ` 2 ) )
188		relogmul 16031	. . . . . . . . . . . . 13 |- ( ( 2 e. RR+ /\ 2 e. RR+ ) -> ( log ` ( 2 x. 2 ) ) = ( ( log ` 2 ) + ( log ` 2 ) ) )
189	77, 77, 188	mp2an 430	. . . . . . . . . . . 12 |- ( log ` ( 2 x. 2 ) ) = ( ( log ` 2 ) + ( log ` 2 ) )
190		2t2e4 9462	. . . . . . . . . . . . 13 |- ( 2 x. 2 ) = 4
191	190	fveq2i 5698	. . . . . . . . . . . 12 |- ( log ` ( 2 x. 2 ) ) = ( log ` 4 )
192	187, 189, 191	3eqtr2i 2265	. . . . . . . . . . 11 |- ( 2 x. ( log ` 2 ) ) = ( log ` 4 )
193	192	oveq2i 6096	. . . . . . . . . 10 |- ( N x. ( 2 x. ( log ` 2 ) ) ) = ( N x. ( log ` 4 ) )
194	186, 193	eqtrdi 2287	. . . . . . . . 9 |- ( ph -> ( ( N x. 2 ) x. ( log ` 2 ) ) = ( N x. ( log ` 4 ) ) )
195	182, 194	eqtrd 2271	. . . . . . . 8 |- ( ph -> ( ( 2 x. N ) x. ( log ` 2 ) ) = ( N x. ( log ` 4 ) ) )
196	195	oveq1d 6100	. . . . . . 7 |- ( 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 ) ) ) )
197	113	recnd 8355	. . . . . . . . . 10 |- ( ph -> ( ( 4 x. N ) / 3 ) e. CC )
198		3rp 10071	. . . . . . . . . . . 12 |- 3 e. RR+
199		rpdivcl 10091	. . . . . . . . . . . 12 |- ( ( ( 2 x. N ) e. RR+ /\ 3 e. RR+ ) -> ( ( 2 x. N ) / 3 ) e. RR+ )
200	82, 198, 199	sylancl 417	. . . . . . . . . . 11 |- ( ph -> ( ( 2 x. N ) / 3 ) e. RR+ )
201	200	rpcnd 10110	. . . . . . . . . 10 |- ( ph -> ( ( 2 x. N ) / 3 ) e. CC )
202		4p2e6 9451	. . . . . . . . . . . . . 14 |- ( 4 + 2 ) = 6
203	202	oveq1i 6095	. . . . . . . . . . . . 13 |- ( ( 4 + 2 ) x. N ) = ( 6 x. N )
204		4cn 9385	. . . . . . . . . . . . . 14 |- 4 e. CC
205		adddir 8318	. . . . . . . . . . . . . 14 |- ( ( 4 e. CC /\ 2 e. CC /\ N e. CC ) -> ( ( 4 + 2 ) x. N ) = ( ( 4 x. N ) + ( 2 x. N ) ) )
206	204, 178, 179, 205	mp3an12i 1382	. . . . . . . . . . . . 13 |- ( ph -> ( ( 4 + 2 ) x. N ) = ( ( 4 x. N ) + ( 2 x. N ) ) )
207	203, 206	eqtr3id 2285	. . . . . . . . . . . 12 |- ( ph -> ( 6 x. N ) = ( ( 4 x. N ) + ( 2 x. N ) ) )
208	207	oveq1d 6100	. . . . . . . . . . 11 |- ( ph -> ( ( 6 x. N ) / 3 ) = ( ( ( 4 x. N ) + ( 2 x. N ) ) / 3 ) )
209		6cn 9389	. . . . . . . . . . . . . 14 |- 6 e. CC
210		3cn 9382	. . . . . . . . . . . . . . 15 |- 3 e. CC
211		3ap0 9403	. . . . . . . . . . . . . . 15 |- 3 # 0
212	210, 211	pm3.2i 272	. . . . . . . . . . . . . 14 |- ( 3 e. CC /\ 3 # 0 )
213		div23ap 9024	. . . . . . . . . . . . . 14 |- ( ( 6 e. CC /\ N e. CC /\ ( 3 e. CC /\ 3 # 0 ) ) -> ( ( 6 x. N ) / 3 ) = ( ( 6 / 3 ) x. N ) )
214	209, 212, 213	mp3an13 1369	. . . . . . . . . . . . 13 |- ( N e. CC -> ( ( 6 x. N ) / 3 ) = ( ( 6 / 3 ) x. N ) )
215	179, 214	syl 14	. . . . . . . . . . . 12 |- ( ph -> ( ( 6 x. N ) / 3 ) = ( ( 6 / 3 ) x. N ) )
216		3t2e6 9464	. . . . . . . . . . . . . . 15 |- ( 3 x. 2 ) = 6
217	216	oveq1i 6095	. . . . . . . . . . . . . 14 |- ( ( 3 x. 2 ) / 3 ) = ( 6 / 3 )
218	178, 210, 211	divcanap3i 9091	. . . . . . . . . . . . . 14 |- ( ( 3 x. 2 ) / 3 ) = 2
219	217, 218	eqtr3i 2261	. . . . . . . . . . . . 13 |- ( 6 / 3 ) = 2
220	219	oveq1i 6095	. . . . . . . . . . . 12 |- ( ( 6 / 3 ) x. N ) = ( 2 x. N )
221	215, 220	eqtrdi 2287	. . . . . . . . . . 11 |- ( ph -> ( ( 6 x. N ) / 3 ) = ( 2 x. N ) )
222	111	recnd 8355	. . . . . . . . . . . 12 |- ( ph -> ( 4 x. N ) e. CC )
223		remulcl 8308	. . . . . . . . . . . . . 14 |- ( ( 2 e. RR /\ N e. RR ) -> ( 2 x. N ) e. RR )
224	104, 36, 223	sylancr 418	. . . . . . . . . . . . 13 |- ( ph -> ( 2 x. N ) e. RR )
225	224	recnd 8355	. . . . . . . . . . . 12 |- ( ph -> ( 2 x. N ) e. CC )
226		divdirap 9030	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) )
227	212, 226	mp3an3 1367	. . . . . . . . . . . 12 |- ( ( ( 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 ) ) )
228	222, 225, 227	syl2anc 415	. . . . . . . . . . 11 |- ( ph -> ( ( ( 4 x. N ) + ( 2 x. N ) ) / 3 ) = ( ( ( 4 x. N ) / 3 ) + ( ( 2 x. N ) / 3 ) ) )
229	208, 221, 228	3eqtr3d 2279	. . . . . . . . . 10 |- ( ph -> ( 2 x. N ) = ( ( ( 4 x. N ) / 3 ) + ( ( 2 x. N ) / 3 ) ) )
230	197, 201, 229	mvrladdd 8695	. . . . . . . . 9 |- ( ph -> ( ( 2 x. N ) - ( ( 4 x. N ) / 3 ) ) = ( ( 2 x. N ) / 3 ) )
231	230	oveq1d 6100	. . . . . . . 8 |- ( ph -> ( ( ( 2 x. N ) - ( ( 4 x. N ) / 3 ) ) x. ( log ` 2 ) ) = ( ( ( 2 x. N ) / 3 ) x. ( log ` 2 ) ) )
232	80	recnd 8355	. . . . . . . . 9 |- ( ph -> ( log ` 2 ) e. CC )
233	225, 197, 232	subdird 8744	. . . . . . . 8 |- ( ph -> ( ( ( 2 x. N ) - ( ( 4 x. N ) / 3 ) ) x. ( log ` 2 ) ) = ( ( ( 2 x. N ) x. ( log ` 2 ) ) - ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) ) )
234	231, 233	eqtr3d 2273	. . . . . . 7 |- ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( log ` 2 ) ) = ( ( ( 2 x. N ) x. ( log ` 2 ) ) - ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) ) )
235	121	recnd 8355	. . . . . . . 8 |- ( ph -> ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) e. CC )
236	156, 235, 157	nnncan2d 8674	. . . . . . 7 |- ( 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 ) ) ) )
237	196, 234, 236	3eqtr4d 2281	. . . . . 6 |- ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( log ` 2 ) ) = ( ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) - ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) ) )
238	103	recnd 8355	. . . . . . . . . 10 |- ( ph -> ( ( sqr ` ( 2 x. N ) ) / 3 ) e. CC )
239	178	a1i 9	. . . . . . . . . 10 |- ( ph -> 2 e. CC )
240	107	recnd 8355	. . . . . . . . . 10 |- ( ph -> ( log ` ( 2 x. N ) ) e. CC )
241	238, 239, 240	adddird 8352	. . . . . . . . 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 x. N ) ) ) ) )
242		relogmul 16031	. . . . . . . . . . . . 13 |- ( ( 2 e. RR+ /\ N e. RR+ ) -> ( log ` ( 2 x. N ) ) = ( ( log ` 2 ) + ( log ` N ) ) )
243	77, 62, 242	sylancr 418	. . . . . . . . . . . 12 |- ( ph -> ( log ` ( 2 x. N ) ) = ( ( log ` 2 ) + ( log ` N ) ) )
244	243	oveq2d 6101	. . . . . . . . . . 11 |- ( ph -> ( 2 x. ( log ` ( 2 x. N ) ) ) = ( 2 x. ( ( log ` 2 ) + ( log ` N ) ) ) )
245	239, 232, 157	adddid 8351	. . . . . . . . . . 11 |- ( ph -> ( 2 x. ( ( log ` 2 ) + ( log ` N ) ) ) = ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) )
246	244, 245	eqtrd 2271	. . . . . . . . . 10 |- ( ph -> ( 2 x. ( log ` ( 2 x. N ) ) ) = ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) )
247	246	oveq2d 6101	. . . . . . . . 9 |- ( 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 ) ) ) ) )
248	241, 247	eqtrd 2271	. . . . . . . 8 |- ( 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 ) ) ) ) )
249		5cn 9387	. . . . . . . . . . . 12 |- 5 e. CC
250	249	a1i 9	. . . . . . . . . . 11 |- ( ph -> 5 e. CC )
251	197, 250, 232	subdird 8744	. . . . . . . . . 10 |- ( ph -> ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) = ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( 5 x. ( log ` 2 ) ) ) )
252	251	oveq1d 6100	. . . . . . . . 9 |- ( 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 ) ) ) )
253	249, 183	mulcli 8332	. . . . . . . . . . 11 |- ( 5 x. ( log ` 2 ) ) e. CC
254	253	a1i 9	. . . . . . . . . 10 |- ( ph -> ( 5 x. ( log ` 2 ) ) e. CC )
255	235, 254, 157	nnncan1d 8673	. . . . . . . . 9 |- ( 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 ) ) ) )
256	252, 255	eqtrd 2271	. . . . . . . 8 |- ( ph -> ( ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) - ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) ) = ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) )
257	248, 256	oveq12d 6103	. . . . . . 7 |- ( 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 ) ) ) ) )
258	122	recnd 8355	. . . . . . . 8 |- ( ph -> ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) e. CC )
259	168, 169, 258	addsubassd 8659	. . . . . . 7 |- ( 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 ) ) ) ) )
260	249, 210, 183	subdiri 8737	. . . . . . . . . . . . 13 |- ( ( 5 - 3 ) x. ( log ` 2 ) ) = ( ( 5 x. ( log ` 2 ) ) - ( 3 x. ( log ` 2 ) ) )
261		3p2e5 9449	. . . . . . . . . . . . . . . 16 |- ( 3 + 2 ) = 5
262	261	oveq1i 6095	. . . . . . . . . . . . . . 15 |- ( ( 3 + 2 ) - 3 ) = ( 5 - 3 )
263		pncan2 8535	. . . . . . . . . . . . . . . 16 |- ( ( 3 e. CC /\ 2 e. CC ) -> ( ( 3 + 2 ) - 3 ) = 2 )
264	210, 178, 263	mp2an 430	. . . . . . . . . . . . . . 15 |- ( ( 3 + 2 ) - 3 ) = 2
265	262, 264	eqtr3i 2261	. . . . . . . . . . . . . 14 |- ( 5 - 3 ) = 2
266	265	oveq1i 6095	. . . . . . . . . . . . 13 |- ( ( 5 - 3 ) x. ( log ` 2 ) ) = ( 2 x. ( log ` 2 ) )
267	260, 266	eqtr3i 2261	. . . . . . . . . . . 12 |- ( ( 5 x. ( log ` 2 ) ) - ( 3 x. ( log ` 2 ) ) ) = ( 2 x. ( log ` 2 ) )
268	267	a1i 9	. . . . . . . . . . 11 |- ( ph -> ( ( 5 x. ( log ` 2 ) ) - ( 3 x. ( log ` 2 ) ) ) = ( 2 x. ( log ` 2 ) ) )
269		mulcl 8307	. . . . . . . . . . . . 13 |- ( ( 2 e. CC /\ ( log ` N ) e. CC ) -> ( 2 x. ( log ` N ) ) e. CC )
270	178, 157, 269	sylancr 418	. . . . . . . . . . . 12 |- ( ph -> ( 2 x. ( log ` N ) ) e. CC )
271		df-3 9367	. . . . . . . . . . . . . . . 16 |- 3 = ( 2 + 1 )
272	271	oveq1i 6095	. . . . . . . . . . . . . . 15 |- ( 3 x. ( log ` N ) ) = ( ( 2 + 1 ) x. ( log ` N ) )
273		1cnd 8343	. . . . . . . . . . . . . . . 16 |- ( ph -> 1 e. CC )
274	239, 273, 157	adddird 8352	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( 2 + 1 ) x. ( log ` N ) ) = ( ( 2 x. ( log ` N ) ) + ( 1 x. ( log ` N ) ) ) )
275	272, 274	eqtrid 2283	. . . . . . . . . . . . . 14 |- ( ph -> ( 3 x. ( log ` N ) ) = ( ( 2 x. ( log ` N ) ) + ( 1 x. ( log ` N ) ) ) )
276	157	mullidd 8345	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 x. ( log ` N ) ) = ( log ` N ) )
277	276	oveq2d 6101	. . . . . . . . . . . . . 14 |- ( ph -> ( ( 2 x. ( log ` N ) ) + ( 1 x. ( log ` N ) ) ) = ( ( 2 x. ( log ` N ) ) + ( log ` N ) ) )
278	275, 277	eqtrd 2271	. . . . . . . . . . . . 13 |- ( ph -> ( 3 x. ( log ` N ) ) = ( ( 2 x. ( log ` N ) ) + ( log ` N ) ) )
279	278	oveq1d 6100	. . . . . . . . . . . 12 |- ( ph -> ( ( 3 x. ( log ` N ) ) - ( 5 x. ( log ` 2 ) ) ) = ( ( ( 2 x. ( log ` N ) ) + ( log ` N ) ) - ( 5 x. ( log ` 2 ) ) ) )
280	270, 157, 254, 279	assraddsubd 8696	. . . . . . . . . . 11 |- ( ph -> ( ( 3 x. ( log ` N ) ) - ( 5 x. ( log ` 2 ) ) ) = ( ( 2 x. ( log ` N ) ) + ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) ) )
281	268, 280	oveq12d 6103	. . . . . . . . . 10 |- ( 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 ) ) ) ) ) )
282		relogdiv 16032	. . . . . . . . . . . . . 14 |- ( ( N e. RR+ /\ 2 e. RR+ ) -> ( log ` ( N / 2 ) ) = ( ( log ` N ) - ( log ` 2 ) ) )
283	62, 77, 282	sylancl 417	. . . . . . . . . . . . 13 |- ( ph -> ( log ` ( N / 2 ) ) = ( ( log ` N ) - ( log ` 2 ) ) )
284	283	oveq2d 6101	. . . . . . . . . . . 12 |- ( ph -> ( 3 x. ( log ` ( N / 2 ) ) ) = ( 3 x. ( ( log ` N ) - ( log ` 2 ) ) ) )
285		subdi 8714	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) )
286	210, 183, 285	mp3an13 1369	. . . . . . . . . . . . 13 |- ( ( log ` N ) e. CC -> ( 3 x. ( ( log ` N ) - ( log ` 2 ) ) ) = ( ( 3 x. ( log ` N ) ) - ( 3 x. ( log ` 2 ) ) ) )
287	157, 286	syl 14	. . . . . . . . . . . 12 |- ( ph -> ( 3 x. ( ( log ` N ) - ( log ` 2 ) ) ) = ( ( 3 x. ( log ` N ) ) - ( 3 x. ( log ` 2 ) ) ) )
288	284, 287	eqtrd 2271	. . . . . . . . . . 11 |- ( ph -> ( 3 x. ( log ` ( N / 2 ) ) ) = ( ( 3 x. ( log ` N ) ) - ( 3 x. ( log ` 2 ) ) ) )
289		div23ap 9024	. . . . . . . . . . . . . . . . 17 |- ( ( 2 e. CC /\ N e. CC /\ ( 3 e. CC /\ 3 # 0 ) ) -> ( ( 2 x. N ) / 3 ) = ( ( 2 / 3 ) x. N ) )
290	178, 212, 289	mp3an13 1369	. . . . . . . . . . . . . . . 16 |- ( N e. CC -> ( ( 2 x. N ) / 3 ) = ( ( 2 / 3 ) x. N ) )
291	179, 290	syl 14	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( 2 x. N ) / 3 ) = ( ( 2 / 3 ) x. N ) )
292		2ap0 9400	. . . . . . . . . . . . . . . . . 18 |- 2 # 0
293	210, 178, 210, 178, 292, 292	divmuldivapi 9105	. . . . . . . . . . . . . . . . 17 |- ( ( 3 / 2 ) x. ( 3 / 2 ) ) = ( ( 3 x. 3 ) / ( 2 x. 2 ) )
294		3t3e9 9466	. . . . . . . . . . . . . . . . . 18 |- ( 3 x. 3 ) = 9
295	294, 190	oveq12i 6097	. . . . . . . . . . . . . . . . 17 |- ( ( 3 x. 3 ) / ( 2 x. 2 ) ) = ( 9 / 4 )
296	293, 295	eqtr2i 2260	. . . . . . . . . . . . . . . 16 |- ( 9 / 4 ) = ( ( 3 / 2 ) x. ( 3 / 2 ) )
297	296	a1i 9	. . . . . . . . . . . . . . 15 |- ( ph -> ( 9 / 4 ) = ( ( 3 / 2 ) x. ( 3 / 2 ) ) )
298	291, 297	oveq12d 6103	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( 9 / 4 ) ) = ( ( ( 2 / 3 ) x. N ) x. ( ( 3 / 2 ) x. ( 3 / 2 ) ) ) )
299	178, 210, 211	divclapi 9087	. . . . . . . . . . . . . . 15 |- ( 2 / 3 ) e. CC
300	210, 178, 292	divclapi 9087	. . . . . . . . . . . . . . . 16 |- ( 3 / 2 ) e. CC
301		mul4 8460	. . . . . . . . . . . . . . . 16 |- ( ( ( ( 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 ) ) ) )
302	300, 300, 301	mpanr12 443	. . . . . . . . . . . . . . 15 |- ( ( ( 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 ) ) ) )
303	299, 179, 302	sylancr 418	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( 2 / 3 ) x. N ) x. ( ( 3 / 2 ) x. ( 3 / 2 ) ) ) = ( ( ( 2 / 3 ) x. ( 3 / 2 ) ) x. ( N x. ( 3 / 2 ) ) ) )
304		divcanap6 9052	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 2 e. CC /\ 2 # 0 ) /\ ( 3 e. CC /\ 3 # 0 ) ) -> ( ( 2 / 3 ) x. ( 3 / 2 ) ) = 1 )
305	178, 292, 210, 211, 304	mp4an 431	. . . . . . . . . . . . . . . . 17 |- ( ( 2 / 3 ) x. ( 3 / 2 ) ) = 1
306	305	oveq1i 6095	. . . . . . . . . . . . . . . 16 |- ( ( ( 2 / 3 ) x. ( 3 / 2 ) ) x. ( N x. ( 3 / 2 ) ) ) = ( 1 x. ( N x. ( 3 / 2 ) ) )
307		mulcl 8307	. . . . . . . . . . . . . . . . . 18 |- ( ( N e. CC /\ ( 3 / 2 ) e. CC ) -> ( N x. ( 3 / 2 ) ) e. CC )
308	179, 300, 307	sylancl 417	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( N x. ( 3 / 2 ) ) e. CC )
309	308	mullidd 8345	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 1 x. ( N x. ( 3 / 2 ) ) ) = ( N x. ( 3 / 2 ) ) )
310	306, 309	eqtrid 2283	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( 2 / 3 ) x. ( 3 / 2 ) ) x. ( N x. ( 3 / 2 ) ) ) = ( N x. ( 3 / 2 ) ) )
311	178, 292	pm3.2i 272	. . . . . . . . . . . . . . . . 17 |- ( 2 e. CC /\ 2 # 0 )
312		div12ap 9027	. . . . . . . . . . . . . . . . 17 |- ( ( N e. CC /\ 3 e. CC /\ ( 2 e. CC /\ 2 # 0 ) ) -> ( N x. ( 3 / 2 ) ) = ( 3 x. ( N / 2 ) ) )
313	210, 311, 312	mp3an23 1370	. . . . . . . . . . . . . . . 16 |- ( N e. CC -> ( N x. ( 3 / 2 ) ) = ( 3 x. ( N / 2 ) ) )
314	179, 313	syl 14	. . . . . . . . . . . . . . 15 |- ( ph -> ( N x. ( 3 / 2 ) ) = ( 3 x. ( N / 2 ) ) )
315	310, 314	eqtrd 2271	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( 2 / 3 ) x. ( 3 / 2 ) ) x. ( N x. ( 3 / 2 ) ) ) = ( 3 x. ( N / 2 ) ) )
316	298, 303, 315	3eqtrd 2275	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( 9 / 4 ) ) = ( 3 x. ( N / 2 ) ) )
317		fveq2 5695	. . . . . . . . . . . . . . 15 |- ( x = ( N / 2 ) -> ( log ` x ) = ( log ` ( N / 2 ) ) )
318		id 19	. . . . . . . . . . . . . . 15 |- ( x = ( N / 2 ) -> x = ( N / 2 ) )
319	317, 318	oveq12d 6103	. . . . . . . . . . . . . 14 |- ( x = ( N / 2 ) -> ( ( log ` x ) / x ) = ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) )
320	73	relogcld 16044	. . . . . . . . . . . . . . 15 |- ( ph -> ( log ` ( N / 2 ) ) e. RR )
321	320, 73	rerpdivcld 10140	. . . . . . . . . . . . . 14 |- ( ph -> ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) e. RR )
322	3, 319, 73, 321	fvmptd3 5799	. . . . . . . . . . . . 13 |- ( ph -> ( G ` ( N / 2 ) ) = ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) )
323	316, 322	oveq12d 6103	. . . . . . . . . . . 12 |- ( ph -> ( ( ( ( 2 x. N ) / 3 ) x. ( 9 / 4 ) ) x. ( G ` ( N / 2 ) ) ) = ( ( 3 x. ( N / 2 ) ) x. ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) ) )
324		9re 9394	. . . . . . . . . . . . . . . 16 |- 9 e. RR
325		4ap0 9406	. . . . . . . . . . . . . . . 16 |- 4 # 0
326	324, 109, 325	redivclapi 9112	. . . . . . . . . . . . . . 15 |- ( 9 / 4 ) e. RR
327	326	recni 8339	. . . . . . . . . . . . . 14 |- ( 9 / 4 ) e. CC
328	327	a1i 9	. . . . . . . . . . . . 13 |- ( ph -> ( 9 / 4 ) e. CC )
329	322, 321	eqeltrd 2315	. . . . . . . . . . . . . 14 |- ( ph -> ( G ` ( N / 2 ) ) e. RR )
330	329	recnd 8355	. . . . . . . . . . . . 13 |- ( ph -> ( G ` ( N / 2 ) ) e. CC )
331	201, 328, 330	mulassd 8350	. . . . . . . . . . . 12 |- ( ph -> ( ( ( ( 2 x. N ) / 3 ) x. ( 9 / 4 ) ) x. ( G ` ( N / 2 ) ) ) = ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) )
332	210	a1i 9	. . . . . . . . . . . . . 14 |- ( ph -> 3 e. CC )
333	73	rpcnd 10110	. . . . . . . . . . . . . 14 |- ( ph -> ( N / 2 ) e. CC )
334	320	recnd 8355	. . . . . . . . . . . . . . 15 |- ( ph -> ( log ` ( N / 2 ) ) e. CC )
335	73	rpap0d 10114	. . . . . . . . . . . . . . 15 |- ( ph -> ( N / 2 ) # 0 )
336	334, 333, 335	divclapd 9123	. . . . . . . . . . . . . 14 |- ( ph -> ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) e. CC )
337	332, 333, 336	mulassd 8350	. . . . . . . . . . . . 13 |- ( ph -> ( ( 3 x. ( N / 2 ) ) x. ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) ) = ( 3 x. ( ( N / 2 ) x. ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) ) ) )
338	334, 333, 335	divcanap2d 9125	. . . . . . . . . . . . . 14 |- ( ph -> ( ( N / 2 ) x. ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) ) = ( log ` ( N / 2 ) ) )
339	338	oveq2d 6101	. . . . . . . . . . . . 13 |- ( ph -> ( 3 x. ( ( N / 2 ) x. ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) ) ) = ( 3 x. ( log ` ( N / 2 ) ) ) )
340	337, 339	eqtrd 2271	. . . . . . . . . . . 12 |- ( ph -> ( ( 3 x. ( N / 2 ) ) x. ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) ) = ( 3 x. ( log ` ( N / 2 ) ) ) )
341	323, 331, 340	3eqtr3d 2279	. . . . . . . . . . 11 |- ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) = ( 3 x. ( log ` ( N / 2 ) ) ) )
342	210, 183	mulcli 8332	. . . . . . . . . . . . 13 |- ( 3 x. ( log ` 2 ) ) e. CC
343	342	a1i 9	. . . . . . . . . . . 12 |- ( ph -> ( 3 x. ( log ` 2 ) ) e. CC )
344		mulcl 8307	. . . . . . . . . . . . 13 |- ( ( 3 e. CC /\ ( log ` N ) e. CC ) -> ( 3 x. ( log ` N ) ) e. CC )
345	210, 157, 344	sylancr 418	. . . . . . . . . . . 12 |- ( ph -> ( 3 x. ( log ` N ) ) e. CC )
346	254, 343, 345	npncan3d 8675	. . . . . . . . . . 11 |- ( 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 ) ) ) )
347	288, 341, 346	3eqtr4d 2281	. . . . . . . . . 10 |- ( 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 ) ) ) ) )
348	104, 79	remulcli 8341	. . . . . . . . . . . . 13 |- ( 2 x. ( log ` 2 ) ) e. RR
349	348	recni 8339	. . . . . . . . . . . 12 |- ( 2 x. ( log ` 2 ) ) e. CC
350	349	a1i 9	. . . . . . . . . . 11 |- ( ph -> ( 2 x. ( log ` 2 ) ) e. CC )
351		subcl 8527	. . . . . . . . . . . 12 |- ( ( ( log ` N ) e. CC /\ ( 5 x. ( log ` 2 ) ) e. CC ) -> ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) e. CC )
352	157, 253, 351	sylancl 417	. . . . . . . . . . 11 |- ( ph -> ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) e. CC )
353	350, 270, 352	addassd 8349	. . . . . . . . . 10 |- ( 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 ) ) ) ) ) )
354	281, 347, 353	3eqtr4d 2281	. . . . . . . . 9 |- ( 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 ) ) ) ) )
355	354	oveq2d 6101	. . . . . . . 8 |- ( 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 ) ) ) ) ) )
356		mulcl 8307	. . . . . . . . . . 11 |- ( ( ( ( sqr ` ( 2 x. N ) ) / 3 ) e. CC /\ ( log ` 2 ) e. CC ) -> ( ( ( sqr ` ( 2 x. N ) ) / 3 ) x. ( log ` 2 ) ) e. CC )
357	238, 183, 356	sylancl 417	. . . . . . . . . 10 |- ( ph -> ( ( ( sqr ` ( 2 x. N ) ) / 3 ) x. ( log ` 2 ) ) e. CC )
358	238, 157	mulcld 8347	. . . . . . . . . 10 |- ( ph -> ( ( ( sqr ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) e. CC )
359		remulcl 8308	. . . . . . . . . . . . 13 |- ( ( ( 9 / 4 ) e. RR /\ ( G ` ( N / 2 ) ) e. RR ) -> ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) e. RR )
360	326, 329, 359	sylancr 418	. . . . . . . . . . . 12 |- ( ph -> ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) e. RR )
361	360	recnd 8355	. . . . . . . . . . 11 |- ( ph -> ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) e. CC )
362	201, 361	mulcld 8347	. . . . . . . . . 10 |- ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) e. CC )
363	357, 358, 362	addassd 8349	. . . . . . . . 9 |- ( 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 ) ) ) ) ) ) )
364	243	oveq2d 6101	. . . . . . . . . . 11 |- ( ph -> ( ( ( sqr ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) = ( ( ( sqr ` ( 2 x. N ) ) / 3 ) x. ( ( log ` 2 ) + ( log ` N ) ) ) )
365	238, 232, 157	adddid 8351	. . . . . . . . . . 11 |- ( 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 ) ) ) )
366	364, 365	eqtrd 2271	. . . . . . . . . 10 |- ( 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 ) ) ) )
367	366	oveq1d 6100	. . . . . . . . 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 ) ) + ( ( ( sqr ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) )
368	86	oveq2d 6101	. . . . . . . . . . 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 ) ) ) ) + ( ( log ` 2 ) / ( sqr ` ( 2 x. N ) ) ) ) ) )
369		fveq2 5695	. . . . . . . . . . . . . . . . . 18 |- ( x = ( sqr ` N ) -> ( log ` x ) = ( log ` ( sqr ` N ) ) )
370		id 19	. . . . . . . . . . . . . . . . . 18 |- ( x = ( sqr ` N ) -> x = ( sqr ` N ) )
371	369, 370	oveq12d 6103	. . . . . . . . . . . . . . . . 17 |- ( x = ( sqr ` N ) -> ( ( log ` x ) / x ) = ( ( log ` ( sqr ` N ) ) / ( sqr ` N ) ) )
372	63	relogcld 16044	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( log ` ( sqr ` N ) ) e. RR )
373	372, 63	rerpdivcld 10140	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( log ` ( sqr ` N ) ) / ( sqr ` N ) ) e. RR )
374	3, 371, 63, 373	fvmptd3 5799	. . . . . . . . . . . . . . . 16 |- ( ph -> ( G ` ( sqr ` N ) ) = ( ( log ` ( sqr ` N ) ) / ( sqr ` N ) ) )
375	374, 373	eqeltrd 2315	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` ( sqr ` N ) ) e. RR )
376		remulcl 8308	. . . . . . . . . . . . . . 15 |- ( ( ( sqr ` 2 ) e. RR /\ ( G ` ( sqr ` N ) ) e. RR ) -> ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) e. RR )
377	55, 375, 376	sylancr 418	. . . . . . . . . . . . . 14 |- ( ph -> ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) e. RR )
378	377, 360	readdcld 8356	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) e. RR )
379	378	recnd 8355	. . . . . . . . . . . 12 |- ( ph -> ( ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) e. CC )
380		rerpdivcl 10096	. . . . . . . . . . . . . 14 |- ( ( ( log ` 2 ) e. RR /\ ( sqr ` ( 2 x. N ) ) e. RR+ ) -> ( ( log ` 2 ) / ( sqr ` ( 2 x. N ) ) ) e. RR )
381	79, 83, 380	sylancr 418	. . . . . . . . . . . . 13 |- ( ph -> ( ( log ` 2 ) / ( sqr ` ( 2 x. N ) ) ) e. RR )
382	381	recnd 8355	. . . . . . . . . . . 12 |- ( ph -> ( ( log ` 2 ) / ( sqr ` ( 2 x. N ) ) ) e. CC )
383	201, 379, 382	adddid 8351	. . . . . . . . . . 11 |- ( 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 ) ) ) ) ) )
384	368, 383	eqtrd 2271	. . . . . . . . . 10 |- ( 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 ) ) ) ) ) )
385	377	recnd 8355	. . . . . . . . . . . . 13 |- ( ph -> ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) e. CC )
386	201, 385, 361	adddid 8351	. . . . . . . . . . . 12 |- ( 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 ) ) ) ) ) )
387	82	rpge0d 10112	. . . . . . . . . . . . . . . . . 18 |- ( ph -> 0 <_ ( 2 x. N ) )
388		remsqsqrt 11814	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 2 x. N ) e. RR /\ 0 <_ ( 2 x. N ) ) -> ( ( sqr ` ( 2 x. N ) ) x. ( sqr ` ( 2 x. N ) ) ) = ( 2 x. N ) )
389	224, 387, 388	syl2anc 415	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( sqr ` ( 2 x. N ) ) x. ( sqr ` ( 2 x. N ) ) ) = ( 2 x. N ) )
390	389	oveq1d 6100	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( sqr ` ( 2 x. N ) ) x. ( sqr ` ( 2 x. N ) ) ) / 3 ) = ( ( 2 x. N ) / 3 ) )
391	100	recnd 8355	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( sqr ` ( 2 x. N ) ) e. CC )
392	211	a1i 9	. . . . . . . . . . . . . . . . 17 |- ( ph -> 3 # 0 )
393	391, 391, 332, 392	div23apd 9161	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( sqr ` ( 2 x. N ) ) x. ( sqr ` ( 2 x. N ) ) ) / 3 ) = ( ( ( sqr ` ( 2 x. N ) ) / 3 ) x. ( sqr ` ( 2 x. N ) ) ) )
394	390, 393	eqtr3d 2273	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( 2 x. N ) / 3 ) = ( ( ( sqr ` ( 2 x. N ) ) / 3 ) x. ( sqr ` ( 2 x. N ) ) ) )
395	394	oveq1d 6100	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) ) )
396	238, 391, 385	mulassd 8350	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) ) ) )
397		0le2 9397	. . . . . . . . . . . . . . . . . . 19 |- 0 <_ 2
398	104, 397	pm3.2i 272	. . . . . . . . . . . . . . . . . 18 |- ( 2 e. RR /\ 0 <_ 2 )
399	62	rprege0d 10116	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( N e. RR /\ 0 <_ N ) )
400		sqrtmul 11817	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 2 e. RR /\ 0 <_ 2 ) /\ ( N e. RR /\ 0 <_ N ) ) -> ( sqr ` ( 2 x. N ) ) = ( ( sqr ` 2 ) x. ( sqr ` N ) ) )
401	398, 399, 400	sylancr 418	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( sqr ` ( 2 x. N ) ) = ( ( sqr ` 2 ) x. ( sqr ` N ) ) )
402	401	oveq1d 6100	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( sqr ` ( 2 x. N ) ) x. ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) ) = ( ( ( sqr ` 2 ) x. ( sqr ` N ) ) x. ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) ) )
403	55	recni 8339	. . . . . . . . . . . . . . . . . 18 |- ( sqr ` 2 ) e. CC
404	403	a1i 9	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( sqr ` 2 ) e. CC )
405	63	rpcnd 10110	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( sqr ` N ) e. CC )
406	375	recnd 8355	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( G ` ( sqr ` N ) ) e. CC )
407	404, 405, 404, 406	mul4d 8483	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) ) )
408		remsqsqrt 11814	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 2 e. RR /\ 0 <_ 2 ) -> ( ( sqr ` 2 ) x. ( sqr ` 2 ) ) = 2 )
409	104, 397, 408	mp2an 430	. . . . . . . . . . . . . . . . . . 19 |- ( ( sqr ` 2 ) x. ( sqr ` 2 ) ) = 2
410	409	a1i 9	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( sqr ` 2 ) x. ( sqr ` 2 ) ) = 2 )
411	374	oveq2d 6101	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( sqr ` N ) x. ( G ` ( sqr ` N ) ) ) = ( ( sqr ` N ) x. ( ( log ` ( sqr ` N ) ) / ( sqr ` N ) ) ) )
412	372	recnd 8355	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( log ` ( sqr ` N ) ) e. CC )
413	63	rpap0d 10114	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( sqr ` N ) # 0 )
414	412, 405, 413	divcanap2d 9125	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( sqr ` N ) x. ( ( log ` ( sqr ` N ) ) / ( sqr ` N ) ) ) = ( log ` ( sqr ` N ) ) )
415	411, 414	eqtrd 2271	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( sqr ` N ) x. ( G ` ( sqr ` N ) ) ) = ( log ` ( sqr ` N ) ) )
416	410, 415	oveq12d 6103	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( sqr ` 2 ) x. ( sqr ` 2 ) ) x. ( ( sqr ` N ) x. ( G ` ( sqr ` N ) ) ) ) = ( 2 x. ( log ` ( sqr ` N ) ) ) )
417	412	2timesd 9553	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( 2 x. ( log ` ( sqr ` N ) ) ) = ( ( log ` ( sqr ` N ) ) + ( log ` ( sqr ` N ) ) ) )
418	63, 63	relogmuld 16046	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( log ` ( ( sqr ` N ) x. ( sqr ` N ) ) ) = ( ( log ` ( sqr ` N ) ) + ( log ` ( sqr ` N ) ) ) )
419		remsqsqrt 11814	. . . . . . . . . . . . . . . . . . . 20 |- ( ( N e. RR /\ 0 <_ N ) -> ( ( sqr ` N ) x. ( sqr ` N ) ) = N )
420	399, 419	syl 14	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( sqr ` N ) x. ( sqr ` N ) ) = N )
421	420	fveq2d 5699	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( log ` ( ( sqr ` N ) x. ( sqr ` N ) ) ) = ( log ` N ) )
422	418, 421	eqtr3d 2273	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( log ` ( sqr ` N ) ) + ( log ` ( sqr ` N ) ) ) = ( log ` N ) )
423	416, 417, 422	3eqtrd 2275	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( sqr ` 2 ) x. ( sqr ` 2 ) ) x. ( ( sqr ` N ) x. ( G ` ( sqr ` N ) ) ) ) = ( log ` N ) )
424	402, 407, 423	3eqtrd 2275	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( sqr ` ( 2 x. N ) ) x. ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) ) = ( log ` N ) )
425	424	oveq2d 6101	. . . . . . . . . . . . . 14 |- ( 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 ) ) )
426	395, 396, 425	3eqtrd 2275	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) ) = ( ( ( sqr ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) )
427	426	oveq1d 6100	. . . . . . . . . . . 12 |- ( 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 ) ) ) ) ) )
428	386, 427	eqtrd 2271	. . . . . . . . . . 11 |- ( 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 ) ) ) ) ) )
429	394	oveq1d 6100	. . . . . . . . . . . 12 |- ( 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 ) ) ) ) )
430	238, 391, 382	mulassd 8350	. . . . . . . . . . . 12 |- ( 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 ) ) ) ) ) )
431	83	rpap0d 10114	. . . . . . . . . . . . . 14 |- ( ph -> ( sqr ` ( 2 x. N ) ) # 0 )
432	232, 391, 431	divcanap2d 9125	. . . . . . . . . . . . 13 |- ( ph -> ( ( sqr ` ( 2 x. N ) ) x. ( ( log ` 2 ) / ( sqr ` ( 2 x. N ) ) ) ) = ( log ` 2 ) )
433	432	oveq2d 6101	. . . . . . . . . . . 12 |- ( 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 ) ) )
434	429, 430, 433	3eqtrd 2275	. . . . . . . . . . 11 |- ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( ( log ` 2 ) / ( sqr ` ( 2 x. N ) ) ) ) = ( ( ( sqr ` ( 2 x. N ) ) / 3 ) x. ( log ` 2 ) ) )
435	428, 434	oveq12d 6103	. . . . . . . . . 10 |- ( 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 ) ) ) )
436	358, 362	addcld 8346	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( sqr ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) + ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) ) e. CC )
437	436, 357	addcomd 8479	. . . . . . . . . 10 |- ( 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 ) ) ) ) ) ) )
438	384, 435, 437	3eqtrd 2275	. . . . . . . . 9 |- ( 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 ) ) ) ) ) ) )
439	363, 367, 438	3eqtr4rd 2282	. . . . . . . 8 |- ( 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 ) ) ) ) ) )
440	238, 240	mulcld 8347	. . . . . . . . 9 |- ( ph -> ( ( ( sqr ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) e. CC )
441		addcl 8305	. . . . . . . . . 10 |- ( ( ( 2 x. ( log ` 2 ) ) e. CC /\ ( 2 x. ( log ` N ) ) e. CC ) -> ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) e. CC )
442	349, 270, 441	sylancr 418	. . . . . . . . 9 |- ( ph -> ( ( 2 x. ( log ` 2 ) ) + ( 2 x. ( log ` N ) ) ) e. CC )
443	440, 442, 352	addassd 8349	. . . . . . . 8 |- ( 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 ) ) ) ) ) )
444	355, 439, 443	3eqtr4d 2281	. . . . . . 7 |- ( 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 ) ) ) ) )
445	257, 259, 444	3eqtr4rd 2282	. . . . . 6 |- ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( F ` 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 ) ) ) )
446	177, 237, 445	3brtr4d 4162	. . . . 5 |- ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( log ` 2 ) ) < ( ( ( 2 x. N ) / 3 ) x. ( F ` N ) ) )
447	80, 87, 200	ltmul2d 10151	. . . . 5 |- ( ph -> ( ( log ` 2 ) < ( F ` N ) <-> ( ( ( 2 x. N ) / 3 ) x. ( log ` 2 ) ) < ( ( ( 2 x. N ) / 3 ) x. ( F ` N ) ) ) )
448	446, 447	mpbird 167	. . . 4 |- ( ph -> ( log ` 2 ) < ( F ` N ) )
449	45, 80, 87, 88, 448	lttrd 8454	. . 3 |- ( ph -> ( F ` ; 6 4 ) < ( F ` N ) )
450	45, 87, 449	ltnsymd 8448	. 2 |- ( ph -> -. ( F ` N ) < ( F ` ; 6 4 ) )
451	42, 450	pm2.21dd 629	1 |- ( ph -> ps )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   e. wcel 2209   E.wrex 2529   ifcif 3638   class class class wbr 4130   |-> cmpt 4192   ` cfv 5377  (class class class)co 6085   CCcc 8178   RRcr 8179   0cc0 8180   1c1 8181   + caddc 8183   x. cmul 8185   < clt 8361   <_ cle 8362   - cmin 8499   # cap 8912   / cdiv 9005   NNcn 9307   2c2 9358   3c3 9359   4c4 9360   5c5 9361   6c6 9362   8c8 9364   9c9 9365   ZZcz 9649  ;cdc 9782   ZZ>=cuz 9931   QQcq 10029   RR+crp 10065   |_cfl 10714   ^cexp 10990   _C cbc 11201   sqrcsqrt 11778   expce 12428   _eceu 12429   Primecprime 12904   pCnt cpc 13086   logclog 16017   ^c ccxp 16018

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-iinf 4735  ax-cnex 8271  ax-resscn 8272  ax-1cn 8273  ax-1re 8274  ax-icn 8275  ax-addcl 8276  ax-addrcl 8277  ax-mulcl 8278  ax-mulrcl 8279  ax-addcom 8280  ax-mulcom 8281  ax-addass 8282  ax-mulass 8283  ax-distr 8284  ax-i2m1 8285  ax-0lt1 8286  ax-1rid 8287  ax-0id 8288  ax-rnegex 8289  ax-precex 8290  ax-cnre 8291  ax-pre-ltirr 8292  ax-pre-ltwlin 8293  ax-pre-lttrn 8294  ax-pre-apti 8295  ax-pre-ltadd 8296  ax-pre-mulgt0 8297  ax-pre-mulext 8298  ax-arch 8299  ax-caucvg 8300  ax-pre-suploc 8301  ax-addf 8302  ax-mulf 8303

This proof depends on definitions:  df-bi 117  df-stab 843  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rmo 2536  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3639  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-disj 4107  df-br 4131  df-opab 4193  df-mpt 4194  df-tr 4230  df-id 4438  df-po 4441  df-iso 4442  df-iord 4511  df-on 4513  df-ilim 4514  df-suc 4516  df-iom 4738  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-isom 5386  df-riota 6038  df-ov 6088  df-oprab 6089  df-mpo 6090  df-of 6302  df-1st 6374  df-2nd 6375  df-recs 6576  df-irdg 6641  df-frec 6662  df-1o 6687  df-2o 6688  df-oadd 6691  df-er 6807  df-map 6924  df-pm 6925  df-en 7023  df-dom 7024  df-fin 7025  df-sup 7325  df-inf 7326  df-pnf 8363  df-mnf 8364  df-xr 8365  df-ltxr 8366  df-le 8367  df-sub 8501  df-neg 8502  df-reap 8906  df-ap 8913  df-div 9006  df-inn 9308  df-2 9366  df-3 9367  df-4 9368  df-5 9369  df-6 9370  df-7 9371  df-8 9372  df-9 9373  df-n0 9569  df-xnn0 9636  df-z 9650  df-dec 9783  df-uz 9932  df-q 10030  df-rp 10066  df-xneg 10185  df-xadd 10186  df-ioo 10305  df-ico 10307  df-icc 10308  df-fz 10423  df-fzo 10561  df-fl 10716  df-mod 10775  df-seqfrec 10900  df-exp 10991  df-fac 11180  df-bc 11202  df-ihash 11231  df-shft 11596  df-cj 11623  df-re 11624  df-im 11625  df-rsqrt 11780  df-abs 11781  df-clim 12064  df-sumdc 12139  df-ef 12434  df-e 12435  df-dvds 12574  df-gcd 12750  df-prm 12905  df-numer 12982  df-denom 12983  df-pc 13087  df-rest 13647  df-topgen 13666  df-psmet 14932  df-xmet 14933  df-met 14934  df-bl 14935  df-mopn 14936  df-top 15158  df-topon 15171  df-bases 15203  df-ntr 15256  df-cn 15348  df-cnp 15349  df-tx 15413  df-cncf 15731  df-limced 15816  df-dvap 15817  df-relog 16019  df-rpcxp 16020  df-logb 16109  df-cht 16165  df-ppi 16166

This theorem is used by:  bpos  16249