Theorem bposlem6 16245

Description: Lemma for bpos 16249. 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 9473	. . . . 5 |- 4 e. NN
2		5nn 9474	. . . . . . 7 |- 5 e. NN
3		bpos.1	. . . . . . 7 |- ( ph -> N e. ( ZZ>= ` 5 ) )
4		eluznn 10010	. . . . . . 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 9625	. . . . 5 |- ( ph -> N e. NN0 )
7		nnexpcl 11004	. . . . 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 9320	. . 3 |- ( ph -> ( 4 ^ N ) e. RR )
10	9, 5	nndivred 9357	. 2 |- ( ph -> ( ( 4 ^ N ) / N ) e. RR )
11		fzctr 10551	. . . . 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 11222	. . . 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 9320	. 2 |- ( ph -> ( ( 2 x. N ) _C N ) e. RR )
16		2nn 9471	. . . . . . 7 |- 2 e. NN
17		nnmulcl 9328	. . . . . . 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 10106	. . . . 5 |- ( ph -> ( 2 x. N ) e. RR+ )
20	18	nnred 9320	. . . . . . . 8 |- ( ph -> ( 2 x. N ) e. RR )
21	19	rpge0d 10112	. . . . . . . 8 |- ( ph -> 0 <_ ( 2 x. N ) )
22	20, 21	resqrtcld 11946	. . . . . . 7 |- ( ph -> ( sqr ` ( 2 x. N ) ) e. RR )
23		3nn 9472	. . . . . . 7 |- 3 e. NN
24		nndivre 9343	. . . . . . 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 9377	. . . . . 6 |- 2 e. RR
27		readdcl 8306	. . . . . 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 16098	. . . 4 |- ( ph -> ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) e. RR+ )
30	29	rpred 10108	. . 3 |- ( ph -> ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) e. RR )
31		2rp 10070	. . . . 5 |- 2 e. RR+
32		nnmulcl 9328	. . . . . . . . 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 9320	. . . . . . 7 |- ( ph -> ( 4 x. N ) e. RR )
35		nndivre 9343	. . . . . . 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 9386	. . . . . 6 |- 5 e. RR
38		resubcl 8592	. . . . . 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 16068	. . . . 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 10108	. . 3 |- ( ph -> ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) e. RR )
43	30, 42	remulcld 8357	. 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 9369	. . . . 5 |- 5 = ( 4 + 1 )
45		4z 9679	. . . . . 6 |- 4 e. ZZ
46		uzid 9946	. . . . . 6 |- ( 4 e. ZZ -> 4 e. ( ZZ>= ` 4 ) )
47		peano2uz 9993	. . . . . 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 9950	. . . 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 16236	. . 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 13101	. . . . . . . . . 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 13144	. . . . . . 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 16243	. . . . . . . 8 |- ( ph -> M e. ( 3 ... K ) )
66		elfzuz 10435	. . . . . . . 8 |- ( M e. ( 3 ... K ) -> M e. ( ZZ>= ` 3 ) )
67	65, 66	syl 14	. . . . . . 7 |- ( ph -> M e. ( ZZ>= ` 3 ) )
68		eluznn 10010	. . . . . . 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 5844	. . . . 5 |- ( ph -> ( seq 1 ( x. , F ) ` M ) e. NN )
71	70	nnred 9320	. . . 4 |- ( ph -> ( seq 1 ( x. , F ) ` M ) e. RR )
72		2z 9677	. . . . . . . . 9 |- 2 e. ZZ
73	18	nnzd 9772	. . . . . . . . . . . 12 |- ( ph -> ( 2 x. N ) e. ZZ )
74		znq 10034	. . . . . . . . . . . 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 10725	. . . . . . . . . 10 |- ( ph -> ( |_ ` ( ( 2 x. N ) / 3 ) ) e. ZZ )
77	63, 76	eqeltrid 2325	. . . . . . . . 9 |- ( ph -> K e. ZZ )
78		zmulcl 9703	. . . . . . . . 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 9670	. . . . . . . 8 |- 5 e. ZZ
81		zsubcl 9690	. . . . . . . 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 9773	. . . . . 6 |- ( ph -> ( ( 2 x. K ) - 5 ) e. RR )
84		rpcxpcl 16068	. . . . . 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 10108	. . . 4 |- ( ph -> ( 2 ^c ( ( 2 x. K ) - 5 ) ) e. RR )
87	71, 86	remulcld 8357	. . 3 |- ( ph -> ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) e. RR )
88	3, 62, 55, 63	bposlem3 16242	. . . 4 |- ( ph -> ( seq 1 ( x. , F ) ` K ) = ( ( 2 x. N ) _C N ) )
89		elfzuz3 10436	. . . . . . . . . 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 13147	. . . . . . . 8 |- ( ph -> ( seq 1 ( x. , F ) ` M ) || ( seq 1 ( x. , F ) ` K ) )
92	70	nnzd 9772	. . . . . . . . 9 |- ( ph -> ( seq 1 ( x. , F ) ` M ) e. ZZ )
93	70	nnne0d 9352	. . . . . . . . 9 |- ( ph -> ( seq 1 ( x. , F ) ` M ) =/= 0 )
94		uztrn 9949	. . . . . . . . . . . . 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 10010	. . . . . . . . . . . 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 5844	. . . . . . . . . 10 |- ( ph -> ( seq 1 ( x. , F ) ` K ) e. NN )
99	98	nnzd 9772	. . . . . . . . 9 |- ( ph -> ( seq 1 ( x. , F ) ` K ) e. ZZ )
100		dvdsval2 12576	. . . . . . . . 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 9773	. . . . . 6 |- ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) e. RR )
104		nnq 10043	. . . . . . . . . 10 |- ( M e. NN -> M e. QQ )
105	69, 104	syl 14	. . . . . . . . 9 |- ( ph -> M e. QQ )
106		zq 10036	. . . . . . . . . 10 |- ( K e. ZZ -> K e. QQ )
107	77, 106	syl 14	. . . . . . . . 9 |- ( ph -> K e. QQ )
108		eluzle 9944	. . . . . . . . . 10 |- ( K e. ( ZZ>= ` M ) -> M <_ K )
109	90, 108	syl 14	. . . . . . . . 9 |- ( ph -> M <_ K )
110		efchtqdvds 16194	. . . . . . . . 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 16175	. . . . . . . . . . 11 |- ( M e. QQ -> ( exp ` ( theta ` M ) ) e. NN )
113	105, 112	syl 14	. . . . . . . . . 10 |- ( ph -> ( exp ` ( theta ` M ) ) e. NN )
114	113	nnzd 9772	. . . . . . . . 9 |- ( ph -> ( exp ` ( theta ` M ) ) e. ZZ )
115	113	nnne0d 9352	. . . . . . . . 9 |- ( ph -> ( exp ` ( theta ` M ) ) =/= 0 )
116		efchtqcl 16175	. . . . . . . . . . 11 |- ( K e. QQ -> ( exp ` ( theta ` K ) ) e. NN )
117	107, 116	syl 14	. . . . . . . . . 10 |- ( ph -> ( exp ` ( theta ` K ) ) e. NN )
118	117	nnzd 9772	. . . . . . . . 9 |- ( ph -> ( exp ` ( theta ` K ) ) e. ZZ )
119		dvdsval2 12576	. . . . . . . . 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 9773	. . . . . 6 |- ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. RR )
123	18	nnnn0d 9625	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( 2 x. N ) e. NN0 )
124		sqrtrirr 13008	. . . . . . . . . . . . . . . . . . 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 12908	. . . . . . . . . . . . . . . . . 18 |- ( p e. Prime -> p e. ZZ )
127		flaplt 10733	. . . . . . . . . . . . . . . . . 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 4137	. . . . . . . . . . . . . . . . 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 9772	. . . . . . . . . . . . . . . . 17 |- ( ph -> M e. ZZ )
132		zltnle 9695	. . . . . . . . . . . . . . . . 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 16240	. . . . . . . . . . . . . . . . . . . 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 9773	. . . . . . . . . . . . . . . . . . . . . 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 13101	. . . . . . . . . . . . . . . . . . . . . 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 11143	. . . . . . . . . . . . . . . . . . . 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 11152	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ p e. Prime ) -> ( p ^ 2 ) e. RR )
145		lelttr 8415	. . . . . . . . . . . . . . . . . . . 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 11813	. . . . . . . . . . . . . . . . . . . . 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 4140	. . . . . . . . . . . . . . . . . . 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 9771	. . . . . . . . . . . . . . . . . . 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 12930	. . . . . . . . . . . . . . . . . . . 20 |- ( p e. Prime -> 1 < p )
155	154	adantl 277	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ p e. Prime ) -> 1 < p )
156	138, 152, 153, 155	ltexp2d 16107	. . . . . . . . . . . . . . . . . 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 9366	. . . . . . . . . . . . . . . . . 18 |- 2 = ( 1 + 1 )
159	158	breq2i 4138	. . . . . . . . . . . . . . . . 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 11949	. . . . . . . . . . . . . . . . . 18 |- ( ph -> 0 <_ ( sqr ` ( 2 x. N ) ) )
163	162	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ p e. Prime ) -> 0 <_ ( sqr ` ( 2 x. N ) ) )
164		prmnn 12907	. . . . . . . . . . . . . . . . . . . 20 |- ( p e. Prime -> p e. NN )
165	164	nnrpd 10106	. . . . . . . . . . . . . . . . . . 19 |- ( p e. Prime -> p e. RR+ )
166	165	rpge0d 10112	. . . . . . . . . . . . . . . . . 18 |- ( p e. Prime -> 0 <_ p )
167	166	adantl 277	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ p e. Prime ) -> 0 <_ p )
168	161, 138, 163, 167	lt2sqd 11157	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ p e. Prime ) -> ( ( sqr ` ( 2 x. N ) ) < p <-> ( ( sqr ` ( 2 x. N ) ) ^ 2 ) < ( p ^ 2 ) ) )
169		1z 9675	. . . . . . . . . . . . . . . . 17 |- 1 e. ZZ
170		zleltp1 9705	. . . . . . . . . . . . . . . . 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 4162	. . . . . . . . . . 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 9396	. . . . . . . . . . . . 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 4143	. . . . . . . . . . . . 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 9726	. . . . . . . . . . . . . 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 9726	. . . . . . . . . . . . . . 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 6092	. . . . . . . . . . 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 13146	. . . . . . . . . 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 16211	. . . . . . . . . . . . . . 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 16211	. . . . . . . . . . . . . . 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 6103	. . . . . . . . . . . . 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 6101	. . . . . . . . . . 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 9315	. . . . . . . . . . . . . . . 16 |- ( n e. NN -> n e. CC )
212	211	exp1d 11121	. . . . . . . . . . . . . . 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 4217	. . . . . . . . . . . . 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 9584	. . . . . . . . . . . . . . 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 13146	. . . . . . . . . . 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 4162	. . . . . . . . 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 13132	. . . . . . . . 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 9320	. . . . . . . . . 10 |- ( ph -> ( exp ` ( theta ` K ) ) e. RR )
229	113	nnred 9320	. . . . . . . . . 10 |- ( ph -> ( exp ` ( theta ` M ) ) e. RR )
230	117	nngt0d 9351	. . . . . . . . . 10 |- ( ph -> 0 < ( exp ` ( theta ` K ) ) )
231	113	nngt0d 9351	. . . . . . . . . 10 |- ( ph -> 0 < ( exp ` ( theta ` M ) ) )
232	228, 229, 230, 231	divgt0d 9268	. . . . . . . . 9 |- ( ph -> 0 < ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) )
233		elnnz 9659	. . . . . . . . 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 12630	. . . . . . . 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 9343	. . . . . . . 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 9384	. . . . . . . . . 10 |- 4 e. RR
241	240	a1i 9	. . . . . . . . 9 |- ( ph -> 4 e. RR )
242		6re 9388	. . . . . . . . . 10 |- 6 e. RR
243	242	a1i 9	. . . . . . . . 9 |- ( ph -> 6 e. RR )
244		4lt6 9490	. . . . . . . . . 10 |- 4 < 6
245	244	a1i 9	. . . . . . . . 9 |- ( ph -> 4 < 6 )
246		cht3 16206	. . . . . . . . . . . 12 |- ( theta ` 3 ) = ( log ` 6 )
247	246	fveq2i 5698	. . . . . . . . . . 11 |- ( exp ` ( theta ` 3 ) ) = ( exp ` ( log ` 6 ) )
248		6pos 9408	. . . . . . . . . . . . 13 |- 0 < 6
249	242, 248	elrpii 10068	. . . . . . . . . . . 12 |- 6 e. RR+
250		reeflog 16024	. . . . . . . . . . . 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 9678	. . . . . . . . . . . . . 14 |- 3 e. ZZ
254		zq 10036	. . . . . . . . . . . . . 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 9944	. . . . . . . . . . . . 13 |- ( M e. ( ZZ>= ` 3 ) -> 3 <_ M )
258	67, 257	syl 14	. . . . . . . . . . . 12 |- ( ph -> 3 <_ M )
259		chtqwordi 16192	. . . . . . . . . . . 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 16173	. . . . . . . . . . . . 13 |- ( 3 e. QQ -> ( theta ` 3 ) e. RR )
262	255, 261	ax-mp 5	. . . . . . . . . . . 12 |- ( theta ` 3 ) e. RR
263		chtqcl 16173	. . . . . . . . . . . . 13 |- ( M e. QQ -> ( theta ` M ) e. RR )
264	105, 263	syl 14	. . . . . . . . . . . 12 |- ( ph -> ( theta ` M ) e. RR )
265		efle 15936	. . . . . . . . . . . 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 4166	. . . . . . . . 9 |- ( ph -> 6 <_ ( exp ` ( theta ` M ) ) )
269	241, 243, 229, 245, 268	ltletrd 8753	. . . . . . . 8 |- ( ph -> 4 < ( exp ` ( theta ` M ) ) )
270		4pos 9404	. . . . . . . . . 10 |- 0 < 4
271	270	a1i 9	. . . . . . . . 9 |- ( ph -> 0 < 4 )
272		ltdiv2 9220	. . . . . . . . 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 9381	. . . . . . . . . . . . . 14 |- 3 e. RR
277	276	a1i 9	. . . . . . . . . . . . 13 |- ( ph -> 3 e. RR )
278	77	zred 9773	. . . . . . . . . . . . 13 |- ( ph -> K e. RR )
279		2lt3 9480	. . . . . . . . . . . . . 14 |- 2 < 3
280	279	a1i 9	. . . . . . . . . . . . 13 |- ( ph -> 2 < 3 )
281	69	nnred 9320	. . . . . . . . . . . . . 14 |- ( ph -> M e. RR )
282	277, 281, 278, 258, 109	letrd 8452	. . . . . . . . . . . . 13 |- ( ph -> 3 <_ K )
283	275, 277, 278, 280, 282	ltletrd 8753	. . . . . . . . . . . 12 |- ( ph -> 2 < K )
284		chtqub 16225	. . . . . . . . . . . 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 16173	. . . . . . . . . . . . 13 |- ( K e. QQ -> ( theta ` K ) e. RR )
287	107, 286	syl 14	. . . . . . . . . . . 12 |- ( ph -> ( theta ` K ) e. RR )
288		relogcl 16023	. . . . . . . . . . . . . 14 |- ( 2 e. RR+ -> ( log ` 2 ) e. RR )
289	31, 288	ax-mp 5	. . . . . . . . . . . . 13 |- ( log ` 2 ) e. RR
290		zsubcl 9690	. . . . . . . . . . . . . . 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 9773	. . . . . . . . . . . . 13 |- ( ph -> ( ( 2 x. K ) - 3 ) e. RR )
293		remulcl 8308	. . . . . . . . . . . . 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 15935	. . . . . . . . . . . 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 16033	. . . . . . . . . . . 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 9774	. . . . . . . . . . . . 13 |- ( ph -> ( ( 2 x. K ) - 3 ) e. CC )
301	289	recni 8339	. . . . . . . . . . . . 13 |- ( log ` 2 ) e. CC
302		mulcom 8309	. . . . . . . . . . . . 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 5699	. . . . . . . . . . 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 4158	. . . . . . . . 9 |- ( ph -> ( exp ` ( theta ` K ) ) < ( 2 ^ ( ( 2 x. K ) - 3 ) ) )
307		3p2e5 9449	. . . . . . . . . . . . . . . 16 |- ( 3 + 2 ) = 5
308	307	oveq1i 6095	. . . . . . . . . . . . . . 15 |- ( ( 3 + 2 ) - 2 ) = ( 5 - 2 )
309		3cn 9382	. . . . . . . . . . . . . . . 16 |- 3 e. CC
310		2cn 9378	. . . . . . . . . . . . . . . 16 |- 2 e. CC
311	309, 310	pncan3oi 8544	. . . . . . . . . . . . . . 15 |- ( ( 3 + 2 ) - 2 ) = 3
312	308, 311	eqtr3i 2261	. . . . . . . . . . . . . 14 |- ( 5 - 2 ) = 3
313	312	oveq2i 6096	. . . . . . . . . . . . 13 |- ( ( 2 x. K ) - ( 5 - 2 ) ) = ( ( 2 x. K ) - 3 )
314	79	zcnd 9774	. . . . . . . . . . . . . 14 |- ( ph -> ( 2 x. K ) e. CC )
315		5cn 9387	. . . . . . . . . . . . . . 15 |- 5 e. CC
316		subsub 8558	. . . . . . . . . . . . . . 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 6101	. . . . . . . . . . 11 |- ( ph -> ( 2 ^c ( ( 2 x. K ) - 3 ) ) = ( 2 ^c ( ( ( 2 x. K ) - 5 ) + 2 ) ) )
321		cxpexpnn 16061	. . . . . . . . . . . 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 9774	. . . . . . . . . . . 12 |- ( ph -> ( ( 2 x. K ) - 5 ) e. CC )
324		rpcxpadd 16070	. . . . . . . . . . . . 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 16061	. . . . . . . . . . . . 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 11087	. . . . . . . . . . . 12 |- ( 2 ^ 2 ) = 4
331	329, 330	eqtri 2259	. . . . . . . . . . 11 |- ( 2 ^c 2 ) = 4
332	331	oveq2i 6096	. . . . . . . . . 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 4156	. . . . . . . 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 9211	. . . . . . . . 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 8454	. . . . . 6 |- ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) )
341	103, 122, 86, 237, 340	lelttrd 8453	. . . . 5 |- ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) )
342	98	nnred 9320	. . . . . 6 |- ( ph -> ( seq 1 ( x. , F ) ` K ) e. RR )
343		nnre 9314	. . . . . . . 8 |- ( ( seq 1 ( x. , F ) ` M ) e. NN -> ( seq 1 ( x. , F ) ` M ) e. RR )
344		nngt0 9332	. . . . . . . 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 9209	. . . . . 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 4154	. . 3 |- ( ph -> ( ( 2 x. N ) _C N ) < ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) )
351	30, 86	remulcld 8357	. . . 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 16244	. . . . 5 |- ( ph -> ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) )
353	71, 30, 85	lemul1d 10152	. . . . 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 9773	. . . . . . 7 |- ( ph -> ( 2 x. K ) e. RR )
356	37	a1i 9	. . . . . . 7 |- ( ph -> 5 e. RR )
357		flqle 10726	. . . . . . . . . . 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 4165	. . . . . . . . 9 |- ( ph -> K <_ ( ( 2 x. N ) / 3 ) )
360		nndivre 9343	. . . . . . . . . . 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 9398	. . . . . . . . . . . 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 9190	. . . . . . . . . 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 9321	. . . . . . . . . 10 |- ( ph -> ( 2 x. N ) e. CC )
369		3ap0 9403	. . . . . . . . . . . 12 |- 3 # 0
370	309, 369	pm3.2i 272	. . . . . . . . . . 11 |- ( 3 e. CC /\ 3 # 0 )
371		divassap 9023	. . . . . . . . . . 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 9321	. . . . . . . . . . . 12 |- ( ph -> N e. CC )
375		mulass 8311	. . . . . . . . . . . 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 9462	. . . . . . . . . . . 12 |- ( 2 x. 2 ) = 4
378	377	oveq1i 6095	. . . . . . . . . . 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 6100	. . . . . . . . 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 4156	. . . . . . 7 |- ( ph -> ( 2 x. K ) <_ ( ( 4 x. N ) / 3 ) )
383	355, 36, 356, 382	lesub1dd 8891	. . . . . 6 |- ( ph -> ( ( 2 x. K ) - 5 ) <_ ( ( ( 4 x. N ) / 3 ) - 5 ) )
384		1lt2 9479	. . . . . . . 8 |- 1 < 2
385	384	a1i 9	. . . . . . 7 |- ( ph -> 1 < 2 )
386	275, 385, 83, 39	cxpled 16094	. . . . . 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 10153	. . . . 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 8452	. . 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 8753	. 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 8454	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 4130   |-> cmpt 4192   -->wf 5373   ` cfv 5377  (class class class)co 6085   CCcc 8178   RRcr 8179   0cc0 8180   1c1 8181   + caddc 8183   x. cmul 8185   < clt 8361   <_ cle 8362   - cmin 8499   # cap 8912   / cdiv 9005   NNcn 9307   2c2 9358   3c3 9359   4c4 9360   5c5 9361   6c6 9362   NN0cn0 9568   ZZcz 9649   ZZ>=cuz 9931   QQcq 10029   RR+crp 10065   ...cfz 10422   |_cfl 10714   seqcseq 10899   ^cexp 10990   _C cbc 11201   sqrcsqrt 11778   expce 12428   || cdvds 12573   Primecprime 12904   pCnt cpc 13086   logclog 16017   ^c ccxp 16018   thetaccht 16162

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

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

This theorem is used by:  bposlem9  16248