Theorem bposlem6 16316

Description: Lemma for bpos 16320. By using the various bounds at our disposal, arrive at an inequality that is false for N large enough. (Contributed by Mario Carneiro, 14-Mar-2014.) (Revised by Wolf Lammen, 12-Sep-2020.)

Hypotheses

Ref	Expression
bpos.1	|- ( ph -> N e. ( ZZ>= ` 5 ) )
bpos.2	|- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
bpos.3	|- F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )
bpos.4	|- K = ( |_ ` ( ( 2 x. N ) / 3 ) )
bpos.5	|- M = ( |_ ` ( sqr ` ( 2 x. N ) ) )

Assertion

Ref	Expression
bposlem6	|- ( ph -> ( ( 4 ^ N ) / N ) < ( ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )

Distinct variable groups:   F, p   n, p, K   M, p   n, N, p   ph, n, p

Allowed substitution hints:   F( n)   M( n)

Proof of Theorem bposlem6

Dummy variable q is distinct from all other variables.

Step	Hyp	Ref	Expression
1		4nn 9479	. . . . 5 |- 4 e. NN
2		5nn 9480	. . . . . . 7 |- 5 e. NN
3		bpos.1	. . . . . . 7 |- ( ph -> N e. ( ZZ>= ` 5 ) )
4		eluznn 10016	. . . . . . 7 |- ( ( 5 e. NN /\ N e. ( ZZ>= ` 5 ) ) -> N e. NN )
5	2, 3, 4	sylancr 418	. . . . . 6 |- ( ph -> N e. NN )
6	5	nnnn0d 9631	. . . . 5 |- ( ph -> N e. NN0 )
7		nnexpcl 11010	. . . . 5 |- ( ( 4 e. NN /\ N e. NN0 ) -> ( 4 ^ N ) e. NN )
8	1, 6, 7	sylancr 418	. . . 4 |- ( ph -> ( 4 ^ N ) e. NN )
9	8	nnred 9326	. . 3 |- ( ph -> ( 4 ^ N ) e. RR )
10	9, 5	nndivred 9363	. 2 |- ( ph -> ( ( 4 ^ N ) / N ) e. RR )
11		fzctr 10557	. . . . 5 |- ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) )
12	6, 11	syl 14	. . . 4 |- ( ph -> N e. ( 0 ... ( 2 x. N ) ) )
13		bccl2 11228	. . . 4 |- ( N e. ( 0 ... ( 2 x. N ) ) -> ( ( 2 x. N ) _C N ) e. NN )
14	12, 13	syl 14	. . 3 |- ( ph -> ( ( 2 x. N ) _C N ) e. NN )
15	14	nnred 9326	. 2 |- ( ph -> ( ( 2 x. N ) _C N ) e. RR )
16		2nn 9477	. . . . . . 7 |- 2 e. NN
17		nnmulcl 9334	. . . . . . 7 |- ( ( 2 e. NN /\ N e. NN ) -> ( 2 x. N ) e. NN )
18	16, 5, 17	sylancr 418	. . . . . 6 |- ( ph -> ( 2 x. N ) e. NN )
19	18	nnrpd 10112	. . . . 5 |- ( ph -> ( 2 x. N ) e. RR+ )
20	18	nnred 9326	. . . . . . . 8 |- ( ph -> ( 2 x. N ) e. RR )
21	19	rpge0d 10118	. . . . . . . 8 |- ( ph -> 0 <_ ( 2 x. N ) )
22	20, 21	resqrtcld 11952	. . . . . . 7 |- ( ph -> ( sqr ` ( 2 x. N ) ) e. RR )
23		3nn 9478	. . . . . . 7 |- 3 e. NN
24		nndivre 9349	. . . . . . 7 |- ( ( ( sqr ` ( 2 x. N ) ) e. RR /\ 3 e. NN ) -> ( ( sqr ` ( 2 x. N ) ) / 3 ) e. RR )
25	22, 23, 24	sylancl 417	. . . . . 6 |- ( ph -> ( ( sqr ` ( 2 x. N ) ) / 3 ) e. RR )
26		2re 9383	. . . . . 6 |- 2 e. RR
27		readdcl 8311	. . . . . 6 |- ( ( ( ( sqr ` ( 2 x. N ) ) / 3 ) e. RR /\ 2 e. RR ) -> ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) e. RR )
28	25, 26, 27	sylancl 417	. . . . 5 |- ( ph -> ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) e. RR )
29	19, 28	rpcxpcld 16168	. . . 4 |- ( ph -> ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) e. RR+ )
30	29	rpred 10114	. . 3 |- ( ph -> ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) e. RR )
31		2rp 10076	. . . . 5 |- 2 e. RR+
32		nnmulcl 9334	. . . . . . . . 9 |- ( ( 4 e. NN /\ N e. NN ) -> ( 4 x. N ) e. NN )
33	1, 5, 32	sylancr 418	. . . . . . . 8 |- ( ph -> ( 4 x. N ) e. NN )
34	33	nnred 9326	. . . . . . 7 |- ( ph -> ( 4 x. N ) e. RR )
35		nndivre 9349	. . . . . . 7 |- ( ( ( 4 x. N ) e. RR /\ 3 e. NN ) -> ( ( 4 x. N ) / 3 ) e. RR )
36	34, 23, 35	sylancl 417	. . . . . 6 |- ( ph -> ( ( 4 x. N ) / 3 ) e. RR )
37		5re 9392	. . . . . 6 |- 5 e. RR
38		resubcl 8597	. . . . . 6 |- ( ( ( ( 4 x. N ) / 3 ) e. RR /\ 5 e. RR ) -> ( ( ( 4 x. N ) / 3 ) - 5 ) e. RR )
39	36, 37, 38	sylancl 417	. . . . 5 |- ( ph -> ( ( ( 4 x. N ) / 3 ) - 5 ) e. RR )
40		rpcxpcl 16136	. . . . 5 |- ( ( 2 e. RR+ /\ ( ( ( 4 x. N ) / 3 ) - 5 ) e. RR ) -> ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) e. RR+ )
41	31, 39, 40	sylancr 418	. . . 4 |- ( ph -> ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) e. RR+ )
42	41	rpred 10114	. . 3 |- ( ph -> ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) e. RR )
43	30, 42	remulcld 8362	. 2 |- ( ph -> ( ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) e. RR )
44		df-5 9375	. . . . 5 |- 5 = ( 4 + 1 )
45		4z 9685	. . . . . 6 |- 4 e. ZZ
46		uzid 9952	. . . . . 6 |- ( 4 e. ZZ -> 4 e. ( ZZ>= ` 4 ) )
47		peano2uz 9999	. . . . . 6 |- ( 4 e. ( ZZ>= ` 4 ) -> ( 4 + 1 ) e. ( ZZ>= ` 4 ) )
48	45, 46, 47	mp2b 8	. . . . 5 |- ( 4 + 1 ) e. ( ZZ>= ` 4 )
49	44, 48	eqeltri 2311	. . . 4 |- 5 e. ( ZZ>= ` 4 )
50		eqid 2238	. . . . 5 |- ( ZZ>= ` 4 ) = ( ZZ>= ` 4 )
51	50	uztrn2 9956	. . . 4 |- ( ( 5 e. ( ZZ>= ` 4 ) /\ N e. ( ZZ>= ` 5 ) ) -> N e. ( ZZ>= ` 4 ) )
52	49, 3, 51	sylancr 418	. . 3 |- ( ph -> N e. ( ZZ>= ` 4 ) )
53		bclbnd 16307	. . 3 |- ( N e. ( ZZ>= ` 4 ) -> ( ( 4 ^ N ) / N ) < ( ( 2 x. N ) _C N ) )
54	52, 53	syl 14	. 2 |- ( ph -> ( ( 4 ^ N ) / N ) < ( ( 2 x. N ) _C N ) )
55		bpos.3	. . . . . . . 8 |- F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )
56		id 19	. . . . . . . . . 10 |- ( n e. Prime -> n e. Prime )
57		pccl 13107	. . . . . . . . . 10 |- ( ( n e. Prime /\ ( ( 2 x. N ) _C N ) e. NN ) -> ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
58	56, 14, 57	syl2anr 290	. . . . . . . . 9 |- ( ( ph /\ n e. Prime ) -> ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
59	58	ralrimiva 2623	. . . . . . . 8 |- ( ph -> A. n e. Prime ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
60	55, 59	pcmptcl 13150	. . . . . . 7 |- ( ph -> ( F : NN --> NN /\ seq 1 ( x. , F ) : NN --> NN ) )
61	60	simprd 114	. . . . . 6 |- ( ph -> seq 1 ( x. , F ) : NN --> NN )
62		bpos.2	. . . . . . . . 9 |- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
63		bpos.4	. . . . . . . . 9 |- K = ( |_ ` ( ( 2 x. N ) / 3 ) )
64		bpos.5	. . . . . . . . 9 |- M = ( |_ ` ( sqr ` ( 2 x. N ) ) )
65	3, 62, 55, 63, 64	bposlem4 16314	. . . . . . . 8 |- ( ph -> M e. ( 3 ... K ) )
66		elfzuz 10441	. . . . . . . 8 |- ( M e. ( 3 ... K ) -> M e. ( ZZ>= ` 3 ) )
67	65, 66	syl 14	. . . . . . 7 |- ( ph -> M e. ( ZZ>= ` 3 ) )
68		eluznn 10016	. . . . . . 7 |- ( ( 3 e. NN /\ M e. ( ZZ>= ` 3 ) ) -> M e. NN )
69	23, 67, 68	sylancr 418	. . . . . 6 |- ( ph -> M e. NN )
70	61, 69	ffvelcdmd 5847	. . . . 5 |- ( ph -> ( seq 1 ( x. , F ) ` M ) e. NN )
71	70	nnred 9326	. . . 4 |- ( ph -> ( seq 1 ( x. , F ) ` M ) e. RR )
72		2z 9683	. . . . . . . . 9 |- 2 e. ZZ
73	18	nnzd 9778	. . . . . . . . . . . 12 |- ( ph -> ( 2 x. N ) e. ZZ )
74		znq 10040	. . . . . . . . . . . 12 |- ( ( ( 2 x. N ) e. ZZ /\ 3 e. NN ) -> ( ( 2 x. N ) / 3 ) e. QQ )
75	73, 23, 74	sylancl 417	. . . . . . . . . . 11 |- ( ph -> ( ( 2 x. N ) / 3 ) e. QQ )
76	75	flqcld 10731	. . . . . . . . . 10 |- ( ph -> ( |_ ` ( ( 2 x. N ) / 3 ) ) e. ZZ )
77	63, 76	eqeltrid 2325	. . . . . . . . 9 |- ( ph -> K e. ZZ )
78		zmulcl 9709	. . . . . . . . 9 |- ( ( 2 e. ZZ /\ K e. ZZ ) -> ( 2 x. K ) e. ZZ )
79	72, 77, 78	sylancr 418	. . . . . . . 8 |- ( ph -> ( 2 x. K ) e. ZZ )
80	2	nnzi 9676	. . . . . . . 8 |- 5 e. ZZ
81		zsubcl 9696	. . . . . . . 8 |- ( ( ( 2 x. K ) e. ZZ /\ 5 e. ZZ ) -> ( ( 2 x. K ) - 5 ) e. ZZ )
82	79, 80, 81	sylancl 417	. . . . . . 7 |- ( ph -> ( ( 2 x. K ) - 5 ) e. ZZ )
83	82	zred 9779	. . . . . 6 |- ( ph -> ( ( 2 x. K ) - 5 ) e. RR )
84		rpcxpcl 16136	. . . . . 6 |- ( ( 2 e. RR+ /\ ( ( 2 x. K ) - 5 ) e. RR ) -> ( 2 ^c ( ( 2 x. K ) - 5 ) ) e. RR+ )
85	31, 83, 84	sylancr 418	. . . . 5 |- ( ph -> ( 2 ^c ( ( 2 x. K ) - 5 ) ) e. RR+ )
86	85	rpred 10114	. . . 4 |- ( ph -> ( 2 ^c ( ( 2 x. K ) - 5 ) ) e. RR )
87	71, 86	remulcld 8362	. . 3 |- ( ph -> ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) e. RR )
88	3, 62, 55, 63	bposlem3 16313	. . . 4 |- ( ph -> ( seq 1 ( x. , F ) ` K ) = ( ( 2 x. N ) _C N ) )
89		elfzuz3 10442	. . . . . . . . . 10 |- ( M e. ( 3 ... K ) -> K e. ( ZZ>= ` M ) )
90	65, 89	syl 14	. . . . . . . . 9 |- ( ph -> K e. ( ZZ>= ` M ) )
91	55, 59, 69, 90	pcmptdvds 13153	. . . . . . . 8 |- ( ph -> ( seq 1 ( x. , F ) ` M ) || ( seq 1 ( x. , F ) ` K ) )
92	70	nnzd 9778	. . . . . . . . 9 |- ( ph -> ( seq 1 ( x. , F ) ` M ) e. ZZ )
93	70	nnne0d 9358	. . . . . . . . 9 |- ( ph -> ( seq 1 ( x. , F ) ` M ) =/= 0 )
94		uztrn 9955	. . . . . . . . . . . . 13 |- ( ( K e. ( ZZ>= ` M ) /\ M e. ( ZZ>= ` 3 ) ) -> K e. ( ZZ>= ` 3 ) )
95	90, 67, 94	syl2anc 415	. . . . . . . . . . . 12 |- ( ph -> K e. ( ZZ>= ` 3 ) )
96		eluznn 10016	. . . . . . . . . . . 12 |- ( ( 3 e. NN /\ K e. ( ZZ>= ` 3 ) ) -> K e. NN )
97	23, 95, 96	sylancr 418	. . . . . . . . . . 11 |- ( ph -> K e. NN )
98	61, 97	ffvelcdmd 5847	. . . . . . . . . 10 |- ( ph -> ( seq 1 ( x. , F ) ` K ) e. NN )
99	98	nnzd 9778	. . . . . . . . 9 |- ( ph -> ( seq 1 ( x. , F ) ` K ) e. ZZ )
100		dvdsval2 12582	. . . . . . . . 9 |- ( ( ( seq 1 ( x. , F ) ` M ) e. ZZ /\ ( seq 1 ( x. , F ) ` M ) =/= 0 /\ ( seq 1 ( x. , F ) ` K ) e. ZZ ) -> ( ( seq 1 ( x. , F ) ` M ) || ( seq 1 ( x. , F ) ` K ) <-> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) e. ZZ ) )
101	92, 93, 99, 100	syl3anc 1278	. . . . . . . 8 |- ( ph -> ( ( seq 1 ( x. , F ) ` M ) || ( seq 1 ( x. , F ) ` K ) <-> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) e. ZZ ) )
102	91, 101	mpbid 147	. . . . . . 7 |- ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) e. ZZ )
103	102	zred 9779	. . . . . 6 |- ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) e. RR )
104		nnq 10049	. . . . . . . . . 10 |- ( M e. NN -> M e. QQ )
105	69, 104	syl 14	. . . . . . . . 9 |- ( ph -> M e. QQ )
106		zq 10042	. . . . . . . . . 10 |- ( K e. ZZ -> K e. QQ )
107	77, 106	syl 14	. . . . . . . . 9 |- ( ph -> K e. QQ )
108		eluzle 9950	. . . . . . . . . 10 |- ( K e. ( ZZ>= ` M ) -> M <_ K )
109	90, 108	syl 14	. . . . . . . . 9 |- ( ph -> M <_ K )
110		efchtqdvds 16265	. . . . . . . . 9 |- ( ( M e. QQ /\ K e. QQ /\ M <_ K ) -> ( exp ` ( theta ` M ) ) || ( exp ` ( theta ` K ) ) )
111	105, 107, 109, 110	syl3anc 1278	. . . . . . . 8 |- ( ph -> ( exp ` ( theta ` M ) ) || ( exp ` ( theta ` K ) ) )
112		efchtqcl 16246	. . . . . . . . . . 11 |- ( M e. QQ -> ( exp ` ( theta ` M ) ) e. NN )
113	105, 112	syl 14	. . . . . . . . . 10 |- ( ph -> ( exp ` ( theta ` M ) ) e. NN )
114	113	nnzd 9778	. . . . . . . . 9 |- ( ph -> ( exp ` ( theta ` M ) ) e. ZZ )
115	113	nnne0d 9358	. . . . . . . . 9 |- ( ph -> ( exp ` ( theta ` M ) ) =/= 0 )
116		efchtqcl 16246	. . . . . . . . . . 11 |- ( K e. QQ -> ( exp ` ( theta ` K ) ) e. NN )
117	107, 116	syl 14	. . . . . . . . . 10 |- ( ph -> ( exp ` ( theta ` K ) ) e. NN )
118	117	nnzd 9778	. . . . . . . . 9 |- ( ph -> ( exp ` ( theta ` K ) ) e. ZZ )
119		dvdsval2 12582	. . . . . . . . 9 |- ( ( ( exp ` ( theta ` M ) ) e. ZZ /\ ( exp ` ( theta ` M ) ) =/= 0 /\ ( exp ` ( theta ` K ) ) e. ZZ ) -> ( ( exp ` ( theta ` M ) ) || ( exp ` ( theta ` K ) ) <-> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. ZZ ) )
120	114, 115, 118, 119	syl3anc 1278	. . . . . . . 8 |- ( ph -> ( ( exp ` ( theta ` M ) ) || ( exp ` ( theta ` K ) ) <-> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. ZZ ) )
121	111, 120	mpbid 147	. . . . . . 7 |- ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. ZZ )
122	121	zred 9779	. . . . . 6 |- ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. RR )
123	18	nnnn0d 9631	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 2 x. N ) e. NN0 )
124		sqrtrirr 13014	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2 x. N ) e. NN0 -> ( ( sqr ` ( 2 x. N ) ) e. QQ \/ ( ( sqr ` ( 2 x. N ) ) e. RR /\ A. q e. QQ ( sqr ` ( 2 x. N ) ) # q ) ) )
125	123, 124	syl 14	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ( sqr ` ( 2 x. N ) ) e. QQ \/ ( ( sqr ` ( 2 x. N ) ) e. RR /\ A. q e. QQ ( sqr ` ( 2 x. N ) ) # q ) ) )
126		prmz 12914	. . . . . . . . . . . . . . . . . 18 |- ( p e. Prime -> p e. ZZ )
127		flaplt 10739	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( sqr ` ( 2 x. N ) ) e. QQ \/ ( ( sqr ` ( 2 x. N ) ) e. RR /\ A. q e. QQ ( sqr ` ( 2 x. N ) ) # q ) ) /\ p e. ZZ ) -> ( ( sqr ` ( 2 x. N ) ) < p <-> ( |_ ` ( sqr ` ( 2 x. N ) ) ) < p ) )
128	125, 126, 127	syl2an 289	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ p e. Prime ) -> ( ( sqr ` ( 2 x. N ) ) < p <-> ( |_ ` ( sqr ` ( 2 x. N ) ) ) < p ) )
129	64	breq1i 4138	. . . . . . . . . . . . . . . . 17 |- ( M < p <-> ( |_ ` ( sqr ` ( 2 x. N ) ) ) < p )
130	128, 129	bitr4di 198	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ p e. Prime ) -> ( ( sqr ` ( 2 x. N ) ) < p <-> M < p ) )
131	69	nnzd 9778	. . . . . . . . . . . . . . . . 17 |- ( ph -> M e. ZZ )
132		zltnle 9701	. . . . . . . . . . . . . . . . 17 |- ( ( M e. ZZ /\ p e. ZZ ) -> ( M < p <-> -. p <_ M ) )
133	131, 126, 132	syl2an 289	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ p e. Prime ) -> ( M < p <-> -. p <_ M ) )
134	130, 133	bitrd 188	. . . . . . . . . . . . . . 15 |- ( ( ph /\ p e. Prime ) -> ( ( sqr ` ( 2 x. N ) ) < p <-> -. p <_ M ) )
135		bposlem1 16311	. . . . . . . . . . . . . . . . . . . 20 |- ( ( N e. NN /\ p e. Prime ) -> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )
136	5, 135	sylan 283	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. Prime ) -> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )
137	126	zred 9779	. . . . . . . . . . . . . . . . . . . . . 22 |- ( p e. Prime -> p e. RR )
138	137	adantl 277	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ p e. Prime ) -> p e. RR )
139		id 19	. . . . . . . . . . . . . . . . . . . . . 22 |- ( p e. Prime -> p e. Prime )
140		pccl 13107	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( p e. Prime /\ ( ( 2 x. N ) _C N ) e. NN ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
141	139, 14, 140	syl2anr 290	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
142	138, 141	reexpcld 11149	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ p e. Prime ) -> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) e. RR )
143	20	adantr 276	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ p e. Prime ) -> ( 2 x. N ) e. RR )
144	138	resqcld 11158	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ p e. Prime ) -> ( p ^ 2 ) e. RR )
145		lelttr 8420	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) e. RR /\ ( 2 x. N ) e. RR /\ ( p ^ 2 ) e. RR ) -> ( ( ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) /\ ( 2 x. N ) < ( p ^ 2 ) ) -> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) < ( p ^ 2 ) ) )
146	142, 143, 144, 145	syl3anc 1278	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. Prime ) -> ( ( ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) /\ ( 2 x. N ) < ( p ^ 2 ) ) -> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) < ( p ^ 2 ) ) )
147	136, 146	mpand 433	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ p e. Prime ) -> ( ( 2 x. N ) < ( p ^ 2 ) -> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) < ( p ^ 2 ) ) )
148		resqrtth 11819	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( 2 x. N ) e. RR /\ 0 <_ ( 2 x. N ) ) -> ( ( sqr ` ( 2 x. N ) ) ^ 2 ) = ( 2 x. N ) )
149	20, 21, 148	syl2anc 415	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( sqr ` ( 2 x. N ) ) ^ 2 ) = ( 2 x. N ) )
150	149	breq1d 4141	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( ( ( sqr ` ( 2 x. N ) ) ^ 2 ) < ( p ^ 2 ) <-> ( 2 x. N ) < ( p ^ 2 ) ) )
151	150	adantr 276	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ p e. Prime ) -> ( ( ( sqr ` ( 2 x. N ) ) ^ 2 ) < ( p ^ 2 ) <-> ( 2 x. N ) < ( p ^ 2 ) ) )
152	141	nn0zd 9777	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) e. ZZ )
153	72	a1i 9	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. Prime ) -> 2 e. ZZ )
154		prmgt1 12936	. . . . . . . . . . . . . . . . . . . 20 |- ( p e. Prime -> 1 < p )
155	154	adantl 277	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. Prime ) -> 1 < p )
156	138, 152, 153, 155	ltexp2d 16178	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ p e. Prime ) -> ( ( p pCnt ( ( 2 x. N ) _C N ) ) < 2 <-> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) < ( p ^ 2 ) ) )
157	147, 151, 156	3imtr4d 203	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ p e. Prime ) -> ( ( ( sqr ` ( 2 x. N ) ) ^ 2 ) < ( p ^ 2 ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) < 2 ) )
158		df-2 9372	. . . . . . . . . . . . . . . . . 18 |- 2 = ( 1 + 1 )
159	158	breq2i 4139	. . . . . . . . . . . . . . . . 17 |- ( ( p pCnt ( ( 2 x. N ) _C N ) ) < 2 <-> ( p pCnt ( ( 2 x. N ) _C N ) ) < ( 1 + 1 ) )
160	157, 159	imbitrdi 161	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ p e. Prime ) -> ( ( ( sqr ` ( 2 x. N ) ) ^ 2 ) < ( p ^ 2 ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) < ( 1 + 1 ) ) )
161	22	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ p e. Prime ) -> ( sqr ` ( 2 x. N ) ) e. RR )
162	20, 21	sqrtge0d 11955	. . . . . . . . . . . . . . . . . 18 |- ( ph -> 0 <_ ( sqr ` ( 2 x. N ) ) )
163	162	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ p e. Prime ) -> 0 <_ ( sqr ` ( 2 x. N ) ) )
164		prmnn 12913	. . . . . . . . . . . . . . . . . . . 20 |- ( p e. Prime -> p e. NN )
165	164	nnrpd 10112	. . . . . . . . . . . . . . . . . . 19 |- ( p e. Prime -> p e. RR+ )
166	165	rpge0d 10118	. . . . . . . . . . . . . . . . . 18 |- ( p e. Prime -> 0 <_ p )
167	166	adantl 277	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ p e. Prime ) -> 0 <_ p )
168	161, 138, 163, 167	lt2sqd 11163	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ p e. Prime ) -> ( ( sqr ` ( 2 x. N ) ) < p <-> ( ( sqr ` ( 2 x. N ) ) ^ 2 ) < ( p ^ 2 ) ) )
169		1z 9681	. . . . . . . . . . . . . . . . 17 |- 1 e. ZZ
170		zleltp1 9711	. . . . . . . . . . . . . . . . 17 |- ( ( ( p pCnt ( ( 2 x. N ) _C N ) ) e. ZZ /\ 1 e. ZZ ) -> ( ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 <-> ( p pCnt ( ( 2 x. N ) _C N ) ) < ( 1 + 1 ) ) )
171	152, 169, 170	sylancl 417	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ p e. Prime ) -> ( ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 <-> ( p pCnt ( ( 2 x. N ) _C N ) ) < ( 1 + 1 ) ) )
172	160, 168, 171	3imtr4d 203	. . . . . . . . . . . . . . 15 |- ( ( ph /\ p e. Prime ) -> ( ( sqr ` ( 2 x. N ) ) < p -> ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 ) )
173	134, 172	sylbird 170	. . . . . . . . . . . . . 14 |- ( ( ph /\ p e. Prime ) -> ( -. p <_ M -> ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 ) )
174	173	imp 124	. . . . . . . . . . . . 13 |- ( ( ( ph /\ p e. Prime ) /\ -. p <_ M ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 )
175	174	adantrl 482	. . . . . . . . . . . 12 |- ( ( ( ph /\ p e. Prime ) /\ ( p <_ K /\ -. p <_ M ) ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 )
176		iftrue 3645	. . . . . . . . . . . . 13 |- ( ( p <_ K /\ -. p <_ M ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) = ( p pCnt ( ( 2 x. N ) _C N ) ) )
177	176	adantl 277	. . . . . . . . . . . 12 |- ( ( ( ph /\ p e. Prime ) /\ ( p <_ K /\ -. p <_ M ) ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) = ( p pCnt ( ( 2 x. N ) _C N ) ) )
178		iftrue 3645	. . . . . . . . . . . . 13 |- ( ( p <_ K /\ -. p <_ M ) -> if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) = 1 )
179	178	adantl 277	. . . . . . . . . . . 12 |- ( ( ( ph /\ p e. Prime ) /\ ( p <_ K /\ -. p <_ M ) ) -> if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) = 1 )
180	175, 177, 179	3brtr4d 4163	. . . . . . . . . . 11 |- ( ( ( ph /\ p e. Prime ) /\ ( p <_ K /\ -. p <_ M ) ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) <_ if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) )
181		0le0 9402	. . . . . . . . . . . . 13 |- 0 <_ 0
182		iffalse 3648	. . . . . . . . . . . . . 14 |- ( -. ( p <_ K /\ -. p <_ M ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) = 0 )
183		iffalse 3648	. . . . . . . . . . . . . 14 |- ( -. ( p <_ K /\ -. p <_ M ) -> if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) = 0 )
184	182, 183	breq12d 4144	. . . . . . . . . . . . 13 |- ( -. ( p <_ K /\ -. p <_ M ) -> ( if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) <_ if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) <-> 0 <_ 0 ) )
185	181, 184	mpbiri 168	. . . . . . . . . . . 12 |- ( -. ( p <_ K /\ -. p <_ M ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) <_ if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) )
186	185	adantl 277	. . . . . . . . . . 11 |- ( ( ( ph /\ p e. Prime ) /\ -. ( p <_ K /\ -. p <_ M ) ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) <_ if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) )
187		zdcle 9732	. . . . . . . . . . . . . 14 |- ( ( p e. ZZ /\ K e. ZZ ) -> DECID p <_ K )
188	126, 77, 187	syl2anr 290	. . . . . . . . . . . . 13 |- ( ( ph /\ p e. Prime ) -> DECID p <_ K )
189		zdcle 9732	. . . . . . . . . . . . . . 15 |- ( ( p e. ZZ /\ M e. ZZ ) -> DECID p <_ M )
190	126, 131, 189	syl2anr 290	. . . . . . . . . . . . . 14 |- ( ( ph /\ p e. Prime ) -> DECID p <_ M )
191		dcn 854	. . . . . . . . . . . . . 14 |- (DECID p <_ M -> DECID -. p <_ M )
192	190, 191	syl 14	. . . . . . . . . . . . 13 |- ( ( ph /\ p e. Prime ) -> DECID -. p <_ M )
193	188, 192	dcand 945	. . . . . . . . . . . 12 |- ( ( ph /\ p e. Prime ) -> DECID ( p <_ K /\ -. p <_ M ) )
194		exmiddc 848	. . . . . . . . . . . 12 |- (DECID ( p <_ K /\ -. p <_ M ) -> ( ( p <_ K /\ -. p <_ M ) \/ -. ( p <_ K /\ -. p <_ M ) ) )
195	193, 194	syl 14	. . . . . . . . . . 11 |- ( ( ph /\ p e. Prime ) -> ( ( p <_ K /\ -. p <_ M ) \/ -. ( p <_ K /\ -. p <_ M ) ) )
196	180, 186, 195	mpjaodan 810	. . . . . . . . . 10 |- ( ( ph /\ p e. Prime ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) <_ if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) )
197	59	adantr 276	. . . . . . . . . . 11 |- ( ( ph /\ p e. Prime ) -> A. n e. Prime ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
198	69	adantr 276	. . . . . . . . . . 11 |- ( ( ph /\ p e. Prime ) -> M e. NN )
199		simpr 110	. . . . . . . . . . 11 |- ( ( ph /\ p e. Prime ) -> p e. Prime )
200		oveq1 6095	. . . . . . . . . . 11 |- ( n = p -> ( n pCnt ( ( 2 x. N ) _C N ) ) = ( p pCnt ( ( 2 x. N ) _C N ) ) )
201	90	adantr 276	. . . . . . . . . . 11 |- ( ( ph /\ p e. Prime ) -> K e. ( ZZ>= ` M ) )
202	55, 197, 198, 199, 200, 201	pcmpt2 13152	. . . . . . . . . 10 |- ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) ) = if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) )
203		eqid 2238	. . . . . . . . . . . . . . . 16 |- ( n e. NN |-> if ( n e. Prime , n , 1 ) ) = ( n e. NN |-> if ( n e. Prime , n , 1 ) )
204	203	prmorcht 16282	. . . . . . . . . . . . . . 15 |- ( K e. NN -> ( exp ` ( theta ` K ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` K ) )
205	97, 204	syl 14	. . . . . . . . . . . . . 14 |- ( ph -> ( exp ` ( theta ` K ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` K ) )
206	203	prmorcht 16282	. . . . . . . . . . . . . . 15 |- ( M e. NN -> ( exp ` ( theta ` M ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` M ) )
207	69, 206	syl 14	. . . . . . . . . . . . . 14 |- ( ph -> ( exp ` ( theta ` M ) ) = ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` M ) )
208	205, 207	oveq12d 6106	. . . . . . . . . . . . 13 |- ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) = ( ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` K ) / ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` M ) ) )
209	208	adantr 276	. . . . . . . . . . . 12 |- ( ( ph /\ p e. Prime ) -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) = ( ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` K ) / ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` M ) ) )
210	209	oveq2d 6104	. . . . . . . . . . 11 |- ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) = ( p pCnt ( ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` K ) / ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` M ) ) ) )
211		nncn 9321	. . . . . . . . . . . . . . . 16 |- ( n e. NN -> n e. CC )
212	211	exp1d 11127	. . . . . . . . . . . . . . 15 |- ( n e. NN -> ( n ^ 1 ) = n )
213	212	ifeq1d 3658	. . . . . . . . . . . . . 14 |- ( n e. NN -> if ( n e. Prime , ( n ^ 1 ) , 1 ) = if ( n e. Prime , n , 1 ) )
214	213	mpteq2ia 4219	. . . . . . . . . . . . 13 |- ( n e. NN |-> if ( n e. Prime , ( n ^ 1 ) , 1 ) ) = ( n e. NN |-> if ( n e. Prime , n , 1 ) )
215	214	eqcomi 2242	. . . . . . . . . . . 12 |- ( n e. NN |-> if ( n e. Prime , n , 1 ) ) = ( n e. NN |-> if ( n e. Prime , ( n ^ 1 ) , 1 ) )
216		1nn0 9590	. . . . . . . . . . . . . . 15 |- 1 e. NN0
217	216	a1i 9	. . . . . . . . . . . . . 14 |- ( ( ph /\ n e. Prime ) -> 1 e. NN0 )
218	217	ralrimiva 2623	. . . . . . . . . . . . 13 |- ( ph -> A. n e. Prime 1 e. NN0 )
219	218	adantr 276	. . . . . . . . . . . 12 |- ( ( ph /\ p e. Prime ) -> A. n e. Prime 1 e. NN0 )
220		eqidd 2239	. . . . . . . . . . . 12 |- ( n = p -> 1 = 1 )
221	215, 219, 198, 199, 220, 201	pcmpt2 13152	. . . . . . . . . . 11 |- ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` K ) / ( seq 1 ( x. , ( n e. NN |-> if ( n e. Prime , n , 1 ) ) ) ` M ) ) ) = if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) )
222	210, 221	eqtrd 2271	. . . . . . . . . 10 |- ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) = if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) )
223	196, 202, 222	3brtr4d 4163	. . . . . . . . 9 |- ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) ) <_ ( p pCnt ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) )
224	223	ralrimiva 2623	. . . . . . . 8 |- ( ph -> A. p e. Prime ( p pCnt ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) ) <_ ( p pCnt ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) )
225		pc2dvds 13138	. . . . . . . . 9 |- ( ( ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) e. ZZ /\ ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. ZZ ) -> ( ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) || ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) <-> A. p e. Prime ( p pCnt ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) ) <_ ( p pCnt ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) ) )
226	102, 121, 225	syl2anc 415	. . . . . . . 8 |- ( ph -> ( ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) || ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) <-> A. p e. Prime ( p pCnt ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) ) <_ ( p pCnt ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) ) )
227	224, 226	mpbird 167	. . . . . . 7 |- ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) || ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) )
228	117	nnred 9326	. . . . . . . . . 10 |- ( ph -> ( exp ` ( theta ` K ) ) e. RR )
229	113	nnred 9326	. . . . . . . . . 10 |- ( ph -> ( exp ` ( theta ` M ) ) e. RR )
230	117	nngt0d 9357	. . . . . . . . . 10 |- ( ph -> 0 < ( exp ` ( theta ` K ) ) )
231	113	nngt0d 9357	. . . . . . . . . 10 |- ( ph -> 0 < ( exp ` ( theta ` M ) ) )
232	228, 229, 230, 231	divgt0d 9273	. . . . . . . . 9 |- ( ph -> 0 < ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) )
233		elnnz 9665	. . . . . . . . 9 |- ( ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. NN <-> ( ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. ZZ /\ 0 < ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) )
234	121, 232, 233	sylanbrc 421	. . . . . . . 8 |- ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. NN )
235		dvdsle 12636	. . . . . . . 8 |- ( ( ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) e. ZZ /\ ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. NN ) -> ( ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) || ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) <_ ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) )
236	102, 234, 235	syl2anc 415	. . . . . . 7 |- ( ph -> ( ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) || ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) <_ ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) )
237	227, 236	mpd 13	. . . . . 6 |- ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) <_ ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) )
238		nndivre 9349	. . . . . . . 8 |- ( ( ( exp ` ( theta ` K ) ) e. RR /\ 4 e. NN ) -> ( ( exp ` ( theta ` K ) ) / 4 ) e. RR )
239	228, 1, 238	sylancl 417	. . . . . . 7 |- ( ph -> ( ( exp ` ( theta ` K ) ) / 4 ) e. RR )
240		4re 9390	. . . . . . . . . 10 |- 4 e. RR
241	240	a1i 9	. . . . . . . . 9 |- ( ph -> 4 e. RR )
242		6re 9394	. . . . . . . . . 10 |- 6 e. RR
243	242	a1i 9	. . . . . . . . 9 |- ( ph -> 6 e. RR )
244		4lt6 9496	. . . . . . . . . 10 |- 4 < 6
245	244	a1i 9	. . . . . . . . 9 |- ( ph -> 4 < 6 )
246		cht3 16277	. . . . . . . . . . . 12 |- ( theta ` 3 ) = ( log ` 6 )
247	246	fveq2i 5701	. . . . . . . . . . 11 |- ( exp ` ( theta ` 3 ) ) = ( exp ` ( log ` 6 ) )
248		6pos 9414	. . . . . . . . . . . . 13 |- 0 < 6
249	242, 248	elrpii 10074	. . . . . . . . . . . 12 |- 6 e. RR+
250		reeflog 16092	. . . . . . . . . . . 12 |- ( 6 e. RR+ -> ( exp ` ( log ` 6 ) ) = 6 )
251	249, 250	ax-mp 5	. . . . . . . . . . 11 |- ( exp ` ( log ` 6 ) ) = 6
252	247, 251	eqtri 2259	. . . . . . . . . 10 |- ( exp ` ( theta ` 3 ) ) = 6
253		3z 9684	. . . . . . . . . . . . . 14 |- 3 e. ZZ
254		zq 10042	. . . . . . . . . . . . . 14 |- ( 3 e. ZZ -> 3 e. QQ )
255	253, 254	ax-mp 5	. . . . . . . . . . . . 13 |- 3 e. QQ
256	255	a1i 9	. . . . . . . . . . . 12 |- ( ph -> 3 e. QQ )
257		eluzle 9950	. . . . . . . . . . . . 13 |- ( M e. ( ZZ>= ` 3 ) -> 3 <_ M )
258	67, 257	syl 14	. . . . . . . . . . . 12 |- ( ph -> 3 <_ M )
259		chtqwordi 16263	. . . . . . . . . . . 12 |- ( ( 3 e. QQ /\ M e. QQ /\ 3 <_ M ) -> ( theta ` 3 ) <_ ( theta ` M ) )
260	256, 105, 258, 259	syl3anc 1278	. . . . . . . . . . 11 |- ( ph -> ( theta ` 3 ) <_ ( theta ` M ) )
261		chtqcl 16244	. . . . . . . . . . . . 13 |- ( 3 e. QQ -> ( theta ` 3 ) e. RR )
262	255, 261	ax-mp 5	. . . . . . . . . . . 12 |- ( theta ` 3 ) e. RR
263		chtqcl 16244	. . . . . . . . . . . . 13 |- ( M e. QQ -> ( theta ` M ) e. RR )
264	105, 263	syl 14	. . . . . . . . . . . 12 |- ( ph -> ( theta ` M ) e. RR )
265		efle 16002	. . . . . . . . . . . 12 |- ( ( ( theta ` 3 ) e. RR /\ ( theta ` M ) e. RR ) -> ( ( theta ` 3 ) <_ ( theta ` M ) <-> ( exp ` ( theta ` 3 ) ) <_ ( exp ` ( theta ` M ) ) ) )
266	262, 264, 265	sylancr 418	. . . . . . . . . . 11 |- ( ph -> ( ( theta ` 3 ) <_ ( theta ` M ) <-> ( exp ` ( theta ` 3 ) ) <_ ( exp ` ( theta ` M ) ) ) )
267	260, 266	mpbid 147	. . . . . . . . . 10 |- ( ph -> ( exp ` ( theta ` 3 ) ) <_ ( exp ` ( theta ` M ) ) )
268	252, 267	eqbrtrrid 4167	. . . . . . . . 9 |- ( ph -> 6 <_ ( exp ` ( theta ` M ) ) )
269	241, 243, 229, 245, 268	ltletrd 8758	. . . . . . . 8 |- ( ph -> 4 < ( exp ` ( theta ` M ) ) )
270		4pos 9410	. . . . . . . . . 10 |- 0 < 4
271	270	a1i 9	. . . . . . . . 9 |- ( ph -> 0 < 4 )
272		ltdiv2 9225	. . . . . . . . 9 |- ( ( ( 4 e. RR /\ 0 < 4 ) /\ ( ( exp ` ( theta ` M ) ) e. RR /\ 0 < ( exp ` ( theta ` M ) ) ) /\ ( ( exp ` ( theta ` K ) ) e. RR /\ 0 < ( exp ` ( theta ` K ) ) ) ) -> ( 4 < ( exp ` ( theta ` M ) ) <-> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) < ( ( exp ` ( theta ` K ) ) / 4 ) ) )
273	241, 271, 229, 231, 228, 230, 272	syl222anc 1294	. . . . . . . 8 |- ( ph -> ( 4 < ( exp ` ( theta ` M ) ) <-> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) < ( ( exp ` ( theta ` K ) ) / 4 ) ) )
274	269, 273	mpbid 147	. . . . . . 7 |- ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) < ( ( exp ` ( theta ` K ) ) / 4 ) )
275	26	a1i 9	. . . . . . . . . . . . 13 |- ( ph -> 2 e. RR )
276		3re 9387	. . . . . . . . . . . . . 14 |- 3 e. RR
277	276	a1i 9	. . . . . . . . . . . . 13 |- ( ph -> 3 e. RR )
278	77	zred 9779	. . . . . . . . . . . . 13 |- ( ph -> K e. RR )
279		2lt3 9486	. . . . . . . . . . . . . 14 |- 2 < 3
280	279	a1i 9	. . . . . . . . . . . . 13 |- ( ph -> 2 < 3 )
281	69	nnred 9326	. . . . . . . . . . . . . 14 |- ( ph -> M e. RR )
282	277, 281, 278, 258, 109	letrd 8457	. . . . . . . . . . . . 13 |- ( ph -> 3 <_ K )
283	275, 277, 278, 280, 282	ltletrd 8758	. . . . . . . . . . . 12 |- ( ph -> 2 < K )
284		chtqub 16296	. . . . . . . . . . . 12 |- ( ( K e. QQ /\ 2 < K ) -> ( theta ` K ) < ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) )
285	107, 283, 284	syl2anc 415	. . . . . . . . . . 11 |- ( ph -> ( theta ` K ) < ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) )
286		chtqcl 16244	. . . . . . . . . . . . 13 |- ( K e. QQ -> ( theta ` K ) e. RR )
287	107, 286	syl 14	. . . . . . . . . . . 12 |- ( ph -> ( theta ` K ) e. RR )
288		relogcl 16091	. . . . . . . . . . . . . 14 |- ( 2 e. RR+ -> ( log ` 2 ) e. RR )
289	31, 288	ax-mp 5	. . . . . . . . . . . . 13 |- ( log ` 2 ) e. RR
290		zsubcl 9696	. . . . . . . . . . . . . . 15 |- ( ( ( 2 x. K ) e. ZZ /\ 3 e. ZZ ) -> ( ( 2 x. K ) - 3 ) e. ZZ )
291	79, 253, 290	sylancl 417	. . . . . . . . . . . . . 14 |- ( ph -> ( ( 2 x. K ) - 3 ) e. ZZ )
292	291	zred 9779	. . . . . . . . . . . . 13 |- ( ph -> ( ( 2 x. K ) - 3 ) e. RR )
293		remulcl 8313	. . . . . . . . . . . . 13 |- ( ( ( log ` 2 ) e. RR /\ ( ( 2 x. K ) - 3 ) e. RR ) -> ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) e. RR )
294	289, 292, 293	sylancr 418	. . . . . . . . . . . 12 |- ( ph -> ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) e. RR )
295		eflt 16001	. . . . . . . . . . . 12 |- ( ( ( theta ` K ) e. RR /\ ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) e. RR ) -> ( ( theta ` K ) < ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) <-> ( exp ` ( theta ` K ) ) < ( exp ` ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) ) ) )
296	287, 294, 295	syl2anc 415	. . . . . . . . . . 11 |- ( ph -> ( ( theta ` K ) < ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) <-> ( exp ` ( theta ` K ) ) < ( exp ` ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) ) ) )
297	285, 296	mpbid 147	. . . . . . . . . 10 |- ( ph -> ( exp ` ( theta ` K ) ) < ( exp ` ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) ) )
298		reexplog 16101	. . . . . . . . . . . 12 |- ( ( 2 e. RR+ /\ ( ( 2 x. K ) - 3 ) e. ZZ ) -> ( 2 ^ ( ( 2 x. K ) - 3 ) ) = ( exp ` ( ( ( 2 x. K ) - 3 ) x. ( log ` 2 ) ) ) )
299	31, 291, 298	sylancr 418	. . . . . . . . . . 11 |- ( ph -> ( 2 ^ ( ( 2 x. K ) - 3 ) ) = ( exp ` ( ( ( 2 x. K ) - 3 ) x. ( log ` 2 ) ) ) )
300	291	zcnd 9780	. . . . . . . . . . . . 13 |- ( ph -> ( ( 2 x. K ) - 3 ) e. CC )
301	289	recni 8344	. . . . . . . . . . . . 13 |- ( log ` 2 ) e. CC
302		mulcom 8314	. . . . . . . . . . . . 13 |- ( ( ( ( 2 x. K ) - 3 ) e. CC /\ ( log ` 2 ) e. CC ) -> ( ( ( 2 x. K ) - 3 ) x. ( log ` 2 ) ) = ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) )
303	300, 301, 302	sylancl 417	. . . . . . . . . . . 12 |- ( ph -> ( ( ( 2 x. K ) - 3 ) x. ( log ` 2 ) ) = ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) )
304	303	fveq2d 5702	. . . . . . . . . . 11 |- ( ph -> ( exp ` ( ( ( 2 x. K ) - 3 ) x. ( log ` 2 ) ) ) = ( exp ` ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) ) )
305	299, 304	eqtrd 2271	. . . . . . . . . 10 |- ( ph -> ( 2 ^ ( ( 2 x. K ) - 3 ) ) = ( exp ` ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) ) )
306	297, 305	breqtrrd 4159	. . . . . . . . 9 |- ( ph -> ( exp ` ( theta ` K ) ) < ( 2 ^ ( ( 2 x. K ) - 3 ) ) )
307		3p2e5 9455	. . . . . . . . . . . . . . . 16 |- ( 3 + 2 ) = 5
308	307	oveq1i 6098	. . . . . . . . . . . . . . 15 |- ( ( 3 + 2 ) - 2 ) = ( 5 - 2 )
309		3cn 9388	. . . . . . . . . . . . . . . 16 |- 3 e. CC
310		2cn 9384	. . . . . . . . . . . . . . . 16 |- 2 e. CC
311	309, 310	pncan3oi 8549	. . . . . . . . . . . . . . 15 |- ( ( 3 + 2 ) - 2 ) = 3
312	308, 311	eqtr3i 2261	. . . . . . . . . . . . . 14 |- ( 5 - 2 ) = 3
313	312	oveq2i 6099	. . . . . . . . . . . . 13 |- ( ( 2 x. K ) - ( 5 - 2 ) ) = ( ( 2 x. K ) - 3 )
314	79	zcnd 9780	. . . . . . . . . . . . . 14 |- ( ph -> ( 2 x. K ) e. CC )
315		5cn 9393	. . . . . . . . . . . . . . 15 |- 5 e. CC
316		subsub 8563	. . . . . . . . . . . . . . 15 |- ( ( ( 2 x. K ) e. CC /\ 5 e. CC /\ 2 e. CC ) -> ( ( 2 x. K ) - ( 5 - 2 ) ) = ( ( ( 2 x. K ) - 5 ) + 2 ) )
317	315, 310, 316	mp3an23 1370	. . . . . . . . . . . . . 14 |- ( ( 2 x. K ) e. CC -> ( ( 2 x. K ) - ( 5 - 2 ) ) = ( ( ( 2 x. K ) - 5 ) + 2 ) )
318	314, 317	syl 14	. . . . . . . . . . . . 13 |- ( ph -> ( ( 2 x. K ) - ( 5 - 2 ) ) = ( ( ( 2 x. K ) - 5 ) + 2 ) )
319	313, 318	eqtr3id 2285	. . . . . . . . . . . 12 |- ( ph -> ( ( 2 x. K ) - 3 ) = ( ( ( 2 x. K ) - 5 ) + 2 ) )
320	319	oveq2d 6104	. . . . . . . . . . 11 |- ( ph -> ( 2 ^c ( ( 2 x. K ) - 3 ) ) = ( 2 ^c ( ( ( 2 x. K ) - 5 ) + 2 ) ) )
321		cxpexpnn 16129	. . . . . . . . . . . 12 |- ( ( 2 e. NN /\ ( ( 2 x. K ) - 3 ) e. ZZ ) -> ( 2 ^c ( ( 2 x. K ) - 3 ) ) = ( 2 ^ ( ( 2 x. K ) - 3 ) ) )
322	16, 291, 321	sylancr 418	. . . . . . . . . . 11 |- ( ph -> ( 2 ^c ( ( 2 x. K ) - 3 ) ) = ( 2 ^ ( ( 2 x. K ) - 3 ) ) )
323	82	zcnd 9780	. . . . . . . . . . . 12 |- ( ph -> ( ( 2 x. K ) - 5 ) e. CC )
324		rpcxpadd 16138	. . . . . . . . . . . . 13 |- ( ( 2 e. RR+ /\ ( ( 2 x. K ) - 5 ) e. CC /\ 2 e. CC ) -> ( 2 ^c ( ( ( 2 x. K ) - 5 ) + 2 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. ( 2 ^c 2 ) ) )
325	31, 310, 324	mp3an13 1369	. . . . . . . . . . . 12 |- ( ( ( 2 x. K ) - 5 ) e. CC -> ( 2 ^c ( ( ( 2 x. K ) - 5 ) + 2 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. ( 2 ^c 2 ) ) )
326	323, 325	syl 14	. . . . . . . . . . 11 |- ( ph -> ( 2 ^c ( ( ( 2 x. K ) - 5 ) + 2 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. ( 2 ^c 2 ) ) )
327	320, 322, 326	3eqtr3d 2279	. . . . . . . . . 10 |- ( ph -> ( 2 ^ ( ( 2 x. K ) - 3 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. ( 2 ^c 2 ) ) )
328		cxpexpnn 16129	. . . . . . . . . . . . 13 |- ( ( 2 e. NN /\ 2 e. ZZ ) -> ( 2 ^c 2 ) = ( 2 ^ 2 ) )
329	16, 72, 328	mp2an 430	. . . . . . . . . . . 12 |- ( 2 ^c 2 ) = ( 2 ^ 2 )
330		sq2 11093	. . . . . . . . . . . 12 |- ( 2 ^ 2 ) = 4
331	329, 330	eqtri 2259	. . . . . . . . . . 11 |- ( 2 ^c 2 ) = 4
332	331	oveq2i 6099	. . . . . . . . . 10 |- ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. ( 2 ^c 2 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. 4 )
333	327, 332	eqtrdi 2287	. . . . . . . . 9 |- ( ph -> ( 2 ^ ( ( 2 x. K ) - 3 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. 4 ) )
334	306, 333	breqtrd 4157	. . . . . . . 8 |- ( ph -> ( exp ` ( theta ` K ) ) < ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. 4 ) )
335	240, 270	pm3.2i 272	. . . . . . . . . 10 |- ( 4 e. RR /\ 0 < 4 )
336	335	a1i 9	. . . . . . . . 9 |- ( ph -> ( 4 e. RR /\ 0 < 4 ) )
337		ltdivmul2 9216	. . . . . . . . 9 |- ( ( ( exp ` ( theta ` K ) ) e. RR /\ ( 2 ^c ( ( 2 x. K ) - 5 ) ) e. RR /\ ( 4 e. RR /\ 0 < 4 ) ) -> ( ( ( exp ` ( theta ` K ) ) / 4 ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) <-> ( exp ` ( theta ` K ) ) < ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. 4 ) ) )
338	228, 86, 336, 337	syl3anc 1278	. . . . . . . 8 |- ( ph -> ( ( ( exp ` ( theta ` K ) ) / 4 ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) <-> ( exp ` ( theta ` K ) ) < ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. 4 ) ) )
339	334, 338	mpbird 167	. . . . . . 7 |- ( ph -> ( ( exp ` ( theta ` K ) ) / 4 ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) )
340	122, 239, 86, 274, 339	lttrd 8459	. . . . . 6 |- ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) )
341	103, 122, 86, 237, 340	lelttrd 8458	. . . . 5 |- ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) )
342	98	nnred 9326	. . . . . 6 |- ( ph -> ( seq 1 ( x. , F ) ` K ) e. RR )
343		nnre 9320	. . . . . . . 8 |- ( ( seq 1 ( x. , F ) ` M ) e. NN -> ( seq 1 ( x. , F ) ` M ) e. RR )
344		nngt0 9338	. . . . . . . 8 |- ( ( seq 1 ( x. , F ) ` M ) e. NN -> 0 < ( seq 1 ( x. , F ) ` M ) )
345	343, 344	jca 306	. . . . . . 7 |- ( ( seq 1 ( x. , F ) ` M ) e. NN -> ( ( seq 1 ( x. , F ) ` M ) e. RR /\ 0 < ( seq 1 ( x. , F ) ` M ) ) )
346	70, 345	syl 14	. . . . . 6 |- ( ph -> ( ( seq 1 ( x. , F ) ` M ) e. RR /\ 0 < ( seq 1 ( x. , F ) ` M ) ) )
347		ltdivmul 9214	. . . . . 6 |- ( ( ( seq 1 ( x. , F ) ` K ) e. RR /\ ( 2 ^c ( ( 2 x. K ) - 5 ) ) e. RR /\ ( ( seq 1 ( x. , F ) ` M ) e. RR /\ 0 < ( seq 1 ( x. , F ) ` M ) ) ) -> ( ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) <-> ( seq 1 ( x. , F ) ` K ) < ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) ) )
348	342, 86, 346, 347	syl3anc 1278	. . . . 5 |- ( ph -> ( ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) <-> ( seq 1 ( x. , F ) ` K ) < ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) ) )
349	341, 348	mpbid 147	. . . 4 |- ( ph -> ( seq 1 ( x. , F ) ` K ) < ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) )
350	88, 349	eqbrtrrd 4155	. . 3 |- ( ph -> ( ( 2 x. N ) _C N ) < ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) )
351	30, 86	remulcld 8362	. . . 4 |- ( ph -> ( ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) e. RR )
352	3, 62, 55, 63, 64	bposlem5 16315	. . . . 5 |- ( ph -> ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) )
353	71, 30, 85	lemul1d 10158	. . . . 5 |- ( ph -> ( ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) <-> ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) <_ ( ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) ) )
354	352, 353	mpbid 147	. . . 4 |- ( ph -> ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) <_ ( ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) )
355	79	zred 9779	. . . . . . 7 |- ( ph -> ( 2 x. K ) e. RR )
356	37	a1i 9	. . . . . . 7 |- ( ph -> 5 e. RR )
357		flqle 10732	. . . . . . . . . . 11 |- ( ( ( 2 x. N ) / 3 ) e. QQ -> ( |_ ` ( ( 2 x. N ) / 3 ) ) <_ ( ( 2 x. N ) / 3 ) )
358	75, 357	syl 14	. . . . . . . . . 10 |- ( ph -> ( |_ ` ( ( 2 x. N ) / 3 ) ) <_ ( ( 2 x. N ) / 3 ) )
359	63, 358	eqbrtrid 4166	. . . . . . . . 9 |- ( ph -> K <_ ( ( 2 x. N ) / 3 ) )
360		nndivre 9349	. . . . . . . . . . 11 |- ( ( ( 2 x. N ) e. RR /\ 3 e. NN ) -> ( ( 2 x. N ) / 3 ) e. RR )
361	20, 23, 360	sylancl 417	. . . . . . . . . 10 |- ( ph -> ( ( 2 x. N ) / 3 ) e. RR )
362		2pos 9404	. . . . . . . . . . . 12 |- 0 < 2
363	26, 362	pm3.2i 272	. . . . . . . . . . 11 |- ( 2 e. RR /\ 0 < 2 )
364	363	a1i 9	. . . . . . . . . 10 |- ( ph -> ( 2 e. RR /\ 0 < 2 ) )
365		lemul2 9195	. . . . . . . . . 10 |- ( ( K e. RR /\ ( ( 2 x. N ) / 3 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( K <_ ( ( 2 x. N ) / 3 ) <-> ( 2 x. K ) <_ ( 2 x. ( ( 2 x. N ) / 3 ) ) ) )
366	278, 361, 364, 365	syl3anc 1278	. . . . . . . . 9 |- ( ph -> ( K <_ ( ( 2 x. N ) / 3 ) <-> ( 2 x. K ) <_ ( 2 x. ( ( 2 x. N ) / 3 ) ) ) )
367	359, 366	mpbid 147	. . . . . . . 8 |- ( ph -> ( 2 x. K ) <_ ( 2 x. ( ( 2 x. N ) / 3 ) ) )
368	18	nncnd 9327	. . . . . . . . . 10 |- ( ph -> ( 2 x. N ) e. CC )
369		3ap0 9409	. . . . . . . . . . . 12 |- 3 # 0
370	309, 369	pm3.2i 272	. . . . . . . . . . 11 |- ( 3 e. CC /\ 3 # 0 )
371		divassap 9028	. . . . . . . . . . 11 |- ( ( 2 e. CC /\ ( 2 x. N ) e. CC /\ ( 3 e. CC /\ 3 # 0 ) ) -> ( ( 2 x. ( 2 x. N ) ) / 3 ) = ( 2 x. ( ( 2 x. N ) / 3 ) ) )
372	310, 370, 371	mp3an13 1369	. . . . . . . . . 10 |- ( ( 2 x. N ) e. CC -> ( ( 2 x. ( 2 x. N ) ) / 3 ) = ( 2 x. ( ( 2 x. N ) / 3 ) ) )
373	368, 372	syl 14	. . . . . . . . 9 |- ( ph -> ( ( 2 x. ( 2 x. N ) ) / 3 ) = ( 2 x. ( ( 2 x. N ) / 3 ) ) )
374	5	nncnd 9327	. . . . . . . . . . . 12 |- ( ph -> N e. CC )
375		mulass 8316	. . . . . . . . . . . 12 |- ( ( 2 e. CC /\ 2 e. CC /\ N e. CC ) -> ( ( 2 x. 2 ) x. N ) = ( 2 x. ( 2 x. N ) ) )
376	310, 310, 374, 375	mp3an12i 1382	. . . . . . . . . . 11 |- ( ph -> ( ( 2 x. 2 ) x. N ) = ( 2 x. ( 2 x. N ) ) )
377		2t2e4 9468	. . . . . . . . . . . 12 |- ( 2 x. 2 ) = 4
378	377	oveq1i 6098	. . . . . . . . . . 11 |- ( ( 2 x. 2 ) x. N ) = ( 4 x. N )
379	376, 378	eqtr3di 2286	. . . . . . . . . 10 |- ( ph -> ( 2 x. ( 2 x. N ) ) = ( 4 x. N ) )
380	379	oveq1d 6103	. . . . . . . . 9 |- ( ph -> ( ( 2 x. ( 2 x. N ) ) / 3 ) = ( ( 4 x. N ) / 3 ) )
381	373, 380	eqtr3d 2273	. . . . . . . 8 |- ( ph -> ( 2 x. ( ( 2 x. N ) / 3 ) ) = ( ( 4 x. N ) / 3 ) )
382	367, 381	breqtrd 4157	. . . . . . 7 |- ( ph -> ( 2 x. K ) <_ ( ( 4 x. N ) / 3 ) )
383	355, 36, 356, 382	lesub1dd 8896	. . . . . 6 |- ( ph -> ( ( 2 x. K ) - 5 ) <_ ( ( ( 4 x. N ) / 3 ) - 5 ) )
384		1lt2 9485	. . . . . . . 8 |- 1 < 2
385	384	a1i 9	. . . . . . 7 |- ( ph -> 1 < 2 )
386	275, 385, 83, 39	cxpled 16164	. . . . . 6 |- ( ph -> ( ( ( 2 x. K ) - 5 ) <_ ( ( ( 4 x. N ) / 3 ) - 5 ) <-> ( 2 ^c ( ( 2 x. K ) - 5 ) ) <_ ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )
387	383, 386	mpbid 147	. . . . 5 |- ( ph -> ( 2 ^c ( ( 2 x. K ) - 5 ) ) <_ ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) )
388	86, 42, 29	lemul2d 10159	. . . . 5 |- ( ph -> ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) <_ ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) <-> ( ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) <_ ( ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) ) )
389	387, 388	mpbid 147	. . . 4 |- ( ph -> ( ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) <_ ( ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )
390	87, 351, 43, 354, 389	letrd 8457	. . 3 |- ( ph -> ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) <_ ( ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )
391	15, 87, 43, 350, 390	ltletrd 8758	. 2 |- ( ph -> ( ( 2 x. N ) _C N ) < ( ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )
392	10, 15, 43, 54, 391	lttrd 8459	1 |- ( ph -> ( ( 4 ^ N ) / N ) < ( ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 720  DECID wdc 846   = wceq 1402   e. wcel 2209   =/= wne 2420   A.wral 2528   E.wrex 2529   ifcif 3638   class class class wbr 4131   |-> cmpt 4193   -->wf 5376   ` 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   NN0cn0 9574   ZZcz 9655   ZZ>=cuz 9937   QQcq 10035   RR+crp 10071   ...cfz 10428   |_cfl 10720   seqcseq 10905   ^cexp 10996   _C cbc 11207   sqrcsqrt 11784   expce 12434   || cdvds 12579   Primecprime 12910   pCnt cpc 13092   logclog 16085   ^c ccxp 16086   thetaccht 16233

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:  bposlem9  16319