Theorem bposlem9 16319

Description: Lemma for bpos 16320. 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 9595	. . . . . 6 |- 6 e. NN0
5		4nn 9479	. . . . . 6 |- 4 e. NN
6	4, 5	decnncl 9811	. . . . 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 12462	. . . . . . . 8 |- _e e. RR
10		8re 9398	. . . . . . . 8 |- 8 e. RR
11		egt2lt3 12572	. . . . . . . . . 10 |- ( 2 < _e /\ _e < 3 )
12	11	simpri 113	. . . . . . . . 9 |- _e < 3
13		3lt8 9510	. . . . . . . . 9 |- 3 < 8
14		3re 9387	. . . . . . . . . 10 |- 3 e. RR
15	9, 14, 10	lttri 8437	. . . . . . . . 9 |- ( ( _e < 3 /\ 3 < 8 ) -> _e < 8 )
16	12, 13, 15	mp2an 430	. . . . . . . 8 |- _e < 8
17	9, 10, 16	ltleii 8435	. . . . . . 7 |- _e <_ 8
18		0re 8332	. . . . . . . . 9 |- 0 e. RR
19		epos 12573	. . . . . . . . 9 |- 0 < _e
20	18, 9, 19	ltleii 8435	. . . . . . . 8 |- 0 <_ _e
21		8pos 9416	. . . . . . . . 9 |- 0 < 8
22	18, 10, 21	ltleii 8435	. . . . . . . 8 |- 0 <_ 8
23		le2sq 11072	. . . . . . . 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 8344	. . . . . . . 8 |- 8 e. CC
27	26	sqvali 11077	. . . . . . 7 |- ( 8 ^ 2 ) = ( 8 x. 8 )
28		8t8e64 9913	. . . . . . 7 |- ( 8 x. 8 ) = ; 6 4
29	27, 28	eqtri 2259	. . . . . 6 |- ( 8 ^ 2 ) = ; 6 4
30	25, 29	breqtri 4156	. . . . 5 |- ( _e ^ 2 ) <_ ; 6 4
31	30	a1i 9	. . . 4 |- ( ph -> ( _e ^ 2 ) <_ ; 6 4 )
32	9	resqcli 11082	. . . . . 6 |- ( _e ^ 2 ) e. RR
33	32	a1i 9	. . . . 5 |- ( ph -> ( _e ^ 2 ) e. RR )
34	6	nnrei 9322	. . . . . 6 |- ; 6 4 e. RR
35	34	a1i 9	. . . . 5 |- ( ph -> ; 6 4 e. RR )
36	8	nnred 9326	. . . . 5 |- ( ph -> N e. RR )
37		ltle 8419	. . . . . . 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 8457	. . . 4 |- ( ph -> ( _e ^ 2 ) <_ N )
41	2, 3, 7, 8, 31, 40	bposlem7 16317	. . 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 16318	. . . . 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 5703	. . . . . . . 8 |- ( n = N -> ( G ` ( sqr ` n ) ) = ( G ` ( sqr ` N ) ) )
47	46	oveq2d 6104	. . . . . . 7 |- ( n = N -> ( ( sqr ` 2 ) x. ( G ` ( sqr ` n ) ) ) = ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) )
48		fvoveq1 6111	. . . . . . . 8 |- ( n = N -> ( G ` ( n / 2 ) ) = ( G ` ( N / 2 ) ) )
49	48	oveq2d 6104	. . . . . . 7 |- ( n = N -> ( ( 9 / 4 ) x. ( G ` ( n / 2 ) ) ) = ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) )
50	47, 49	oveq12d 6106	. . . . . 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 6096	. . . . . . . 8 |- ( n = N -> ( 2 x. n ) = ( 2 x. N ) )
52	51	fveq2d 5702	. . . . . . 7 |- ( n = N -> ( sqr ` ( 2 x. n ) ) = ( sqr ` ( 2 x. N ) ) )
53	52	oveq2d 6104	. . . . . 6 |- ( n = N -> ( ( log ` 2 ) / ( sqr ` ( 2 x. n ) ) ) = ( ( log ` 2 ) / ( sqr ` ( 2 x. N ) ) ) )
54	50, 53	oveq12d 6106	. . . . 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 12967	. . . . . . . . 9 |- ( sqr ` 2 ) e. RR
56	55	a1i 9	. . . . . . . 8 |- ( ph -> ( sqr ` 2 ) e. RR )
57		relogcl 16091	. . . . . . . . . . . 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 10146	. . . . . . . . . 10 |- ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) / x ) e. RR )
61	60, 3	fmptd 5865	. . . . . . . . 9 |- ( ph -> G : RR+ --> RR )
62	8	nnrpd 10112	. . . . . . . . . 10 |- ( ph -> N e. RR+ )
63	62	rpsqrtcld 11947	. . . . . . . . 9 |- ( ph -> ( sqr ` N ) e. RR+ )
64	61, 63	ffvelcdmd 5847	. . . . . . . 8 |- ( ph -> ( G ` ( sqr ` N ) ) e. RR )
65	56, 64	remulcld 8362	. . . . . . 7 |- ( ph -> ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) e. RR )
66		9nn 9484	. . . . . . . . . . . 12 |- 9 e. NN
67	66	nnzi 9676	. . . . . . . . . . 11 |- 9 e. ZZ
68		znq 10040	. . . . . . . . . . 11 |- ( ( 9 e. ZZ /\ 4 e. NN ) -> ( 9 / 4 ) e. QQ )
69	67, 5, 68	mp2an 430	. . . . . . . . . 10 |- ( 9 / 4 ) e. QQ
70		qre 10041	. . . . . . . . . 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 10127	. . . . . . . . 9 |- ( ph -> ( N / 2 ) e. RR+ )
74	61, 73	ffvelcdmd 5847	. . . . . . . 8 |- ( ph -> ( G ` ( N / 2 ) ) e. RR )
75	72, 74	remulcld 8362	. . . . . . 7 |- ( ph -> ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) e. RR )
76	65, 75	readdcld 8361	. . . . . 6 |- ( ph -> ( ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) e. RR )
77		2rp 10076	. . . . . . . . 9 |- 2 e. RR+
78		relogcl 16091	. . . . . . . . 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 10096	. . . . . . . . 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 11947	. . . . . . 7 |- ( ph -> ( sqr ` ( 2 x. N ) ) e. RR+ )
84	80, 83	rerpdivcld 10146	. . . . . 6 |- ( ph -> ( ( log ` 2 ) / ( sqr ` ( 2 x. N ) ) ) e. RR )
85	76, 84	readdcld 8361	. . . . 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 5802	. . . 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 10081	. . . . . . . . . . 11 |- ( 4 e. NN -> 4 e. RR+ )
90	5, 89	ax-mp 5	. . . . . . . . . 10 |- 4 e. RR+
91		relogcl 16091	. . . . . . . . . 10 |- ( 4 e. RR+ -> ( log ` 4 ) e. RR )
92	90, 91	ax-mp 5	. . . . . . . . 9 |- ( log ` 4 ) e. RR
93		remulcl 8313	. . . . . . . . 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 16112	. . . . . . . 8 |- ( ph -> ( log ` N ) e. RR )
96	94, 95	resubcld 8715	. . . . . . 7 |- ( ph -> ( ( N x. ( log ` 4 ) ) - ( log ` N ) ) e. RR )
97		rpre 10078	. . . . . . . . . . . . 13 |- ( ( 2 x. N ) e. RR+ -> ( 2 x. N ) e. RR )
98		rpge0 10084	. . . . . . . . . . . . 13 |- ( ( 2 x. N ) e. RR+ -> 0 <_ ( 2 x. N ) )
99	97, 98	resqrtcld 11952	. . . . . . . . . . . 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 9478	. . . . . . . . . . 11 |- 3 e. NN
102		nndivre 9349	. . . . . . . . . . 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 9383	. . . . . . . . . 10 |- 2 e. RR
105		readdcl 8311	. . . . . . . . . 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 16112	. . . . . . . . 9 |- ( ph -> ( log ` ( 2 x. N ) ) e. RR )
108	106, 107	remulcld 8362	. . . . . . . 8 |- ( ph -> ( ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) e. RR )
109		4re 9390	. . . . . . . . . . . 12 |- 4 e. RR
110		remulcl 8313	. . . . . . . . . . . 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 9349	. . . . . . . . . . 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 9392	. . . . . . . . . 10 |- 5 e. RR
115		resubcl 8597	. . . . . . . . . 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 8313	. . . . . . . . 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 8361	. . . . . . 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 8313	. . . . . . . . 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 8715	. . . . . . 7 |- ( ph -> ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) e. RR )
123	8	nnzd 9778	. . . . . . . . . . 11 |- ( ph -> N e. ZZ )
124		df-5 9375	. . . . . . . . . . . 12 |- 5 = ( 4 + 1 )
125	109	a1i 9	. . . . . . . . . . . . . 14 |- ( ph -> 4 e. RR )
126		6nn 9481	. . . . . . . . . . . . . . . 16 |- 6 e. NN
127		4nn0 9593	. . . . . . . . . . . . . . . 16 |- 4 e. NN0
128		4lt10 9928	. . . . . . . . . . . . . . . 16 |- 4 < ; 1 0
129	126, 127, 127, 128	declti 9830	. . . . . . . . . . . . . . 15 |- 4 < ; 6 4
130	129	a1i 9	. . . . . . . . . . . . . 14 |- ( ph -> 4 < ; 6 4 )
131	125, 35, 36, 130, 1	lttrd 8459	. . . . . . . . . . . . 13 |- ( ph -> 4 < N )
132		4z 9685	. . . . . . . . . . . . . 14 |- 4 e. ZZ
133		zltp1le 9710	. . . . . . . . . . . . . 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 4166	. . . . . . . . . . 11 |- ( ph -> 5 <_ N )
137		5nn 9480	. . . . . . . . . . . . 13 |- 5 e. NN
138	137	nnzi 9676	. . . . . . . . . . . 12 |- 5 e. ZZ
139	138	eluz1i 9945	. . . . . . . . . . 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 4135	. . . . . . . . . . . . 13 |- ( p = q -> ( N < p <-> N < q ) )
143		breq1 4134	. . . . . . . . . . . . 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 16316	. . . . . . . . 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 16101	. . . . . . . . . . . 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 16113	. . . . . . . . . . . 12 |- ( ph -> ( exp ` ( log ` N ) ) = N )
154	153	eqcomd 2244	. . . . . . . . . . 11 |- ( ph -> N = ( exp ` ( log ` N ) ) )
155	152, 154	oveq12d 6106	. . . . . . . . . 10 |- ( ph -> ( ( 4 ^ N ) / N ) = ( ( exp ` ( N x. ( log ` 4 ) ) ) / ( exp ` ( log ` N ) ) ) )
156	94	recnd 8360	. . . . . . . . . . 11 |- ( ph -> ( N x. ( log ` 4 ) ) e. CC )
157	95	recnd 8360	. . . . . . . . . . 11 |- ( ph -> ( log ` N ) e. CC )
158		efsub 12473	. . . . . . . . . . 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 8360	. . . . . . . . . . . 12 |- ( ph -> ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) e. CC )
162		rpcxpef 16127	. . . . . . . . . . . 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 8360	. . . . . . . . . . . 12 |- ( ph -> ( ( ( 4 x. N ) / 3 ) - 5 ) e. CC )
165		rpcxpef 16127	. . . . . . . . . . . 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 6106	. . . . . . . . . 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 8360	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) x. ( log ` ( 2 x. N ) ) ) e. CC )
169	118	recnd 8360	. . . . . . . . . . 11 |- ( ph -> ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) e. CC )
170		efadd 12467	. . . . . . . . . . 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 4162	. . . . . . . 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 16001	. . . . . . . . 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 8892	. . . . . 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 9384	. . . . . . . . . . 11 |- 2 e. CC
179	36	recnd 8360	. . . . . . . . . . 11 |- ( ph -> N e. CC )
180		mulcom 8314	. . . . . . . . . . 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 6103	. . . . . . . . 9 |- ( ph -> ( ( 2 x. N ) x. ( log ` 2 ) ) = ( ( N x. 2 ) x. ( log ` 2 ) ) )
183	79	recni 8344	. . . . . . . . . . . 12 |- ( log ` 2 ) e. CC
184		mulass 8316	. . . . . . . . . . . 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 9443	. . . . . . . . . . . 12 |- ( 2 x. ( log ` 2 ) ) = ( ( log ` 2 ) + ( log ` 2 ) )
188		relogmul 16099	. . . . . . . . . . . . 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 9468	. . . . . . . . . . . . 13 |- ( 2 x. 2 ) = 4
191	190	fveq2i 5701	. . . . . . . . . . . 12 |- ( log ` ( 2 x. 2 ) ) = ( log ` 4 )
192	187, 189, 191	3eqtr2i 2265	. . . . . . . . . . 11 |- ( 2 x. ( log ` 2 ) ) = ( log ` 4 )
193	192	oveq2i 6099	. . . . . . . . . 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 6103	. . . . . . 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 8360	. . . . . . . . . 10 |- ( ph -> ( ( 4 x. N ) / 3 ) e. CC )
198		3rp 10077	. . . . . . . . . . . 12 |- 3 e. RR+
199		rpdivcl 10097	. . . . . . . . . . . 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 10116	. . . . . . . . . 10 |- ( ph -> ( ( 2 x. N ) / 3 ) e. CC )
202		4p2e6 9457	. . . . . . . . . . . . . 14 |- ( 4 + 2 ) = 6
203	202	oveq1i 6098	. . . . . . . . . . . . 13 |- ( ( 4 + 2 ) x. N ) = ( 6 x. N )
204		4cn 9391	. . . . . . . . . . . . . 14 |- 4 e. CC
205		adddir 8323	. . . . . . . . . . . . . 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 6103	. . . . . . . . . . 11 |- ( ph -> ( ( 6 x. N ) / 3 ) = ( ( ( 4 x. N ) + ( 2 x. N ) ) / 3 ) )
209		6cn 9395	. . . . . . . . . . . . . 14 |- 6 e. CC
210		3cn 9388	. . . . . . . . . . . . . . 15 |- 3 e. CC
211		3ap0 9409	. . . . . . . . . . . . . . 15 |- 3 # 0
212	210, 211	pm3.2i 272	. . . . . . . . . . . . . 14 |- ( 3 e. CC /\ 3 # 0 )
213		div23ap 9029	. . . . . . . . . . . . . 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 9470	. . . . . . . . . . . . . . 15 |- ( 3 x. 2 ) = 6
217	216	oveq1i 6098	. . . . . . . . . . . . . 14 |- ( ( 3 x. 2 ) / 3 ) = ( 6 / 3 )
218	178, 210, 211	divcanap3i 9096	. . . . . . . . . . . . . 14 |- ( ( 3 x. 2 ) / 3 ) = 2
219	217, 218	eqtr3i 2261	. . . . . . . . . . . . 13 |- ( 6 / 3 ) = 2
220	219	oveq1i 6098	. . . . . . . . . . . 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 8360	. . . . . . . . . . . 12 |- ( ph -> ( 4 x. N ) e. CC )
223		remulcl 8313	. . . . . . . . . . . . . 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 8360	. . . . . . . . . . . 12 |- ( ph -> ( 2 x. N ) e. CC )
226		divdirap 9035	. . . . . . . . . . . . 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 8700	. . . . . . . . 9 |- ( ph -> ( ( 2 x. N ) - ( ( 4 x. N ) / 3 ) ) = ( ( 2 x. N ) / 3 ) )
231	230	oveq1d 6103	. . . . . . . 8 |- ( ph -> ( ( ( 2 x. N ) - ( ( 4 x. N ) / 3 ) ) x. ( log ` 2 ) ) = ( ( ( 2 x. N ) / 3 ) x. ( log ` 2 ) ) )
232	80	recnd 8360	. . . . . . . . 9 |- ( ph -> ( log ` 2 ) e. CC )
233	225, 197, 232	subdird 8749	. . . . . . . 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 8360	. . . . . . . 8 |- ( ph -> ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) e. CC )
236	156, 235, 157	nnncan2d 8679	. . . . . . 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 8360	. . . . . . . . . 10 |- ( ph -> ( ( sqr ` ( 2 x. N ) ) / 3 ) e. CC )
239	178	a1i 9	. . . . . . . . . 10 |- ( ph -> 2 e. CC )
240	107	recnd 8360	. . . . . . . . . 10 |- ( ph -> ( log ` ( 2 x. N ) ) e. CC )
241	238, 239, 240	adddird 8357	. . . . . . . . 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 16099	. . . . . . . . . . . . 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 6104	. . . . . . . . . . 11 |- ( ph -> ( 2 x. ( log ` ( 2 x. N ) ) ) = ( 2 x. ( ( log ` 2 ) + ( log ` N ) ) ) )
245	239, 232, 157	adddid 8356	. . . . . . . . . . 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 6104	. . . . . . . . 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 9393	. . . . . . . . . . . 12 |- 5 e. CC
250	249	a1i 9	. . . . . . . . . . 11 |- ( ph -> 5 e. CC )
251	197, 250, 232	subdird 8749	. . . . . . . . . 10 |- ( ph -> ( ( ( ( 4 x. N ) / 3 ) - 5 ) x. ( log ` 2 ) ) = ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( 5 x. ( log ` 2 ) ) ) )
252	251	oveq1d 6103	. . . . . . . . 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 8337	. . . . . . . . . . 11 |- ( 5 x. ( log ` 2 ) ) e. CC
254	253	a1i 9	. . . . . . . . . 10 |- ( ph -> ( 5 x. ( log ` 2 ) ) e. CC )
255	235, 254, 157	nnncan1d 8678	. . . . . . . . 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 6106	. . . . . . 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 8360	. . . . . . . 8 |- ( ph -> ( ( ( ( 4 x. N ) / 3 ) x. ( log ` 2 ) ) - ( log ` N ) ) e. CC )
259	168, 169, 258	addsubassd 8664	. . . . . . 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 8742	. . . . . . . . . . . . 13 |- ( ( 5 - 3 ) x. ( log ` 2 ) ) = ( ( 5 x. ( log ` 2 ) ) - ( 3 x. ( log ` 2 ) ) )
261		3p2e5 9455	. . . . . . . . . . . . . . . 16 |- ( 3 + 2 ) = 5
262	261	oveq1i 6098	. . . . . . . . . . . . . . 15 |- ( ( 3 + 2 ) - 3 ) = ( 5 - 3 )
263		pncan2 8540	. . . . . . . . . . . . . . . 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 6098	. . . . . . . . . . . . 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 8312	. . . . . . . . . . . . 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 9373	. . . . . . . . . . . . . . . 16 |- 3 = ( 2 + 1 )
272	271	oveq1i 6098	. . . . . . . . . . . . . . 15 |- ( 3 x. ( log ` N ) ) = ( ( 2 + 1 ) x. ( log ` N ) )
273		1cnd 8348	. . . . . . . . . . . . . . . 16 |- ( ph -> 1 e. CC )
274	239, 273, 157	adddird 8357	. . . . . . . . . . . . . . 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 8350	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 x. ( log ` N ) ) = ( log ` N ) )
277	276	oveq2d 6104	. . . . . . . . . . . . . 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 6103	. . . . . . . . . . . 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 8701	. . . . . . . . . . 11 |- ( ph -> ( ( 3 x. ( log ` N ) ) - ( 5 x. ( log ` 2 ) ) ) = ( ( 2 x. ( log ` N ) ) + ( ( log ` N ) - ( 5 x. ( log ` 2 ) ) ) ) )
281	268, 280	oveq12d 6106	. . . . . . . . . 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 16100	. . . . . . . . . . . . . 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 6104	. . . . . . . . . . . 12 |- ( ph -> ( 3 x. ( log ` ( N / 2 ) ) ) = ( 3 x. ( ( log ` N ) - ( log ` 2 ) ) ) )
285		subdi 8719	. . . . . . . . . . . . . 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 9029	. . . . . . . . . . . . . . . . 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 9406	. . . . . . . . . . . . . . . . . 18 |- 2 # 0
293	210, 178, 210, 178, 292, 292	divmuldivapi 9110	. . . . . . . . . . . . . . . . 17 |- ( ( 3 / 2 ) x. ( 3 / 2 ) ) = ( ( 3 x. 3 ) / ( 2 x. 2 ) )
294		3t3e9 9472	. . . . . . . . . . . . . . . . . 18 |- ( 3 x. 3 ) = 9
295	294, 190	oveq12i 6100	. . . . . . . . . . . . . . . . 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 6106	. . . . . . . . . . . . . 14 |- ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( 9 / 4 ) ) = ( ( ( 2 / 3 ) x. N ) x. ( ( 3 / 2 ) x. ( 3 / 2 ) ) ) )
299	178, 210, 211	divclapi 9092	. . . . . . . . . . . . . . 15 |- ( 2 / 3 ) e. CC
300	210, 178, 292	divclapi 9092	. . . . . . . . . . . . . . . 16 |- ( 3 / 2 ) e. CC
301		mul4 8465	. . . . . . . . . . . . . . . 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 9057	. . . . . . . . . . . . . . . . . 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 6098	. . . . . . . . . . . . . . . 16 |- ( ( ( 2 / 3 ) x. ( 3 / 2 ) ) x. ( N x. ( 3 / 2 ) ) ) = ( 1 x. ( N x. ( 3 / 2 ) ) )
307		mulcl 8312	. . . . . . . . . . . . . . . . . 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 8350	. . . . . . . . . . . . . . . 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 9032	. . . . . . . . . . . . . . . . 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 5698	. . . . . . . . . . . . . . 15 |- ( x = ( N / 2 ) -> ( log ` x ) = ( log ` ( N / 2 ) ) )
318		id 19	. . . . . . . . . . . . . . 15 |- ( x = ( N / 2 ) -> x = ( N / 2 ) )
319	317, 318	oveq12d 6106	. . . . . . . . . . . . . 14 |- ( x = ( N / 2 ) -> ( ( log ` x ) / x ) = ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) )
320	73	relogcld 16112	. . . . . . . . . . . . . . 15 |- ( ph -> ( log ` ( N / 2 ) ) e. RR )
321	320, 73	rerpdivcld 10146	. . . . . . . . . . . . . 14 |- ( ph -> ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) e. RR )
322	3, 319, 73, 321	fvmptd3 5802	. . . . . . . . . . . . 13 |- ( ph -> ( G ` ( N / 2 ) ) = ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) )
323	316, 322	oveq12d 6106	. . . . . . . . . . . 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 9400	. . . . . . . . . . . . . . . 16 |- 9 e. RR
325		4ap0 9412	. . . . . . . . . . . . . . . 16 |- 4 # 0
326	324, 109, 325	redivclapi 9117	. . . . . . . . . . . . . . 15 |- ( 9 / 4 ) e. RR
327	326	recni 8344	. . . . . . . . . . . . . 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 8360	. . . . . . . . . . . . 13 |- ( ph -> ( G ` ( N / 2 ) ) e. CC )
331	201, 328, 330	mulassd 8355	. . . . . . . . . . . 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 10116	. . . . . . . . . . . . . 14 |- ( ph -> ( N / 2 ) e. CC )
334	320	recnd 8360	. . . . . . . . . . . . . . 15 |- ( ph -> ( log ` ( N / 2 ) ) e. CC )
335	73	rpap0d 10120	. . . . . . . . . . . . . . 15 |- ( ph -> ( N / 2 ) # 0 )
336	334, 333, 335	divclapd 9128	. . . . . . . . . . . . . 14 |- ( ph -> ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) e. CC )
337	332, 333, 336	mulassd 8355	. . . . . . . . . . . . 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 9130	. . . . . . . . . . . . . 14 |- ( ph -> ( ( N / 2 ) x. ( ( log ` ( N / 2 ) ) / ( N / 2 ) ) ) = ( log ` ( N / 2 ) ) )
339	338	oveq2d 6104	. . . . . . . . . . . . 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 8337	. . . . . . . . . . . . 13 |- ( 3 x. ( log ` 2 ) ) e. CC
343	342	a1i 9	. . . . . . . . . . . 12 |- ( ph -> ( 3 x. ( log ` 2 ) ) e. CC )
344		mulcl 8312	. . . . . . . . . . . . 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 8680	. . . . . . . . . . 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 8346	. . . . . . . . . . . . 13 |- ( 2 x. ( log ` 2 ) ) e. RR
349	348	recni 8344	. . . . . . . . . . . 12 |- ( 2 x. ( log ` 2 ) ) e. CC
350	349	a1i 9	. . . . . . . . . . 11 |- ( ph -> ( 2 x. ( log ` 2 ) ) e. CC )
351		subcl 8532	. . . . . . . . . . . 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 8354	. . . . . . . . . 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 6104	. . . . . . . 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 8312	. . . . . . . . . . 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 8352	. . . . . . . . . 10 |- ( ph -> ( ( ( sqr ` ( 2 x. N ) ) / 3 ) x. ( log ` N ) ) e. CC )
359		remulcl 8313	. . . . . . . . . . . . 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 8360	. . . . . . . . . . 11 |- ( ph -> ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) e. CC )
362	201, 361	mulcld 8352	. . . . . . . . . 10 |- ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) e. CC )
363	357, 358, 362	addassd 8354	. . . . . . . . 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 6104	. . . . . . . . . . 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 8356	. . . . . . . . . . 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 6103	. . . . . . . . 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 6104	. . . . . . . . . . 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 5698	. . . . . . . . . . . . . . . . . 18 |- ( x = ( sqr ` N ) -> ( log ` x ) = ( log ` ( sqr ` N ) ) )
370		id 19	. . . . . . . . . . . . . . . . . 18 |- ( x = ( sqr ` N ) -> x = ( sqr ` N ) )
371	369, 370	oveq12d 6106	. . . . . . . . . . . . . . . . 17 |- ( x = ( sqr ` N ) -> ( ( log ` x ) / x ) = ( ( log ` ( sqr ` N ) ) / ( sqr ` N ) ) )
372	63	relogcld 16112	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( log ` ( sqr ` N ) ) e. RR )
373	372, 63	rerpdivcld 10146	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( log ` ( sqr ` N ) ) / ( sqr ` N ) ) e. RR )
374	3, 371, 63, 373	fvmptd3 5802	. . . . . . . . . . . . . . . 16 |- ( ph -> ( G ` ( sqr ` N ) ) = ( ( log ` ( sqr ` N ) ) / ( sqr ` N ) ) )
375	374, 373	eqeltrd 2315	. . . . . . . . . . . . . . 15 |- ( ph -> ( G ` ( sqr ` N ) ) e. RR )
376		remulcl 8313	. . . . . . . . . . . . . . 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 8361	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) e. RR )
379	378	recnd 8360	. . . . . . . . . . . 12 |- ( ph -> ( ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) + ( ( 9 / 4 ) x. ( G ` ( N / 2 ) ) ) ) e. CC )
380		rerpdivcl 10102	. . . . . . . . . . . . . 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 8360	. . . . . . . . . . . 12 |- ( ph -> ( ( log ` 2 ) / ( sqr ` ( 2 x. N ) ) ) e. CC )
383	201, 379, 382	adddid 8356	. . . . . . . . . . 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 8360	. . . . . . . . . . . . 13 |- ( ph -> ( ( sqr ` 2 ) x. ( G ` ( sqr ` N ) ) ) e. CC )
386	201, 385, 361	adddid 8356	. . . . . . . . . . . 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 10118	. . . . . . . . . . . . . . . . . 18 |- ( ph -> 0 <_ ( 2 x. N ) )
388		remsqsqrt 11820	. . . . . . . . . . . . . . . . . 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 6103	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( ( sqr ` ( 2 x. N ) ) x. ( sqr ` ( 2 x. N ) ) ) / 3 ) = ( ( 2 x. N ) / 3 ) )
391	100	recnd 8360	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( sqr ` ( 2 x. N ) ) e. CC )
392	211	a1i 9	. . . . . . . . . . . . . . . . 17 |- ( ph -> 3 # 0 )
393	391, 391, 332, 392	div23apd 9166	. . . . . . . . . . . . . . . 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 6103	. . . . . . . . . . . . . 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 8355	. . . . . . . . . . . . . 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 9403	. . . . . . . . . . . . . . . . . . 19 |- 0 <_ 2
398	104, 397	pm3.2i 272	. . . . . . . . . . . . . . . . . 18 |- ( 2 e. RR /\ 0 <_ 2 )
399	62	rprege0d 10122	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( N e. RR /\ 0 <_ N ) )
400		sqrtmul 11823	. . . . . . . . . . . . . . . . . 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 6103	. . . . . . . . . . . . . . . 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 8344	. . . . . . . . . . . . . . . . . 18 |- ( sqr ` 2 ) e. CC
404	403	a1i 9	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( sqr ` 2 ) e. CC )
405	63	rpcnd 10116	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( sqr ` N ) e. CC )
406	375	recnd 8360	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( G ` ( sqr ` N ) ) e. CC )
407	404, 405, 404, 406	mul4d 8488	. . . . . . . . . . . . . . . 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 11820	. . . . . . . . . . . . . . . . . . . 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 6104	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( sqr ` N ) x. ( G ` ( sqr ` N ) ) ) = ( ( sqr ` N ) x. ( ( log ` ( sqr ` N ) ) / ( sqr ` N ) ) ) )
412	372	recnd 8360	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( log ` ( sqr ` N ) ) e. CC )
413	63	rpap0d 10120	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( sqr ` N ) # 0 )
414	412, 405, 413	divcanap2d 9130	. . . . . . . . . . . . . . . . . . 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 6106	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( ( ( sqr ` 2 ) x. ( sqr ` 2 ) ) x. ( ( sqr ` N ) x. ( G ` ( sqr ` N ) ) ) ) = ( 2 x. ( log ` ( sqr ` N ) ) ) )
417	412	2timesd 9559	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( 2 x. ( log ` ( sqr ` N ) ) ) = ( ( log ` ( sqr ` N ) ) + ( log ` ( sqr ` N ) ) ) )
418	63, 63	relogmuld 16114	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( log ` ( ( sqr ` N ) x. ( sqr ` N ) ) ) = ( ( log ` ( sqr ` N ) ) + ( log ` ( sqr ` N ) ) ) )
419		remsqsqrt 11820	. . . . . . . . . . . . . . . . . . . 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 5702	. . . . . . . . . . . . . . . . . 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 6104	. . . . . . . . . . . . . 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 6103	. . . . . . . . . . . 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 6103	. . . . . . . . . . . 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 8355	. . . . . . . . . . . 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 10120	. . . . . . . . . . . . . 14 |- ( ph -> ( sqr ` ( 2 x. N ) ) # 0 )
432	232, 391, 431	divcanap2d 9130	. . . . . . . . . . . . 13 |- ( ph -> ( ( sqr ` ( 2 x. N ) ) x. ( ( log ` 2 ) / ( sqr ` ( 2 x. N ) ) ) ) = ( log ` 2 ) )
433	432	oveq2d 6104	. . . . . . . . . . . 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 6106	. . . . . . . . . 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 8351	. . . . . . . . . . 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 8484	. . . . . . . . . 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 8352	. . . . . . . . 9 |- ( ph -> ( ( ( sqr ` ( 2 x. N ) ) / 3 ) x. ( log ` ( 2 x. N ) ) ) e. CC )
441		addcl 8310	. . . . . . . . . 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 8354	. . . . . . . 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 4163	. . . . 5 |- ( ph -> ( ( ( 2 x. N ) / 3 ) x. ( log ` 2 ) ) < ( ( ( 2 x. N ) / 3 ) x. ( F ` N ) ) )
447	80, 87, 200	ltmul2d 10157	. . . . 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 8459	. . 3 |- ( ph -> ( F ` ; 6 4 ) < ( F ` N ) )
450	45, 87, 449	ltnsymd 8453	. 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 4131   |-> cmpt 4193   ` cfv 5380  (class class class)co 6088   CCcc 8183   RRcr 8184   0cc0 8185   1c1 8186   + caddc 8188   x. cmul 8190   < clt 8366   <_ cle 8367   - cmin 8504   # cap 8917   / cdiv 9010   NNcn 9313   2c2 9364   3c3 9365   4c4 9366   5c5 9367   6c6 9368   8c8 9370   9c9 9371   ZZcz 9655  ;cdc 9788   ZZ>=cuz 9937   QQcq 10035   RR+crp 10071   |_cfl 10720   ^cexp 10996   _C cbc 11207   sqrcsqrt 11784   expce 12434   _eceu 12435   Primecprime 12910   pCnt cpc 13092   logclog 16085   ^c ccxp 16086

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 4248  ax-sep 4251  ax-nul 4261  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-iinf 4737  ax-cnex 8276  ax-resscn 8277  ax-1cn 8278  ax-1re 8279  ax-icn 8280  ax-addcl 8281  ax-addrcl 8282  ax-mulcl 8283  ax-mulrcl 8284  ax-addcom 8285  ax-mulcom 8286  ax-addass 8287  ax-mulass 8288  ax-distr 8289  ax-i2m1 8290  ax-0lt1 8291  ax-1rid 8292  ax-0id 8293  ax-rnegex 8294  ax-precex 8295  ax-cnre 8296  ax-pre-ltirr 8297  ax-pre-ltwlin 8298  ax-pre-lttrn 8299  ax-pre-apti 8300  ax-pre-ltadd 8301  ax-pre-mulgt0 8302  ax-pre-mulext 8303  ax-arch 8304  ax-caucvg 8305  ax-pre-suploc 8306  ax-addf 8307  ax-mulf 8308

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 4132  df-opab 4194  df-mpt 4195  df-tr 4232  df-id 4440  df-po 4443  df-iso 4444  df-iord 4513  df-on 4515  df-ilim 4516  df-suc 4518  df-iom 4740  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-res 4788  df-ima 4789  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-f1 5385  df-fo 5386  df-f1o 5387  df-fv 5388  df-isom 5389  df-riota 6041  df-ov 6091  df-oprab 6092  df-mpo 6093  df-of 6305  df-1st 6378  df-2nd 6379  df-recs 6580  df-irdg 6645  df-frec 6666  df-1o 6691  df-2o 6692  df-oadd 6695  df-er 6811  df-map 6928  df-pm 6929  df-en 7027  df-dom 7028  df-fin 7029  df-sup 7330  df-inf 7331  df-pnf 8368  df-mnf 8369  df-xr 8370  df-ltxr 8371  df-le 8372  df-sub 8506  df-neg 8507  df-reap 8911  df-ap 8918  df-div 9011  df-inn 9314  df-2 9372  df-3 9373  df-4 9374  df-5 9375  df-6 9376  df-7 9377  df-8 9378  df-9 9379  df-n0 9575  df-xnn0 9642  df-z 9656  df-dec 9789  df-uz 9938  df-q 10036  df-rp 10072  df-xneg 10191  df-xadd 10192  df-ioo 10311  df-ico 10313  df-icc 10314  df-fz 10429  df-fzo 10567  df-fl 10722  df-mod 10781  df-seqfrec 10906  df-exp 10997  df-fac 11186  df-bc 11208  df-ihash 11237  df-shft 11602  df-cj 11629  df-re 11630  df-im 11631  df-rsqrt 11786  df-abs 11787  df-clim 12070  df-sumdc 12145  df-ef 12440  df-e 12441  df-dvds 12580  df-gcd 12756  df-prm 12911  df-numer 12988  df-denom 12989  df-pc 13093  df-rest 13654  df-topgen 13673  df-psmet 14989  df-xmet 14990  df-met 14991  df-bl 14992  df-mopn 14993  df-top 15224  df-topon 15237  df-bases 15269  df-ntr 15322  df-cn 15414  df-cnp 15415  df-tx 15479  df-cncf 15797  df-limced 15882  df-dvap 15883  df-relog 16087  df-rpcxp 16088  df-logb 16180  df-cht 16236  df-ppi 16237

This theorem is used by:  bpos  16320