bposlem6

Description: Lemma for bpos . 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)

	Ref	Expression
Hypotheses	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 = ( \|_ ` ( sqrt ` ( 2 x. N ) ) )
Assertion	bposlem6	\|- ( ph -> ( ( 4 ^ N ) / N ) < ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		bpos.1	\|- ( ph -> N e. ( ZZ>= ` 5 ) )
2		bpos.2	\|- ( ph -> -. E. p e. Prime ( N < p /\ p <_ ( 2 x. N ) ) )
3		bpos.3	\|- F = ( n e. NN \|-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )
4		bpos.4	\|- K = ( \|_ ` ( ( 2 x. N ) / 3 ) )
5		bpos.5	\|- M = ( \|_ ` ( sqrt ` ( 2 x. N ) ) )
6		4nn	\|- 4 e. NN
7		5nn	\|- 5 e. NN
8		eluznn	\|- ( ( 5 e. NN /\ N e. ( ZZ>= ` 5 ) ) -> N e. NN )
9	7 1 8	sylancr	\|- ( ph -> N e. NN )
10	9	nnnn0d	\|- ( ph -> N e. NN0 )
11		nnexpcl	\|- ( ( 4 e. NN /\ N e. NN0 ) -> ( 4 ^ N ) e. NN )
12	6 10 11	sylancr	\|- ( ph -> ( 4 ^ N ) e. NN )
13	12	nnred	\|- ( ph -> ( 4 ^ N ) e. RR )
14	13 9	nndivred	\|- ( ph -> ( ( 4 ^ N ) / N ) e. RR )
15		fzctr	\|- ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) )
16	10 15	syl	\|- ( ph -> N e. ( 0 ... ( 2 x. N ) ) )
17		bccl2	\|- ( N e. ( 0 ... ( 2 x. N ) ) -> ( ( 2 x. N ) _C N ) e. NN )
18	16 17	syl	\|- ( ph -> ( ( 2 x. N ) _C N ) e. NN )
19	18	nnred	\|- ( ph -> ( ( 2 x. N ) _C N ) e. RR )
20		2nn	\|- 2 e. NN
21		nnmulcl	\|- ( ( 2 e. NN /\ N e. NN ) -> ( 2 x. N ) e. NN )
22	20 9 21	sylancr	\|- ( ph -> ( 2 x. N ) e. NN )
23	22	nnrpd	\|- ( ph -> ( 2 x. N ) e. RR+ )
24	22	nnred	\|- ( ph -> ( 2 x. N ) e. RR )
25	23	rpge0d	\|- ( ph -> 0 <_ ( 2 x. N ) )
26	24 25	resqrtcld	\|- ( ph -> ( sqrt ` ( 2 x. N ) ) e. RR )
27		3nn	\|- 3 e. NN
28		nndivre	\|- ( ( ( sqrt ` ( 2 x. N ) ) e. RR /\ 3 e. NN ) -> ( ( sqrt ` ( 2 x. N ) ) / 3 ) e. RR )
29	26 27 28	sylancl	\|- ( ph -> ( ( sqrt ` ( 2 x. N ) ) / 3 ) e. RR )
30		2re	\|- 2 e. RR
31		readdcl	\|- ( ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) e. RR /\ 2 e. RR ) -> ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) e. RR )
32	29 30 31	sylancl	\|- ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) e. RR )
33	23 32	rpcxpcld	\|- ( ph -> ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) e. RR+ )
34	33	rpred	\|- ( ph -> ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) e. RR )
35		2rp	\|- 2 e. RR+
36		nnmulcl	\|- ( ( 4 e. NN /\ N e. NN ) -> ( 4 x. N ) e. NN )
37	6 9 36	sylancr	\|- ( ph -> ( 4 x. N ) e. NN )
38	37	nnred	\|- ( ph -> ( 4 x. N ) e. RR )
39		nndivre	\|- ( ( ( 4 x. N ) e. RR /\ 3 e. NN ) -> ( ( 4 x. N ) / 3 ) e. RR )
40	38 27 39	sylancl	\|- ( ph -> ( ( 4 x. N ) / 3 ) e. RR )
41		5re	\|- 5 e. RR
42		resubcl	\|- ( ( ( ( 4 x. N ) / 3 ) e. RR /\ 5 e. RR ) -> ( ( ( 4 x. N ) / 3 ) - 5 ) e. RR )
43	40 41 42	sylancl	\|- ( ph -> ( ( ( 4 x. N ) / 3 ) - 5 ) e. RR )
44		rpcxpcl	\|- ( ( 2 e. RR+ /\ ( ( ( 4 x. N ) / 3 ) - 5 ) e. RR ) -> ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) e. RR+ )
45	35 43 44	sylancr	\|- ( ph -> ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) e. RR+ )
46	45	rpred	\|- ( ph -> ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) e. RR )
47	34 46	remulcld	\|- ( ph -> ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) e. RR )
48		df-5	\|- 5 = ( 4 + 1 )
49		4z	\|- 4 e. ZZ
50		uzid	\|- ( 4 e. ZZ -> 4 e. ( ZZ>= ` 4 ) )
51		peano2uz	\|- ( 4 e. ( ZZ>= ` 4 ) -> ( 4 + 1 ) e. ( ZZ>= ` 4 ) )
52	49 50 51	mp2b	\|- ( 4 + 1 ) e. ( ZZ>= ` 4 )
53	48 52	eqeltri	\|- 5 e. ( ZZ>= ` 4 )
54		eqid	\|- ( ZZ>= ` 4 ) = ( ZZ>= ` 4 )
55	54	uztrn2	\|- ( ( 5 e. ( ZZ>= ` 4 ) /\ N e. ( ZZ>= ` 5 ) ) -> N e. ( ZZ>= ` 4 ) )
56	53 1 55	sylancr	\|- ( ph -> N e. ( ZZ>= ` 4 ) )
57		bclbnd	\|- ( N e. ( ZZ>= ` 4 ) -> ( ( 4 ^ N ) / N ) < ( ( 2 x. N ) _C N ) )
58	56 57	syl	\|- ( ph -> ( ( 4 ^ N ) / N ) < ( ( 2 x. N ) _C N ) )
59		id	\|- ( n e. Prime -> n e. Prime )
60		pccl	\|- ( ( n e. Prime /\ ( ( 2 x. N ) _C N ) e. NN ) -> ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
61	59 18 60	syl2anr	\|- ( ( ph /\ n e. Prime ) -> ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
62	61	ralrimiva	\|- ( ph -> A. n e. Prime ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
63	3 62	pcmptcl	\|- ( ph -> ( F : NN --> NN /\ seq 1 ( x. , F ) : NN --> NN ) )
64	63	simprd	\|- ( ph -> seq 1 ( x. , F ) : NN --> NN )
65	1 2 3 4 5	bposlem4	\|- ( ph -> M e. ( 3 ... K ) )
66		elfzuz	\|- ( M e. ( 3 ... K ) -> M e. ( ZZ>= ` 3 ) )
67	65 66	syl	\|- ( ph -> M e. ( ZZ>= ` 3 ) )
68		eluznn	\|- ( ( 3 e. NN /\ M e. ( ZZ>= ` 3 ) ) -> M e. NN )
69	27 67 68	sylancr	\|- ( ph -> M e. NN )
70	64 69	ffvelcdmd	\|- ( ph -> ( seq 1 ( x. , F ) ` M ) e. NN )
71	70	nnred	\|- ( ph -> ( seq 1 ( x. , F ) ` M ) e. RR )
72		2z	\|- 2 e. ZZ
73		nndivre	\|- ( ( ( 2 x. N ) e. RR /\ 3 e. NN ) -> ( ( 2 x. N ) / 3 ) e. RR )
74	24 27 73	sylancl	\|- ( ph -> ( ( 2 x. N ) / 3 ) e. RR )
75	74	flcld	\|- ( ph -> ( \|_ ` ( ( 2 x. N ) / 3 ) ) e. ZZ )
76	4 75	eqeltrid	\|- ( ph -> K e. ZZ )
77		zmulcl	\|- ( ( 2 e. ZZ /\ K e. ZZ ) -> ( 2 x. K ) e. ZZ )
78	72 76 77	sylancr	\|- ( ph -> ( 2 x. K ) e. ZZ )
79	7	nnzi	\|- 5 e. ZZ
80		zsubcl	\|- ( ( ( 2 x. K ) e. ZZ /\ 5 e. ZZ ) -> ( ( 2 x. K ) - 5 ) e. ZZ )
81	78 79 80	sylancl	\|- ( ph -> ( ( 2 x. K ) - 5 ) e. ZZ )
82	81	zred	\|- ( ph -> ( ( 2 x. K ) - 5 ) e. RR )
83		rpcxpcl	\|- ( ( 2 e. RR+ /\ ( ( 2 x. K ) - 5 ) e. RR ) -> ( 2 ^c ( ( 2 x. K ) - 5 ) ) e. RR+ )
84	35 82 83	sylancr	\|- ( ph -> ( 2 ^c ( ( 2 x. K ) - 5 ) ) e. RR+ )
85	84	rpred	\|- ( ph -> ( 2 ^c ( ( 2 x. K ) - 5 ) ) e. RR )
86	71 85	remulcld	\|- ( ph -> ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) e. RR )
87	1 2 3 4	bposlem3	\|- ( ph -> ( seq 1 ( x. , F ) ` K ) = ( ( 2 x. N ) _C N ) )
88		elfzuz3	\|- ( M e. ( 3 ... K ) -> K e. ( ZZ>= ` M ) )
89	65 88	syl	\|- ( ph -> K e. ( ZZ>= ` M ) )
90	3 62 69 89	pcmptdvds	\|- ( ph -> ( seq 1 ( x. , F ) ` M ) \|\| ( seq 1 ( x. , F ) ` K ) )
91	70	nnzd	\|- ( ph -> ( seq 1 ( x. , F ) ` M ) e. ZZ )
92	70	nnne0d	\|- ( ph -> ( seq 1 ( x. , F ) ` M ) =/= 0 )
93		uztrn	\|- ( ( K e. ( ZZ>= ` M ) /\ M e. ( ZZ>= ` 3 ) ) -> K e. ( ZZ>= ` 3 ) )
94	89 67 93	syl2anc	\|- ( ph -> K e. ( ZZ>= ` 3 ) )
95		eluznn	\|- ( ( 3 e. NN /\ K e. ( ZZ>= ` 3 ) ) -> K e. NN )
96	27 94 95	sylancr	\|- ( ph -> K e. NN )
97	64 96	ffvelcdmd	\|- ( ph -> ( seq 1 ( x. , F ) ` K ) e. NN )
98	97	nnzd	\|- ( ph -> ( seq 1 ( x. , F ) ` K ) e. ZZ )
99		dvdsval2	\|- ( ( ( 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 ) )
100	91 92 98 99	syl3anc	\|- ( ph -> ( ( seq 1 ( x. , F ) ` M ) \|\| ( seq 1 ( x. , F ) ` K ) <-> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) e. ZZ ) )
101	90 100	mpbid	\|- ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) e. ZZ )
102	101	zred	\|- ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) e. RR )
103	69	nnred	\|- ( ph -> M e. RR )
104	76	zred	\|- ( ph -> K e. RR )
105		eluzle	\|- ( K e. ( ZZ>= ` M ) -> M <_ K )
106	89 105	syl	\|- ( ph -> M <_ K )
107		efchtdvds	\|- ( ( M e. RR /\ K e. RR /\ M <_ K ) -> ( exp ` ( theta ` M ) ) \|\| ( exp ` ( theta ` K ) ) )
108	103 104 106 107	syl3anc	\|- ( ph -> ( exp ` ( theta ` M ) ) \|\| ( exp ` ( theta ` K ) ) )
109		efchtcl	\|- ( M e. RR -> ( exp ` ( theta ` M ) ) e. NN )
110	103 109	syl	\|- ( ph -> ( exp ` ( theta ` M ) ) e. NN )
111	110	nnzd	\|- ( ph -> ( exp ` ( theta ` M ) ) e. ZZ )
112	110	nnne0d	\|- ( ph -> ( exp ` ( theta ` M ) ) =/= 0 )
113		efchtcl	\|- ( K e. RR -> ( exp ` ( theta ` K ) ) e. NN )
114	104 113	syl	\|- ( ph -> ( exp ` ( theta ` K ) ) e. NN )
115	114	nnzd	\|- ( ph -> ( exp ` ( theta ` K ) ) e. ZZ )
116		dvdsval2	\|- ( ( ( 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 ) )
117	111 112 115 116	syl3anc	\|- ( ph -> ( ( exp ` ( theta ` M ) ) \|\| ( exp ` ( theta ` K ) ) <-> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. ZZ ) )
118	108 117	mpbid	\|- ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. ZZ )
119	118	zred	\|- ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. RR )
120		prmz	\|- ( p e. Prime -> p e. ZZ )
121		fllt	\|- ( ( ( sqrt ` ( 2 x. N ) ) e. RR /\ p e. ZZ ) -> ( ( sqrt ` ( 2 x. N ) ) < p <-> ( \|_ ` ( sqrt ` ( 2 x. N ) ) ) < p ) )
122	26 120 121	syl2an	\|- ( ( ph /\ p e. Prime ) -> ( ( sqrt ` ( 2 x. N ) ) < p <-> ( \|_ ` ( sqrt ` ( 2 x. N ) ) ) < p ) )
123	5	breq1i	\|- ( M < p <-> ( \|_ ` ( sqrt ` ( 2 x. N ) ) ) < p )
124	122 123	bitr4di	\|- ( ( ph /\ p e. Prime ) -> ( ( sqrt ` ( 2 x. N ) ) < p <-> M < p ) )
125	120	zred	\|- ( p e. Prime -> p e. RR )
126		ltnle	\|- ( ( M e. RR /\ p e. RR ) -> ( M < p <-> -. p <_ M ) )
127	103 125 126	syl2an	\|- ( ( ph /\ p e. Prime ) -> ( M < p <-> -. p <_ M ) )
128	124 127	bitrd	\|- ( ( ph /\ p e. Prime ) -> ( ( sqrt ` ( 2 x. N ) ) < p <-> -. p <_ M ) )
129		bposlem1	\|- ( ( N e. NN /\ p e. Prime ) -> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )
130	9 129	sylan	\|- ( ( ph /\ p e. Prime ) -> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )
131	125	adantl	\|- ( ( ph /\ p e. Prime ) -> p e. RR )
132		id	\|- ( p e. Prime -> p e. Prime )
133		pccl	\|- ( ( p e. Prime /\ ( ( 2 x. N ) _C N ) e. NN ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
134	132 18 133	syl2anr	\|- ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
135	131 134	reexpcld	\|- ( ( ph /\ p e. Prime ) -> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) e. RR )
136	24	adantr	\|- ( ( ph /\ p e. Prime ) -> ( 2 x. N ) e. RR )
137	131	resqcld	\|- ( ( ph /\ p e. Prime ) -> ( p ^ 2 ) e. RR )
138		lelttr	\|- ( ( ( 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 ) ) )
139	135 136 137 138	syl3anc	\|- ( ( 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 ) ) )
140	130 139	mpand	\|- ( ( ph /\ p e. Prime ) -> ( ( 2 x. N ) < ( p ^ 2 ) -> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) < ( p ^ 2 ) ) )
141		resqrtth	\|- ( ( ( 2 x. N ) e. RR /\ 0 <_ ( 2 x. N ) ) -> ( ( sqrt ` ( 2 x. N ) ) ^ 2 ) = ( 2 x. N ) )
142	24 25 141	syl2anc	\|- ( ph -> ( ( sqrt ` ( 2 x. N ) ) ^ 2 ) = ( 2 x. N ) )
143	142	breq1d	\|- ( ph -> ( ( ( sqrt ` ( 2 x. N ) ) ^ 2 ) < ( p ^ 2 ) <-> ( 2 x. N ) < ( p ^ 2 ) ) )
144	143	adantr	\|- ( ( ph /\ p e. Prime ) -> ( ( ( sqrt ` ( 2 x. N ) ) ^ 2 ) < ( p ^ 2 ) <-> ( 2 x. N ) < ( p ^ 2 ) ) )
145	134	nn0zd	\|- ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) e. ZZ )
146	72	a1i	\|- ( ( ph /\ p e. Prime ) -> 2 e. ZZ )
147		prmgt1	\|- ( p e. Prime -> 1 < p )
148	147	adantl	\|- ( ( ph /\ p e. Prime ) -> 1 < p )
149	131 145 146 148	ltexp2d	\|- ( ( ph /\ p e. Prime ) -> ( ( p pCnt ( ( 2 x. N ) _C N ) ) < 2 <-> ( p ^ ( p pCnt ( ( 2 x. N ) _C N ) ) ) < ( p ^ 2 ) ) )
150	140 144 149	3imtr4d	\|- ( ( ph /\ p e. Prime ) -> ( ( ( sqrt ` ( 2 x. N ) ) ^ 2 ) < ( p ^ 2 ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) < 2 ) )
151		df-2	\|- 2 = ( 1 + 1 )
152	151	breq2i	\|- ( ( p pCnt ( ( 2 x. N ) _C N ) ) < 2 <-> ( p pCnt ( ( 2 x. N ) _C N ) ) < ( 1 + 1 ) )
153	150 152	imbitrdi	\|- ( ( ph /\ p e. Prime ) -> ( ( ( sqrt ` ( 2 x. N ) ) ^ 2 ) < ( p ^ 2 ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) < ( 1 + 1 ) ) )
154	26	adantr	\|- ( ( ph /\ p e. Prime ) -> ( sqrt ` ( 2 x. N ) ) e. RR )
155	24 25	sqrtge0d	\|- ( ph -> 0 <_ ( sqrt ` ( 2 x. N ) ) )
156	155	adantr	\|- ( ( ph /\ p e. Prime ) -> 0 <_ ( sqrt ` ( 2 x. N ) ) )
157		prmnn	\|- ( p e. Prime -> p e. NN )
158	157	nnrpd	\|- ( p e. Prime -> p e. RR+ )
159	158	rpge0d	\|- ( p e. Prime -> 0 <_ p )
160	159	adantl	\|- ( ( ph /\ p e. Prime ) -> 0 <_ p )
161	154 131 156 160	lt2sqd	\|- ( ( ph /\ p e. Prime ) -> ( ( sqrt ` ( 2 x. N ) ) < p <-> ( ( sqrt ` ( 2 x. N ) ) ^ 2 ) < ( p ^ 2 ) ) )
162		1z	\|- 1 e. ZZ
163		zleltp1	\|- ( ( ( 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 ) ) )
164	145 162 163	sylancl	\|- ( ( ph /\ p e. Prime ) -> ( ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 <-> ( p pCnt ( ( 2 x. N ) _C N ) ) < ( 1 + 1 ) ) )
165	153 161 164	3imtr4d	\|- ( ( ph /\ p e. Prime ) -> ( ( sqrt ` ( 2 x. N ) ) < p -> ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 ) )
166	128 165	sylbird	\|- ( ( ph /\ p e. Prime ) -> ( -. p <_ M -> ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 ) )
167	166	imp	\|- ( ( ( ph /\ p e. Prime ) /\ -. p <_ M ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 )
168	167	adantrl	\|- ( ( ( ph /\ p e. Prime ) /\ ( p <_ K /\ -. p <_ M ) ) -> ( p pCnt ( ( 2 x. N ) _C N ) ) <_ 1 )
169		iftrue	\|- ( ( p <_ K /\ -. p <_ M ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) = ( p pCnt ( ( 2 x. N ) _C N ) ) )
170	169	adantl	\|- ( ( ( 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 ) ) )
171		iftrue	\|- ( ( p <_ K /\ -. p <_ M ) -> if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) = 1 )
172	171	adantl	\|- ( ( ( ph /\ p e. Prime ) /\ ( p <_ K /\ -. p <_ M ) ) -> if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) = 1 )
173	168 170 172	3brtr4d	\|- ( ( ( 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 ) )
174		0le0	\|- 0 <_ 0
175		iffalse	\|- ( -. ( p <_ K /\ -. p <_ M ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) = 0 )
176		iffalse	\|- ( -. ( p <_ K /\ -. p <_ M ) -> if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) = 0 )
177	175 176	breq12d	\|- ( -. ( 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 ) )
178	174 177	mpbiri	\|- ( -. ( p <_ K /\ -. p <_ M ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) <_ if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) )
179	178	adantl	\|- ( ( ( 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 ) )
180	173 179	pm2.61dan	\|- ( ( ph /\ p e. Prime ) -> if ( ( p <_ K /\ -. p <_ M ) , ( p pCnt ( ( 2 x. N ) _C N ) ) , 0 ) <_ if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) )
181	62	adantr	\|- ( ( ph /\ p e. Prime ) -> A. n e. Prime ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
182	69	adantr	\|- ( ( ph /\ p e. Prime ) -> M e. NN )
183		simpr	\|- ( ( ph /\ p e. Prime ) -> p e. Prime )
184		oveq1	\|- ( n = p -> ( n pCnt ( ( 2 x. N ) _C N ) ) = ( p pCnt ( ( 2 x. N ) _C N ) ) )
185	89	adantr	\|- ( ( ph /\ p e. Prime ) -> K e. ( ZZ>= ` M ) )
186	3 181 182 183 184 185	pcmpt2	\|- ( ( 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 ) )
187		eqid	\|- ( n e. NN \|-> if ( n e. Prime , n , 1 ) ) = ( n e. NN \|-> if ( n e. Prime , n , 1 ) )
188	187	prmorcht	\|- ( K e. NN -> ( exp ` ( theta ` K ) ) = ( seq 1 ( x. , ( n e. NN \|-> if ( n e. Prime , n , 1 ) ) ) ` K ) )
189	96 188	syl	\|- ( ph -> ( exp ` ( theta ` K ) ) = ( seq 1 ( x. , ( n e. NN \|-> if ( n e. Prime , n , 1 ) ) ) ` K ) )
190	187	prmorcht	\|- ( M e. NN -> ( exp ` ( theta ` M ) ) = ( seq 1 ( x. , ( n e. NN \|-> if ( n e. Prime , n , 1 ) ) ) ` M ) )
191	69 190	syl	\|- ( ph -> ( exp ` ( theta ` M ) ) = ( seq 1 ( x. , ( n e. NN \|-> if ( n e. Prime , n , 1 ) ) ) ` M ) )
192	189 191	oveq12d	\|- ( 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 ) ) )
193	192	adantr	\|- ( ( 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 ) ) )
194	193	oveq2d	\|- ( ( 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 ) ) ) )
195		nncn	\|- ( n e. NN -> n e. CC )
196	195	exp1d	\|- ( n e. NN -> ( n ^ 1 ) = n )
197	196	ifeq1d	\|- ( n e. NN -> if ( n e. Prime , ( n ^ 1 ) , 1 ) = if ( n e. Prime , n , 1 ) )
198	197	mpteq2ia	\|- ( n e. NN \|-> if ( n e. Prime , ( n ^ 1 ) , 1 ) ) = ( n e. NN \|-> if ( n e. Prime , n , 1 ) )
199	198	eqcomi	\|- ( n e. NN \|-> if ( n e. Prime , n , 1 ) ) = ( n e. NN \|-> if ( n e. Prime , ( n ^ 1 ) , 1 ) )
200		1nn0	\|- 1 e. NN0
201	200	a1i	\|- ( ( ph /\ n e. Prime ) -> 1 e. NN0 )
202	201	ralrimiva	\|- ( ph -> A. n e. Prime 1 e. NN0 )
203	202	adantr	\|- ( ( ph /\ p e. Prime ) -> A. n e. Prime 1 e. NN0 )
204		eqidd	\|- ( n = p -> 1 = 1 )
205	199 203 182 183 204 185	pcmpt2	\|- ( ( 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 ) )
206	194 205	eqtrd	\|- ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) = if ( ( p <_ K /\ -. p <_ M ) , 1 , 0 ) )
207	180 186 206	3brtr4d	\|- ( ( ph /\ p e. Prime ) -> ( p pCnt ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) ) <_ ( p pCnt ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) )
208	207	ralrimiva	\|- ( 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 ) ) ) ) )
209		pc2dvds	\|- ( ( ( ( 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 ) ) ) ) ) )
210	101 118 209	syl2anc	\|- ( 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 ) ) ) ) ) )
211	208 210	mpbird	\|- ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) \|\| ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) )
212	114	nnred	\|- ( ph -> ( exp ` ( theta ` K ) ) e. RR )
213	110	nnred	\|- ( ph -> ( exp ` ( theta ` M ) ) e. RR )
214	114	nngt0d	\|- ( ph -> 0 < ( exp ` ( theta ` K ) ) )
215	110	nngt0d	\|- ( ph -> 0 < ( exp ` ( theta ` M ) ) )
216	212 213 214 215	divgt0d	\|- ( ph -> 0 < ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) )
217		elnnz	\|- ( ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. NN <-> ( ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. ZZ /\ 0 < ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) ) )
218	118 216 217	sylanbrc	\|- ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) e. NN )
219		dvdsle	\|- ( ( ( ( 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 ) ) ) ) )
220	101 218 219	syl2anc	\|- ( 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 ) ) ) ) )
221	211 220	mpd	\|- ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) <_ ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) )
222		nndivre	\|- ( ( ( exp ` ( theta ` K ) ) e. RR /\ 4 e. NN ) -> ( ( exp ` ( theta ` K ) ) / 4 ) e. RR )
223	212 6 222	sylancl	\|- ( ph -> ( ( exp ` ( theta ` K ) ) / 4 ) e. RR )
224		4re	\|- 4 e. RR
225	224	a1i	\|- ( ph -> 4 e. RR )
226		6re	\|- 6 e. RR
227	226	a1i	\|- ( ph -> 6 e. RR )
228		4lt6	\|- 4 < 6
229	228	a1i	\|- ( ph -> 4 < 6 )
230		cht3	\|- ( theta ` 3 ) = ( log ` 6 )
231	230	fveq2i	\|- ( exp ` ( theta ` 3 ) ) = ( exp ` ( log ` 6 ) )
232		6pos	\|- 0 < 6
233	226 232	elrpii	\|- 6 e. RR+
234		reeflog	\|- ( 6 e. RR+ -> ( exp ` ( log ` 6 ) ) = 6 )
235	233 234	ax-mp	\|- ( exp ` ( log ` 6 ) ) = 6
236	231 235	eqtri	\|- ( exp ` ( theta ` 3 ) ) = 6
237		3re	\|- 3 e. RR
238	237	a1i	\|- ( ph -> 3 e. RR )
239		eluzle	\|- ( M e. ( ZZ>= ` 3 ) -> 3 <_ M )
240	67 239	syl	\|- ( ph -> 3 <_ M )
241		chtwordi	\|- ( ( 3 e. RR /\ M e. RR /\ 3 <_ M ) -> ( theta ` 3 ) <_ ( theta ` M ) )
242	238 103 240 241	syl3anc	\|- ( ph -> ( theta ` 3 ) <_ ( theta ` M ) )
243		chtcl	\|- ( 3 e. RR -> ( theta ` 3 ) e. RR )
244	237 243	ax-mp	\|- ( theta ` 3 ) e. RR
245		chtcl	\|- ( M e. RR -> ( theta ` M ) e. RR )
246	103 245	syl	\|- ( ph -> ( theta ` M ) e. RR )
247		efle	\|- ( ( ( theta ` 3 ) e. RR /\ ( theta ` M ) e. RR ) -> ( ( theta ` 3 ) <_ ( theta ` M ) <-> ( exp ` ( theta ` 3 ) ) <_ ( exp ` ( theta ` M ) ) ) )
248	244 246 247	sylancr	\|- ( ph -> ( ( theta ` 3 ) <_ ( theta ` M ) <-> ( exp ` ( theta ` 3 ) ) <_ ( exp ` ( theta ` M ) ) ) )
249	242 248	mpbid	\|- ( ph -> ( exp ` ( theta ` 3 ) ) <_ ( exp ` ( theta ` M ) ) )
250	236 249	eqbrtrrid	\|- ( ph -> 6 <_ ( exp ` ( theta ` M ) ) )
251	225 227 213 229 250	ltletrd	\|- ( ph -> 4 < ( exp ` ( theta ` M ) ) )
252		4pos	\|- 0 < 4
253	252	a1i	\|- ( ph -> 0 < 4 )
254		ltdiv2	\|- ( ( ( 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 ) ) )
255	225 253 213 215 212 214 254	syl222anc	\|- ( ph -> ( 4 < ( exp ` ( theta ` M ) ) <-> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) < ( ( exp ` ( theta ` K ) ) / 4 ) ) )
256	251 255	mpbid	\|- ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) < ( ( exp ` ( theta ` K ) ) / 4 ) )
257	30	a1i	\|- ( ph -> 2 e. RR )
258		2lt3	\|- 2 < 3
259	258	a1i	\|- ( ph -> 2 < 3 )
260	238 103 104 240 106	letrd	\|- ( ph -> 3 <_ K )
261	257 238 104 259 260	ltletrd	\|- ( ph -> 2 < K )
262		chtub	\|- ( ( K e. RR /\ 2 < K ) -> ( theta ` K ) < ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) )
263	104 261 262	syl2anc	\|- ( ph -> ( theta ` K ) < ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) )
264		chtcl	\|- ( K e. RR -> ( theta ` K ) e. RR )
265	104 264	syl	\|- ( ph -> ( theta ` K ) e. RR )
266		relogcl	\|- ( 2 e. RR+ -> ( log ` 2 ) e. RR )
267	35 266	ax-mp	\|- ( log ` 2 ) e. RR
268		3z	\|- 3 e. ZZ
269		zsubcl	\|- ( ( ( 2 x. K ) e. ZZ /\ 3 e. ZZ ) -> ( ( 2 x. K ) - 3 ) e. ZZ )
270	78 268 269	sylancl	\|- ( ph -> ( ( 2 x. K ) - 3 ) e. ZZ )
271	270	zred	\|- ( ph -> ( ( 2 x. K ) - 3 ) e. RR )
272		remulcl	\|- ( ( ( log ` 2 ) e. RR /\ ( ( 2 x. K ) - 3 ) e. RR ) -> ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) e. RR )
273	267 271 272	sylancr	\|- ( ph -> ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) e. RR )
274		eflt	\|- ( ( ( 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 ) ) ) ) )
275	265 273 274	syl2anc	\|- ( ph -> ( ( theta ` K ) < ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) <-> ( exp ` ( theta ` K ) ) < ( exp ` ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) ) ) )
276	263 275	mpbid	\|- ( ph -> ( exp ` ( theta ` K ) ) < ( exp ` ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) ) )
277		reexplog	\|- ( ( 2 e. RR+ /\ ( ( 2 x. K ) - 3 ) e. ZZ ) -> ( 2 ^ ( ( 2 x. K ) - 3 ) ) = ( exp ` ( ( ( 2 x. K ) - 3 ) x. ( log ` 2 ) ) ) )
278	35 270 277	sylancr	\|- ( ph -> ( 2 ^ ( ( 2 x. K ) - 3 ) ) = ( exp ` ( ( ( 2 x. K ) - 3 ) x. ( log ` 2 ) ) ) )
279	270	zcnd	\|- ( ph -> ( ( 2 x. K ) - 3 ) e. CC )
280	267	recni	\|- ( log ` 2 ) e. CC
281		mulcom	\|- ( ( ( ( 2 x. K ) - 3 ) e. CC /\ ( log ` 2 ) e. CC ) -> ( ( ( 2 x. K ) - 3 ) x. ( log ` 2 ) ) = ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) )
282	279 280 281	sylancl	\|- ( ph -> ( ( ( 2 x. K ) - 3 ) x. ( log ` 2 ) ) = ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) )
283	282	fveq2d	\|- ( ph -> ( exp ` ( ( ( 2 x. K ) - 3 ) x. ( log ` 2 ) ) ) = ( exp ` ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) ) )
284	278 283	eqtrd	\|- ( ph -> ( 2 ^ ( ( 2 x. K ) - 3 ) ) = ( exp ` ( ( log ` 2 ) x. ( ( 2 x. K ) - 3 ) ) ) )
285	276 284	breqtrrd	\|- ( ph -> ( exp ` ( theta ` K ) ) < ( 2 ^ ( ( 2 x. K ) - 3 ) ) )
286		3p2e5	\|- ( 3 + 2 ) = 5
287	286	oveq1i	\|- ( ( 3 + 2 ) - 2 ) = ( 5 - 2 )
288		3cn	\|- 3 e. CC
289		2cn	\|- 2 e. CC
290	288 289	pncan3oi	\|- ( ( 3 + 2 ) - 2 ) = 3
291	287 290	eqtr3i	\|- ( 5 - 2 ) = 3
292	291	oveq2i	\|- ( ( 2 x. K ) - ( 5 - 2 ) ) = ( ( 2 x. K ) - 3 )
293	78	zcnd	\|- ( ph -> ( 2 x. K ) e. CC )
294		5cn	\|- 5 e. CC
295		subsub	\|- ( ( ( 2 x. K ) e. CC /\ 5 e. CC /\ 2 e. CC ) -> ( ( 2 x. K ) - ( 5 - 2 ) ) = ( ( ( 2 x. K ) - 5 ) + 2 ) )
296	294 289 295	mp3an23	\|- ( ( 2 x. K ) e. CC -> ( ( 2 x. K ) - ( 5 - 2 ) ) = ( ( ( 2 x. K ) - 5 ) + 2 ) )
297	293 296	syl	\|- ( ph -> ( ( 2 x. K ) - ( 5 - 2 ) ) = ( ( ( 2 x. K ) - 5 ) + 2 ) )
298	292 297	eqtr3id	\|- ( ph -> ( ( 2 x. K ) - 3 ) = ( ( ( 2 x. K ) - 5 ) + 2 ) )
299	298	oveq2d	\|- ( ph -> ( 2 ^c ( ( 2 x. K ) - 3 ) ) = ( 2 ^c ( ( ( 2 x. K ) - 5 ) + 2 ) ) )
300		2ne0	\|- 2 =/= 0
301		cxpexpz	\|- ( ( 2 e. CC /\ 2 =/= 0 /\ ( ( 2 x. K ) - 3 ) e. ZZ ) -> ( 2 ^c ( ( 2 x. K ) - 3 ) ) = ( 2 ^ ( ( 2 x. K ) - 3 ) ) )
302	289 300 270 301	mp3an12i	\|- ( ph -> ( 2 ^c ( ( 2 x. K ) - 3 ) ) = ( 2 ^ ( ( 2 x. K ) - 3 ) ) )
303	81	zcnd	\|- ( ph -> ( ( 2 x. K ) - 5 ) e. CC )
304		2cnne0	\|- ( 2 e. CC /\ 2 =/= 0 )
305		cxpadd	\|- ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( ( 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 ) ) )
306	304 289 305	mp3an13	\|- ( ( ( 2 x. K ) - 5 ) e. CC -> ( 2 ^c ( ( ( 2 x. K ) - 5 ) + 2 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. ( 2 ^c 2 ) ) )
307	303 306	syl	\|- ( ph -> ( 2 ^c ( ( ( 2 x. K ) - 5 ) + 2 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. ( 2 ^c 2 ) ) )
308	299 302 307	3eqtr3d	\|- ( ph -> ( 2 ^ ( ( 2 x. K ) - 3 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. ( 2 ^c 2 ) ) )
309		2nn0	\|- 2 e. NN0
310		cxpexp	\|- ( ( 2 e. CC /\ 2 e. NN0 ) -> ( 2 ^c 2 ) = ( 2 ^ 2 ) )
311	289 309 310	mp2an	\|- ( 2 ^c 2 ) = ( 2 ^ 2 )
312		sq2	\|- ( 2 ^ 2 ) = 4
313	311 312	eqtri	\|- ( 2 ^c 2 ) = 4
314	313	oveq2i	\|- ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. ( 2 ^c 2 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. 4 )
315	308 314	eqtrdi	\|- ( ph -> ( 2 ^ ( ( 2 x. K ) - 3 ) ) = ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. 4 ) )
316	285 315	breqtrd	\|- ( ph -> ( exp ` ( theta ` K ) ) < ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. 4 ) )
317	224 252	pm3.2i	\|- ( 4 e. RR /\ 0 < 4 )
318	317	a1i	\|- ( ph -> ( 4 e. RR /\ 0 < 4 ) )
319		ltdivmul2	\|- ( ( ( 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 ) ) )
320	212 85 318 319	syl3anc	\|- ( ph -> ( ( ( exp ` ( theta ` K ) ) / 4 ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) <-> ( exp ` ( theta ` K ) ) < ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) x. 4 ) ) )
321	316 320	mpbird	\|- ( ph -> ( ( exp ` ( theta ` K ) ) / 4 ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) )
322	119 223 85 256 321	lttrd	\|- ( ph -> ( ( exp ` ( theta ` K ) ) / ( exp ` ( theta ` M ) ) ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) )
323	102 119 85 221 322	lelttrd	\|- ( ph -> ( ( seq 1 ( x. , F ) ` K ) / ( seq 1 ( x. , F ) ` M ) ) < ( 2 ^c ( ( 2 x. K ) - 5 ) ) )
324	97	nnred	\|- ( ph -> ( seq 1 ( x. , F ) ` K ) e. RR )
325		nnre	\|- ( ( seq 1 ( x. , F ) ` M ) e. NN -> ( seq 1 ( x. , F ) ` M ) e. RR )
326		nngt0	\|- ( ( seq 1 ( x. , F ) ` M ) e. NN -> 0 < ( seq 1 ( x. , F ) ` M ) )
327	325 326	jca	\|- ( ( seq 1 ( x. , F ) ` M ) e. NN -> ( ( seq 1 ( x. , F ) ` M ) e. RR /\ 0 < ( seq 1 ( x. , F ) ` M ) ) )
328	70 327	syl	\|- ( ph -> ( ( seq 1 ( x. , F ) ` M ) e. RR /\ 0 < ( seq 1 ( x. , F ) ` M ) ) )
329		ltdivmul	\|- ( ( ( 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 ) ) ) ) )
330	324 85 328 329	syl3anc	\|- ( 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 ) ) ) ) )
331	323 330	mpbid	\|- ( ph -> ( seq 1 ( x. , F ) ` K ) < ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) )
332	87 331	eqbrtrrd	\|- ( ph -> ( ( 2 x. N ) _C N ) < ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) )
333	34 85	remulcld	\|- ( ph -> ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) e. RR )
334	1 2 3 4 5	bposlem5	\|- ( ph -> ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) )
335	71 34 84	lemul1d	\|- ( ph -> ( ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) <-> ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) <_ ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) ) )
336	334 335	mpbid	\|- ( ph -> ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) <_ ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) )
337	78	zred	\|- ( ph -> ( 2 x. K ) e. RR )
338	41	a1i	\|- ( ph -> 5 e. RR )
339		flle	\|- ( ( ( 2 x. N ) / 3 ) e. RR -> ( \|_ ` ( ( 2 x. N ) / 3 ) ) <_ ( ( 2 x. N ) / 3 ) )
340	74 339	syl	\|- ( ph -> ( \|_ ` ( ( 2 x. N ) / 3 ) ) <_ ( ( 2 x. N ) / 3 ) )
341	4 340	eqbrtrid	\|- ( ph -> K <_ ( ( 2 x. N ) / 3 ) )
342		2pos	\|- 0 < 2
343	30 342	pm3.2i	\|- ( 2 e. RR /\ 0 < 2 )
344	343	a1i	\|- ( ph -> ( 2 e. RR /\ 0 < 2 ) )
345		lemul2	\|- ( ( 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 ) ) ) )
346	104 74 344 345	syl3anc	\|- ( ph -> ( K <_ ( ( 2 x. N ) / 3 ) <-> ( 2 x. K ) <_ ( 2 x. ( ( 2 x. N ) / 3 ) ) ) )
347	341 346	mpbid	\|- ( ph -> ( 2 x. K ) <_ ( 2 x. ( ( 2 x. N ) / 3 ) ) )
348	22	nncnd	\|- ( ph -> ( 2 x. N ) e. CC )
349		3ne0	\|- 3 =/= 0
350	288 349	pm3.2i	\|- ( 3 e. CC /\ 3 =/= 0 )
351		divass	\|- ( ( 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 ) ) )
352	289 350 351	mp3an13	\|- ( ( 2 x. N ) e. CC -> ( ( 2 x. ( 2 x. N ) ) / 3 ) = ( 2 x. ( ( 2 x. N ) / 3 ) ) )
353	348 352	syl	\|- ( ph -> ( ( 2 x. ( 2 x. N ) ) / 3 ) = ( 2 x. ( ( 2 x. N ) / 3 ) ) )
354	9	nncnd	\|- ( ph -> N e. CC )
355		mulass	\|- ( ( 2 e. CC /\ 2 e. CC /\ N e. CC ) -> ( ( 2 x. 2 ) x. N ) = ( 2 x. ( 2 x. N ) ) )
356	289 289 354 355	mp3an12i	\|- ( ph -> ( ( 2 x. 2 ) x. N ) = ( 2 x. ( 2 x. N ) ) )
357		2t2e4	\|- ( 2 x. 2 ) = 4
358	357	oveq1i	\|- ( ( 2 x. 2 ) x. N ) = ( 4 x. N )
359	356 358	eqtr3di	\|- ( ph -> ( 2 x. ( 2 x. N ) ) = ( 4 x. N ) )
360	359	oveq1d	\|- ( ph -> ( ( 2 x. ( 2 x. N ) ) / 3 ) = ( ( 4 x. N ) / 3 ) )
361	353 360	eqtr3d	\|- ( ph -> ( 2 x. ( ( 2 x. N ) / 3 ) ) = ( ( 4 x. N ) / 3 ) )
362	347 361	breqtrd	\|- ( ph -> ( 2 x. K ) <_ ( ( 4 x. N ) / 3 ) )
363	337 40 338 362	lesub1dd	\|- ( ph -> ( ( 2 x. K ) - 5 ) <_ ( ( ( 4 x. N ) / 3 ) - 5 ) )
364		1lt2	\|- 1 < 2
365	364	a1i	\|- ( ph -> 1 < 2 )
366	257 365 82 43	cxpled	\|- ( ph -> ( ( ( 2 x. K ) - 5 ) <_ ( ( ( 4 x. N ) / 3 ) - 5 ) <-> ( 2 ^c ( ( 2 x. K ) - 5 ) ) <_ ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )
367	363 366	mpbid	\|- ( ph -> ( 2 ^c ( ( 2 x. K ) - 5 ) ) <_ ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) )
368	85 46 33	lemul2d	\|- ( ph -> ( ( 2 ^c ( ( 2 x. K ) - 5 ) ) <_ ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) <-> ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) <_ ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) ) )
369	367 368	mpbid	\|- ( ph -> ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) <_ ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )
370	86 333 47 336 369	letrd	\|- ( ph -> ( ( seq 1 ( x. , F ) ` M ) x. ( 2 ^c ( ( 2 x. K ) - 5 ) ) ) <_ ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )
371	19 86 47 332 370	ltletrd	\|- ( ph -> ( ( 2 x. N ) _C N ) < ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )
372	14 19 47 58 371	lttrd	\|- ( ph -> ( ( 4 ^ N ) / N ) < ( ( ( 2 x. N ) ^c ( ( ( sqrt ` ( 2 x. N ) ) / 3 ) + 2 ) ) x. ( 2 ^c ( ( ( 4 x. N ) / 3 ) - 5 ) ) ) )

Metamath Proof Explorer

Theorem bposlem6

Proof