Theorem bposlem5 16315

Description: Lemma for bpos . Bound the product of all small primes in the binomial coefficient. (Contributed by Mario Carneiro, 15-Mar-2014.) (Proof shortened by AV, 15-Sep-2021.)

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
bposlem5	|- ( ph -> ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) )

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 bposlem5

Dummy variables k x q u v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		bpos.3	. . . . . 6 |- F = ( n e. NN |-> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )
2		id 19	. . . . . . . 8 |- ( n e. Prime -> n e. Prime )
3		5nn 9480	. . . . . . . . . . 11 |- 5 e. NN
4		bpos.1	. . . . . . . . . . 11 |- ( ph -> N e. ( ZZ>= ` 5 ) )
5		eluznn 10016	. . . . . . . . . . 11 |- ( ( 5 e. NN /\ N e. ( ZZ>= ` 5 ) ) -> N e. NN )
6	3, 4, 5	sylancr 418	. . . . . . . . . 10 |- ( ph -> N e. NN )
7	6	nnnn0d 9631	. . . . . . . . 9 |- ( ph -> N e. NN0 )
8		fzctr 10557	. . . . . . . . 9 |- ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) )
9		bccl2 11228	. . . . . . . . 9 |- ( N e. ( 0 ... ( 2 x. N ) ) -> ( ( 2 x. N ) _C N ) e. NN )
10	7, 8, 9	3syl 17	. . . . . . . 8 |- ( ph -> ( ( 2 x. N ) _C N ) e. NN )
11		pccl 13107	. . . . . . . 8 |- ( ( n e. Prime /\ ( ( 2 x. N ) _C N ) e. NN ) -> ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
12	2, 10, 11	syl2anr 290	. . . . . . 7 |- ( ( ph /\ n e. Prime ) -> ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
13	12	ralrimiva 2623	. . . . . 6 |- ( ph -> A. n e. Prime ( n pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
14	1, 13	pcmptcl 13150	. . . . 5 |- ( ph -> ( F : NN --> NN /\ seq 1 ( x. , F ) : NN --> NN ) )
15	14	simprd 114	. . . 4 |- ( ph -> seq 1 ( x. , F ) : NN --> NN )
16		3nn 9478	. . . . 5 |- 3 e. NN
17		bpos.5	. . . . . 6 |- M = ( |_ ` ( sqr ` ( 2 x. N ) ) )
18		2nn 9477	. . . . . . . . . . 11 |- 2 e. NN
19		nnmulcl 9334	. . . . . . . . . . 11 |- ( ( 2 e. NN /\ N e. NN ) -> ( 2 x. N ) e. NN )
20	18, 6, 19	sylancr 418	. . . . . . . . . 10 |- ( ph -> ( 2 x. N ) e. NN )
21	20	nnnn0d 9631	. . . . . . . . 9 |- ( ph -> ( 2 x. N ) e. NN0 )
22		sqrtrirr 13014	. . . . . . . . 9 |- ( ( 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 ) ) )
23	21, 22	syl 14	. . . . . . . 8 |- ( ph -> ( ( sqr ` ( 2 x. N ) ) e. QQ \/ ( ( sqr ` ( 2 x. N ) ) e. RR /\ A. q e. QQ ( sqr ` ( 2 x. N ) ) # q ) ) )
24		flapcl 10728	. . . . . . . 8 |- ( ( ( sqr ` ( 2 x. N ) ) e. QQ \/ ( ( sqr ` ( 2 x. N ) ) e. RR /\ A. q e. QQ ( sqr ` ( 2 x. N ) ) # q ) ) -> ( |_ ` ( sqr ` ( 2 x. N ) ) ) e. ZZ )
25	23, 24	syl 14	. . . . . . 7 |- ( ph -> ( |_ ` ( sqr ` ( 2 x. N ) ) ) e. ZZ )
26		sqrt9 11836	. . . . . . . . 9 |- ( sqr ` 9 ) = 3
27		9re 9400	. . . . . . . . . . . 12 |- 9 e. RR
28	27	a1i 9	. . . . . . . . . . 11 |- ( ph -> 9 e. RR )
29		10re 9810	. . . . . . . . . . . 12 |- ; 1 0 e. RR
30	29	a1i 9	. . . . . . . . . . 11 |- ( ph -> ; 1 0 e. RR )
31		2z 9683	. . . . . . . . . . . . 13 |- 2 e. ZZ
32	6	nnzd 9778	. . . . . . . . . . . . 13 |- ( ph -> N e. ZZ )
33		zmulcl 9709	. . . . . . . . . . . . 13 |- ( ( 2 e. ZZ /\ N e. ZZ ) -> ( 2 x. N ) e. ZZ )
34	31, 32, 33	sylancr 418	. . . . . . . . . . . 12 |- ( ph -> ( 2 x. N ) e. ZZ )
35	34	zred 9779	. . . . . . . . . . 11 |- ( ph -> ( 2 x. N ) e. RR )
36		lep1 9183	. . . . . . . . . . . . . 14 |- ( 9 e. RR -> 9 <_ ( 9 + 1 ) )
37	27, 36	ax-mp 5	. . . . . . . . . . . . 13 |- 9 <_ ( 9 + 1 )
38		9p1e10 9790	. . . . . . . . . . . . 13 |- ( 9 + 1 ) = ; 1 0
39	37, 38	breqtri 4156	. . . . . . . . . . . 12 |- 9 <_ ; 1 0
40	39	a1i 9	. . . . . . . . . . 11 |- ( ph -> 9 <_ ; 1 0 )
41		5cn 9393	. . . . . . . . . . . . 13 |- 5 e. CC
42		2cn 9384	. . . . . . . . . . . . 13 |- 2 e. CC
43		5t2e10 9892	. . . . . . . . . . . . 13 |- ( 5 x. 2 ) = ; 1 0
44	41, 42, 43	mulcomli 8339	. . . . . . . . . . . 12 |- ( 2 x. 5 ) = ; 1 0
45		eluzle 9950	. . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` 5 ) -> 5 <_ N )
46	4, 45	syl 14	. . . . . . . . . . . . 13 |- ( ph -> 5 <_ N )
47	6	nnred 9326	. . . . . . . . . . . . . 14 |- ( ph -> N e. RR )
48		5re 9392	. . . . . . . . . . . . . . 15 |- 5 e. RR
49		2re 9383	. . . . . . . . . . . . . . . 16 |- 2 e. RR
50		2pos 9404	. . . . . . . . . . . . . . . 16 |- 0 < 2
51	49, 50	pm3.2i 272	. . . . . . . . . . . . . . 15 |- ( 2 e. RR /\ 0 < 2 )
52		lemul2 9195	. . . . . . . . . . . . . . 15 |- ( ( 5 e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( 5 <_ N <-> ( 2 x. 5 ) <_ ( 2 x. N ) ) )
53	48, 51, 52	mp3an13 1369	. . . . . . . . . . . . . 14 |- ( N e. RR -> ( 5 <_ N <-> ( 2 x. 5 ) <_ ( 2 x. N ) ) )
54	47, 53	syl 14	. . . . . . . . . . . . 13 |- ( ph -> ( 5 <_ N <-> ( 2 x. 5 ) <_ ( 2 x. N ) ) )
55	46, 54	mpbid 147	. . . . . . . . . . . 12 |- ( ph -> ( 2 x. 5 ) <_ ( 2 x. N ) )
56	44, 55	eqbrtrrid 4167	. . . . . . . . . . 11 |- ( ph -> ; 1 0 <_ ( 2 x. N ) )
57	28, 30, 35, 40, 56	letrd 8457	. . . . . . . . . 10 |- ( ph -> 9 <_ ( 2 x. N ) )
58		0re 8332	. . . . . . . . . . . . 13 |- 0 e. RR
59		9pos 9417	. . . . . . . . . . . . 13 |- 0 < 9
60	58, 27, 59	ltleii 8435	. . . . . . . . . . . 12 |- 0 <_ 9
61	27, 60	pm3.2i 272	. . . . . . . . . . 11 |- ( 9 e. RR /\ 0 <_ 9 )
62	20	nnrpd 10112	. . . . . . . . . . . . 13 |- ( ph -> ( 2 x. N ) e. RR+ )
63	62	rpge0d 10118	. . . . . . . . . . . 12 |- ( ph -> 0 <_ ( 2 x. N ) )
64	35, 63	jca 306	. . . . . . . . . . 11 |- ( ph -> ( ( 2 x. N ) e. RR /\ 0 <_ ( 2 x. N ) ) )
65		sqrtle 11824	. . . . . . . . . . 11 |- ( ( ( 9 e. RR /\ 0 <_ 9 ) /\ ( ( 2 x. N ) e. RR /\ 0 <_ ( 2 x. N ) ) ) -> ( 9 <_ ( 2 x. N ) <-> ( sqr ` 9 ) <_ ( sqr ` ( 2 x. N ) ) ) )
66	61, 64, 65	sylancr 418	. . . . . . . . . 10 |- ( ph -> ( 9 <_ ( 2 x. N ) <-> ( sqr ` 9 ) <_ ( sqr ` ( 2 x. N ) ) ) )
67	57, 66	mpbid 147	. . . . . . . . 9 |- ( ph -> ( sqr ` 9 ) <_ ( sqr ` ( 2 x. N ) ) )
68	26, 67	eqbrtrrid 4167	. . . . . . . 8 |- ( ph -> 3 <_ ( sqr ` ( 2 x. N ) ) )
69		3z 9684	. . . . . . . . 9 |- 3 e. ZZ
70		flapge 10737	. . . . . . . . 9 |- ( ( ( ( sqr ` ( 2 x. N ) ) e. QQ \/ ( ( sqr ` ( 2 x. N ) ) e. RR /\ A. q e. QQ ( sqr ` ( 2 x. N ) ) # q ) ) /\ 3 e. ZZ ) -> ( 3 <_ ( sqr ` ( 2 x. N ) ) <-> 3 <_ ( |_ ` ( sqr ` ( 2 x. N ) ) ) ) )
71	23, 69, 70	sylancl 417	. . . . . . . 8 |- ( ph -> ( 3 <_ ( sqr ` ( 2 x. N ) ) <-> 3 <_ ( |_ ` ( sqr ` ( 2 x. N ) ) ) ) )
72	68, 71	mpbid 147	. . . . . . 7 |- ( ph -> 3 <_ ( |_ ` ( sqr ` ( 2 x. N ) ) ) )
73	69	eluz1i 9945	. . . . . . 7 |- ( ( |_ ` ( sqr ` ( 2 x. N ) ) ) e. ( ZZ>= ` 3 ) <-> ( ( |_ ` ( sqr ` ( 2 x. N ) ) ) e. ZZ /\ 3 <_ ( |_ ` ( sqr ` ( 2 x. N ) ) ) ) )
74	25, 72, 73	sylanbrc 421	. . . . . 6 |- ( ph -> ( |_ ` ( sqr ` ( 2 x. N ) ) ) e. ( ZZ>= ` 3 ) )
75	17, 74	eqeltrid 2325	. . . . 5 |- ( ph -> M e. ( ZZ>= ` 3 ) )
76		eluznn 10016	. . . . 5 |- ( ( 3 e. NN /\ M e. ( ZZ>= ` 3 ) ) -> M e. NN )
77	16, 75, 76	sylancr 418	. . . 4 |- ( ph -> M e. NN )
78	15, 77	ffvelcdmd 5847	. . 3 |- ( ph -> ( seq 1 ( x. , F ) ` M ) e. NN )
79	78	nnred 9326	. 2 |- ( ph -> ( seq 1 ( x. , F ) ` M ) e. RR )
80		nnq 10049	. . . . . 6 |- ( M e. NN -> M e. QQ )
81	77, 80	syl 14	. . . . 5 |- ( ph -> M e. QQ )
82		ppiqcl 16251	. . . . 5 |- ( M e. QQ -> (π ` M ) e. NN0 )
83	81, 82	syl 14	. . . 4 |- ( ph -> (π ` M ) e. NN0 )
84	20, 83	nnexpcld 11154	. . 3 |- ( ph -> ( ( 2 x. N ) ^ (π ` M ) ) e. NN )
85	84	nnred 9326	. 2 |- ( ph -> ( ( 2 x. N ) ^ (π ` M ) ) e. RR )
86	35, 63	resqrtcld 11952	. . . . . 6 |- ( ph -> ( sqr ` ( 2 x. N ) ) e. RR )
87		nndivre 9349	. . . . . 6 |- ( ( ( sqr ` ( 2 x. N ) ) e. RR /\ 3 e. NN ) -> ( ( sqr ` ( 2 x. N ) ) / 3 ) e. RR )
88	86, 16, 87	sylancl 417	. . . . 5 |- ( ph -> ( ( sqr ` ( 2 x. N ) ) / 3 ) e. RR )
89		readdcl 8311	. . . . 5 |- ( ( ( ( sqr ` ( 2 x. N ) ) / 3 ) e. RR /\ 2 e. RR ) -> ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) e. RR )
90	88, 49, 89	sylancl 417	. . . 4 |- ( ph -> ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) e. RR )
91	62, 90	rpcxpcld 16168	. . 3 |- ( ph -> ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) e. RR+ )
92	91	rpred 10114	. 2 |- ( ph -> ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) e. RR )
93		fveq2 5698	. . . . . 6 |- ( x = 1 -> ( seq 1 ( x. , F ) ` x ) = ( seq 1 ( x. , F ) ` 1 ) )
94		fveq2 5698	. . . . . . . 8 |- ( x = 1 -> (π ` x ) = (π ` 1 ) )
95		ppi1 16270	. . . . . . . 8 |- (π ` 1 ) = 0
96	94, 95	eqtrdi 2287	. . . . . . 7 |- ( x = 1 -> (π ` x ) = 0 )
97	96	oveq2d 6104	. . . . . 6 |- ( x = 1 -> ( ( 2 x. N ) ^ (π ` x ) ) = ( ( 2 x. N ) ^ 0 ) )
98	93, 97	breq12d 4144	. . . . 5 |- ( x = 1 -> ( ( seq 1 ( x. , F ) ` x ) <_ ( ( 2 x. N ) ^ (π ` x ) ) <-> ( seq 1 ( x. , F ) ` 1 ) <_ ( ( 2 x. N ) ^ 0 ) ) )
99	98	imbi2d 230	. . . 4 |- ( x = 1 -> ( ( ph -> ( seq 1 ( x. , F ) ` x ) <_ ( ( 2 x. N ) ^ (π ` x ) ) ) <-> ( ph -> ( seq 1 ( x. , F ) ` 1 ) <_ ( ( 2 x. N ) ^ 0 ) ) ) )
100		fveq2 5698	. . . . . 6 |- ( x = k -> ( seq 1 ( x. , F ) ` x ) = ( seq 1 ( x. , F ) ` k ) )
101		fveq2 5698	. . . . . . 7 |- ( x = k -> (π ` x ) = (π ` k ) )
102	101	oveq2d 6104	. . . . . 6 |- ( x = k -> ( ( 2 x. N ) ^ (π ` x ) ) = ( ( 2 x. N ) ^ (π ` k ) ) )
103	100, 102	breq12d 4144	. . . . 5 |- ( x = k -> ( ( seq 1 ( x. , F ) ` x ) <_ ( ( 2 x. N ) ^ (π ` x ) ) <-> ( seq 1 ( x. , F ) ` k ) <_ ( ( 2 x. N ) ^ (π ` k ) ) ) )
104	103	imbi2d 230	. . . 4 |- ( x = k -> ( ( ph -> ( seq 1 ( x. , F ) ` x ) <_ ( ( 2 x. N ) ^ (π ` x ) ) ) <-> ( ph -> ( seq 1 ( x. , F ) ` k ) <_ ( ( 2 x. N ) ^ (π ` k ) ) ) ) )
105		fveq2 5698	. . . . . 6 |- ( x = ( k + 1 ) -> ( seq 1 ( x. , F ) ` x ) = ( seq 1 ( x. , F ) ` ( k + 1 ) ) )
106		fveq2 5698	. . . . . . 7 |- ( x = ( k + 1 ) -> (π ` x ) = (π ` ( k + 1 ) ) )
107	106	oveq2d 6104	. . . . . 6 |- ( x = ( k + 1 ) -> ( ( 2 x. N ) ^ (π ` x ) ) = ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) )
108	105, 107	breq12d 4144	. . . . 5 |- ( x = ( k + 1 ) -> ( ( seq 1 ( x. , F ) ` x ) <_ ( ( 2 x. N ) ^ (π ` x ) ) <-> ( seq 1 ( x. , F ) ` ( k + 1 ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) ) )
109	108	imbi2d 230	. . . 4 |- ( x = ( k + 1 ) -> ( ( ph -> ( seq 1 ( x. , F ) ` x ) <_ ( ( 2 x. N ) ^ (π ` x ) ) ) <-> ( ph -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) ) ) )
110		fveq2 5698	. . . . . 6 |- ( x = M -> ( seq 1 ( x. , F ) ` x ) = ( seq 1 ( x. , F ) ` M ) )
111		fveq2 5698	. . . . . . 7 |- ( x = M -> (π ` x ) = (π ` M ) )
112	111	oveq2d 6104	. . . . . 6 |- ( x = M -> ( ( 2 x. N ) ^ (π ` x ) ) = ( ( 2 x. N ) ^ (π ` M ) ) )
113	110, 112	breq12d 4144	. . . . 5 |- ( x = M -> ( ( seq 1 ( x. , F ) ` x ) <_ ( ( 2 x. N ) ^ (π ` x ) ) <-> ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^ (π ` M ) ) ) )
114	113	imbi2d 230	. . . 4 |- ( x = M -> ( ( ph -> ( seq 1 ( x. , F ) ` x ) <_ ( ( 2 x. N ) ^ (π ` x ) ) ) <-> ( ph -> ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^ (π ` M ) ) ) ) )
115		1zzd 9682	. . . . . . . 8 |- ( ph -> 1 e. ZZ )
116		eleq1 2301	. . . . . . . . . . 11 |- ( n = u -> ( n e. Prime <-> u e. Prime ) )
117		id 19	. . . . . . . . . . . 12 |- ( n = u -> n = u )
118		oveq1 6095	. . . . . . . . . . . 12 |- ( n = u -> ( n pCnt ( ( 2 x. N ) _C N ) ) = ( u pCnt ( ( 2 x. N ) _C N ) ) )
119	117, 118	oveq12d 6106	. . . . . . . . . . 11 |- ( n = u -> ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) = ( u ^ ( u pCnt ( ( 2 x. N ) _C N ) ) ) )
120	116, 119	ifbieq1d 3663	. . . . . . . . . 10 |- ( n = u -> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) = if ( u e. Prime , ( u ^ ( u pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )
121		elnnuz 9975	. . . . . . . . . . 11 |- ( u e. NN <-> u e. ( ZZ>= ` 1 ) )
122	121	bilanri 389	. . . . . . . . . 10 |- ( ( ph /\ u e. ( ZZ>= ` 1 ) ) -> u e. NN )
123	122	adantr 276	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. ( ZZ>= ` 1 ) ) /\ u e. Prime ) -> u e. NN )
124		simpr 110	. . . . . . . . . . . . 13 |- ( ( ( ph /\ u e. ( ZZ>= ` 1 ) ) /\ u e. Prime ) -> u e. Prime )
125	10	ad2antrr 492	. . . . . . . . . . . . 13 |- ( ( ( ph /\ u e. ( ZZ>= ` 1 ) ) /\ u e. Prime ) -> ( ( 2 x. N ) _C N ) e. NN )
126	124, 125	pccld 13108	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. ( ZZ>= ` 1 ) ) /\ u e. Prime ) -> ( u pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
127	123, 126	nnexpcld 11154	. . . . . . . . . . 11 |- ( ( ( ph /\ u e. ( ZZ>= ` 1 ) ) /\ u e. Prime ) -> ( u ^ ( u pCnt ( ( 2 x. N ) _C N ) ) ) e. NN )
128		1nn 9324	. . . . . . . . . . . 12 |- 1 e. NN
129	128	a1i 9	. . . . . . . . . . 11 |- ( ( ( ph /\ u e. ( ZZ>= ` 1 ) ) /\ -. u e. Prime ) -> 1 e. NN )
130		prmdc 12933	. . . . . . . . . . . 12 |- ( u e. NN -> DECID u e. Prime )
131	122, 130	syl 14	. . . . . . . . . . 11 |- ( ( ph /\ u e. ( ZZ>= ` 1 ) ) -> DECID u e. Prime )
132	127, 129, 131	ifcldadc 3670	. . . . . . . . . 10 |- ( ( ph /\ u e. ( ZZ>= ` 1 ) ) -> if ( u e. Prime , ( u ^ ( u pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) e. NN )
133	1, 120, 122, 132	fvmptd3 5802	. . . . . . . . 9 |- ( ( ph /\ u e. ( ZZ>= ` 1 ) ) -> ( F ` u ) = if ( u e. Prime , ( u ^ ( u pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )
134	133, 132	eqeltrd 2315	. . . . . . . 8 |- ( ( ph /\ u e. ( ZZ>= ` 1 ) ) -> ( F ` u ) e. NN )
135		nnmulcl 9334	. . . . . . . . 9 |- ( ( u e. NN /\ v e. NN ) -> ( u x. v ) e. NN )
136	135	adantl 277	. . . . . . . 8 |- ( ( ph /\ ( u e. NN /\ v e. NN ) ) -> ( u x. v ) e. NN )
137	115, 134, 136	seq3-1 10920	. . . . . . 7 |- ( ph -> ( seq 1 ( x. , F ) ` 1 ) = ( F ` 1 ) )
138		1nprm 12917	. . . . . . . . . . 11 |- -. 1 e. Prime
139		eleq1 2301	. . . . . . . . . . 11 |- ( n = 1 -> ( n e. Prime <-> 1 e. Prime ) )
140	138, 139	mtbiri 686	. . . . . . . . . 10 |- ( n = 1 -> -. n e. Prime )
141	140	iffalsed 3650	. . . . . . . . 9 |- ( n = 1 -> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) = 1 )
142		1ex 8327	. . . . . . . . 9 |- 1 e. _V
143	141, 1, 142	fvmpt 5785	. . . . . . . 8 |- ( 1 e. NN -> ( F ` 1 ) = 1 )
144	128, 143	ax-mp 5	. . . . . . 7 |- ( F ` 1 ) = 1
145	137, 144	eqtrdi 2287	. . . . . 6 |- ( ph -> ( seq 1 ( x. , F ) ` 1 ) = 1 )
146		1le1 8908	. . . . . 6 |- 1 <_ 1
147	145, 146	eqbrtrdi 4170	. . . . 5 |- ( ph -> ( seq 1 ( x. , F ) ` 1 ) <_ 1 )
148	34	zcnd 9780	. . . . . 6 |- ( ph -> ( 2 x. N ) e. CC )
149	148	exp0d 11126	. . . . 5 |- ( ph -> ( ( 2 x. N ) ^ 0 ) = 1 )
150	147, 149	breqtrrd 4159	. . . 4 |- ( ph -> ( seq 1 ( x. , F ) ` 1 ) <_ ( ( 2 x. N ) ^ 0 ) )
151	15	ffvelcdmda 5846	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( seq 1 ( x. , F ) ` k ) e. NN )
152	151	nnred 9326	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( seq 1 ( x. , F ) ` k ) e. RR )
153	152	adantr 276	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( seq 1 ( x. , F ) ` k ) e. RR )
154	20	ad2antrr 492	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( 2 x. N ) e. NN )
155		nnq 10049	. . . . . . . . . . . . . 14 |- ( k e. NN -> k e. QQ )
156	155	ad2antlr 493	. . . . . . . . . . . . 13 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> k e. QQ )
157		ppiqcl 16251	. . . . . . . . . . . . 13 |- ( k e. QQ -> (π ` k ) e. NN0 )
158	156, 157	syl 14	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> (π ` k ) e. NN0 )
159	154, 158	nnexpcld 11154	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( 2 x. N ) ^ (π ` k ) ) e. NN )
160	159	nnred 9326	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( 2 x. N ) ^ (π ` k ) ) e. RR )
161		nnre 9320	. . . . . . . . . . . . 13 |- ( ( 2 x. N ) e. NN -> ( 2 x. N ) e. RR )
162		nngt0 9338	. . . . . . . . . . . . 13 |- ( ( 2 x. N ) e. NN -> 0 < ( 2 x. N ) )
163	161, 162	jca 306	. . . . . . . . . . . 12 |- ( ( 2 x. N ) e. NN -> ( ( 2 x. N ) e. RR /\ 0 < ( 2 x. N ) ) )
164	20, 163	syl 14	. . . . . . . . . . 11 |- ( ph -> ( ( 2 x. N ) e. RR /\ 0 < ( 2 x. N ) ) )
165	164	ad2antrr 492	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( 2 x. N ) e. RR /\ 0 < ( 2 x. N ) ) )
166		lemul1 8929	. . . . . . . . . 10 |- ( ( ( seq 1 ( x. , F ) ` k ) e. RR /\ ( ( 2 x. N ) ^ (π ` k ) ) e. RR /\ ( ( 2 x. N ) e. RR /\ 0 < ( 2 x. N ) ) ) -> ( ( seq 1 ( x. , F ) ` k ) <_ ( ( 2 x. N ) ^ (π ` k ) ) <-> ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) <_ ( ( ( 2 x. N ) ^ (π ` k ) ) x. ( 2 x. N ) ) ) )
167	153, 160, 165, 166	syl3anc 1278	. . . . . . . . 9 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( seq 1 ( x. , F ) ` k ) <_ ( ( 2 x. N ) ^ (π ` k ) ) <-> ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) <_ ( ( ( 2 x. N ) ^ (π ` k ) ) x. ( 2 x. N ) ) ) )
168		nnz 9674	. . . . . . . . . . . . . 14 |- ( k e. NN -> k e. ZZ )
169	168	adantl 277	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> k e. ZZ )
170		ppiprm 16259	. . . . . . . . . . . . 13 |- ( ( k e. ZZ /\ ( k + 1 ) e. Prime ) -> (π ` ( k + 1 ) ) = ( (π ` k ) + 1 ) )
171	169, 170	sylan 283	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> (π ` ( k + 1 ) ) = ( (π ` k ) + 1 ) )
172	171	oveq2d 6104	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) = ( ( 2 x. N ) ^ ( (π ` k ) + 1 ) ) )
173	148	ad2antrr 492	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( 2 x. N ) e. CC )
174	173, 158	expp1d 11133	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( 2 x. N ) ^ ( (π ` k ) + 1 ) ) = ( ( ( 2 x. N ) ^ (π ` k ) ) x. ( 2 x. N ) ) )
175	172, 174	eqtrd 2271	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) = ( ( ( 2 x. N ) ^ (π ` k ) ) x. ( 2 x. N ) ) )
176	175	breq2d 4143	. . . . . . . . 9 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) <-> ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) <_ ( ( ( 2 x. N ) ^ (π ` k ) ) x. ( 2 x. N ) ) ) )
177	167, 176	bitr4d 191	. . . . . . . 8 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( seq 1 ( x. , F ) ` k ) <_ ( ( 2 x. N ) ^ (π ` k ) ) <-> ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) ) )
178		simpr 110	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> k e. NN )
179		nnuz 9974	. . . . . . . . . . . . 13 |- NN = ( ZZ>= ` 1 )
180	178, 179	eleqtrdi 2331	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
181	134	adantlr 481	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ u e. ( ZZ>= ` 1 ) ) -> ( F ` u ) e. NN )
182	135	adantl 277	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ ( u e. NN /\ v e. NN ) ) -> ( u x. v ) e. NN )
183	180, 181, 182	seq3p1 10923	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) = ( ( seq 1 ( x. , F ) ` k ) x. ( F ` ( k + 1 ) ) ) )
184	183	adantr 276	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) = ( ( seq 1 ( x. , F ) ` k ) x. ( F ` ( k + 1 ) ) ) )
185		eleq1 2301	. . . . . . . . . . . . . . 15 |- ( n = ( k + 1 ) -> ( n e. Prime <-> ( k + 1 ) e. Prime ) )
186		id 19	. . . . . . . . . . . . . . . 16 |- ( n = ( k + 1 ) -> n = ( k + 1 ) )
187		oveq1 6095	. . . . . . . . . . . . . . . 16 |- ( n = ( k + 1 ) -> ( n pCnt ( ( 2 x. N ) _C N ) ) = ( ( k + 1 ) pCnt ( ( 2 x. N ) _C N ) ) )
188	186, 187	oveq12d 6106	. . . . . . . . . . . . . . 15 |- ( n = ( k + 1 ) -> ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) = ( ( k + 1 ) ^ ( ( k + 1 ) pCnt ( ( 2 x. N ) _C N ) ) ) )
189	185, 188	ifbieq1d 3663	. . . . . . . . . . . . . 14 |- ( n = ( k + 1 ) -> if ( n e. Prime , ( n ^ ( n pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) = if ( ( k + 1 ) e. Prime , ( ( k + 1 ) ^ ( ( k + 1 ) pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )
190		peano2nn 9325	. . . . . . . . . . . . . . 15 |- ( k e. NN -> ( k + 1 ) e. NN )
191	190	adantl 277	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( k + 1 ) e. NN )
192	191	adantr 276	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( k + 1 ) e. NN )
193		simpr 110	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( k + 1 ) e. Prime )
194	10	ad2antrr 492	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( 2 x. N ) _C N ) e. NN )
195	193, 194	pccld 13108	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( k + 1 ) pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
196	192, 195	nnexpcld 11154	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( k + 1 ) ^ ( ( k + 1 ) pCnt ( ( 2 x. N ) _C N ) ) ) e. NN )
197	128	a1i 9	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ k e. NN ) /\ -. ( k + 1 ) e. Prime ) -> 1 e. NN )
198		prmdc 12933	. . . . . . . . . . . . . . . 16 |- ( ( k + 1 ) e. NN -> DECID ( k + 1 ) e. Prime )
199	191, 198	syl 14	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. NN ) -> DECID ( k + 1 ) e. Prime )
200	196, 197, 199	ifcldadc 3670	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> if ( ( k + 1 ) e. Prime , ( ( k + 1 ) ^ ( ( k + 1 ) pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) e. NN )
201	1, 189, 191, 200	fvmptd3 5802	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) = if ( ( k + 1 ) e. Prime , ( ( k + 1 ) ^ ( ( k + 1 ) pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) )
202		iftrue 3645	. . . . . . . . . . . . 13 |- ( ( k + 1 ) e. Prime -> if ( ( k + 1 ) e. Prime , ( ( k + 1 ) ^ ( ( k + 1 ) pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) = ( ( k + 1 ) ^ ( ( k + 1 ) pCnt ( ( 2 x. N ) _C N ) ) ) )
203	201, 202	sylan9eq 2291	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( F ` ( k + 1 ) ) = ( ( k + 1 ) ^ ( ( k + 1 ) pCnt ( ( 2 x. N ) _C N ) ) ) )
204	6	adantr 276	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> N e. NN )
205		bposlem1 16311	. . . . . . . . . . . . 13 |- ( ( N e. NN /\ ( k + 1 ) e. Prime ) -> ( ( k + 1 ) ^ ( ( k + 1 ) pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )
206	204, 205	sylan 283	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( k + 1 ) ^ ( ( k + 1 ) pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )
207	203, 206	eqbrtrd 4153	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( F ` ( k + 1 ) ) <_ ( 2 x. N ) )
208	14	simpld 112	. . . . . . . . . . . . . . 15 |- ( ph -> F : NN --> NN )
209		ffvelcdm 5844	. . . . . . . . . . . . . . 15 |- ( ( F : NN --> NN /\ ( k + 1 ) e. NN ) -> ( F ` ( k + 1 ) ) e. NN )
210	208, 190, 209	syl2an 289	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) e. NN )
211	210	nnred 9326	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) e. RR )
212	211	adantr 276	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( F ` ( k + 1 ) ) e. RR )
213	35	ad2antrr 492	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( 2 x. N ) e. RR )
214		nnre 9320	. . . . . . . . . . . . . . 15 |- ( ( seq 1 ( x. , F ) ` k ) e. NN -> ( seq 1 ( x. , F ) ` k ) e. RR )
215		nngt0 9338	. . . . . . . . . . . . . . 15 |- ( ( seq 1 ( x. , F ) ` k ) e. NN -> 0 < ( seq 1 ( x. , F ) ` k ) )
216	214, 215	jca 306	. . . . . . . . . . . . . 14 |- ( ( seq 1 ( x. , F ) ` k ) e. NN -> ( ( seq 1 ( x. , F ) ` k ) e. RR /\ 0 < ( seq 1 ( x. , F ) ` k ) ) )
217	151, 216	syl 14	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( ( seq 1 ( x. , F ) ` k ) e. RR /\ 0 < ( seq 1 ( x. , F ) ` k ) ) )
218	217	adantr 276	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( seq 1 ( x. , F ) ` k ) e. RR /\ 0 < ( seq 1 ( x. , F ) ` k ) ) )
219		lemul2 9195	. . . . . . . . . . . 12 |- ( ( ( F ` ( k + 1 ) ) e. RR /\ ( 2 x. N ) e. RR /\ ( ( seq 1 ( x. , F ) ` k ) e. RR /\ 0 < ( seq 1 ( x. , F ) ` k ) ) ) -> ( ( F ` ( k + 1 ) ) <_ ( 2 x. N ) <-> ( ( seq 1 ( x. , F ) ` k ) x. ( F ` ( k + 1 ) ) ) <_ ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) ) )
220	212, 213, 218, 219	syl3anc 1278	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( F ` ( k + 1 ) ) <_ ( 2 x. N ) <-> ( ( seq 1 ( x. , F ) ` k ) x. ( F ` ( k + 1 ) ) ) <_ ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) ) )
221	207, 220	mpbid 147	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( seq 1 ( x. , F ) ` k ) x. ( F ` ( k + 1 ) ) ) <_ ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) )
222	184, 221	eqbrtrd 4153	. . . . . . . . 9 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) <_ ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) )
223		ffvelcdm 5844	. . . . . . . . . . . . 13 |- ( ( seq 1 ( x. , F ) : NN --> NN /\ ( k + 1 ) e. NN ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) e. NN )
224	15, 190, 223	syl2an 289	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) e. NN )
225	224	nnred 9326	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) e. RR )
226	20	adantr 276	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> ( 2 x. N ) e. NN )
227	151, 226	nnmulcld 9362	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) e. NN )
228	227	nnred 9326	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) e. RR )
229		nnq 10049	. . . . . . . . . . . . . . 15 |- ( ( k + 1 ) e. NN -> ( k + 1 ) e. QQ )
230	191, 229	syl 14	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. NN ) -> ( k + 1 ) e. QQ )
231		ppiqcl 16251	. . . . . . . . . . . . . 14 |- ( ( k + 1 ) e. QQ -> (π ` ( k + 1 ) ) e. NN0 )
232	230, 231	syl 14	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> (π ` ( k + 1 ) ) e. NN0 )
233	226, 232	nnexpcld 11154	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) e. NN )
234	233	nnred 9326	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) e. RR )
235		letr 8414	. . . . . . . . . . 11 |- ( ( ( seq 1 ( x. , F ) ` ( k + 1 ) ) e. RR /\ ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) e. RR /\ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) e. RR ) -> ( ( ( seq 1 ( x. , F ) ` ( k + 1 ) ) <_ ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) /\ ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) ) )
236	225, 228, 234, 235	syl3anc 1278	. . . . . . . . . 10 |- ( ( ph /\ k e. NN ) -> ( ( ( seq 1 ( x. , F ) ` ( k + 1 ) ) <_ ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) /\ ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) ) )
237	236	adantr 276	. . . . . . . . 9 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( ( seq 1 ( x. , F ) ` ( k + 1 ) ) <_ ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) /\ ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) ) )
238	222, 237	mpand 433	. . . . . . . 8 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) ) )
239	177, 238	sylbid 150	. . . . . . 7 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( seq 1 ( x. , F ) ` k ) <_ ( ( 2 x. N ) ^ (π ` k ) ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) ) )
240	183	adantr 276	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ -. ( k + 1 ) e. Prime ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) = ( ( seq 1 ( x. , F ) ` k ) x. ( F ` ( k + 1 ) ) ) )
241		iffalse 3648	. . . . . . . . . . . 12 |- ( -. ( k + 1 ) e. Prime -> if ( ( k + 1 ) e. Prime , ( ( k + 1 ) ^ ( ( k + 1 ) pCnt ( ( 2 x. N ) _C N ) ) ) , 1 ) = 1 )
242	201, 241	sylan9eq 2291	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. NN ) /\ -. ( k + 1 ) e. Prime ) -> ( F ` ( k + 1 ) ) = 1 )
243	242	oveq2d 6104	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ -. ( k + 1 ) e. Prime ) -> ( ( seq 1 ( x. , F ) ` k ) x. ( F ` ( k + 1 ) ) ) = ( ( seq 1 ( x. , F ) ` k ) x. 1 ) )
244	151	adantr 276	. . . . . . . . . . . 12 |- ( ( ( ph /\ k e. NN ) /\ -. ( k + 1 ) e. Prime ) -> ( seq 1 ( x. , F ) ` k ) e. NN )
245	244	nncnd 9327	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. NN ) /\ -. ( k + 1 ) e. Prime ) -> ( seq 1 ( x. , F ) ` k ) e. CC )
246	245	mulridd 8349	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ -. ( k + 1 ) e. Prime ) -> ( ( seq 1 ( x. , F ) ` k ) x. 1 ) = ( seq 1 ( x. , F ) ` k ) )
247	240, 243, 246	3eqtrd 2275	. . . . . . . . 9 |- ( ( ( ph /\ k e. NN ) /\ -. ( k + 1 ) e. Prime ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) = ( seq 1 ( x. , F ) ` k ) )
248		ppinprm 16260	. . . . . . . . . . 11 |- ( ( k e. ZZ /\ -. ( k + 1 ) e. Prime ) -> (π ` ( k + 1 ) ) = (π ` k ) )
249	169, 248	sylan 283	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ -. ( k + 1 ) e. Prime ) -> (π ` ( k + 1 ) ) = (π ` k ) )
250	249	oveq2d 6104	. . . . . . . . 9 |- ( ( ( ph /\ k e. NN ) /\ -. ( k + 1 ) e. Prime ) -> ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) = ( ( 2 x. N ) ^ (π ` k ) ) )
251	247, 250	breq12d 4144	. . . . . . . 8 |- ( ( ( ph /\ k e. NN ) /\ -. ( k + 1 ) e. Prime ) -> ( ( seq 1 ( x. , F ) ` ( k + 1 ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) <-> ( seq 1 ( x. , F ) ` k ) <_ ( ( 2 x. N ) ^ (π ` k ) ) ) )
252	251	biimprd 158	. . . . . . 7 |- ( ( ( ph /\ k e. NN ) /\ -. ( k + 1 ) e. Prime ) -> ( ( seq 1 ( x. , F ) ` k ) <_ ( ( 2 x. N ) ^ (π ` k ) ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) ) )
253		exmiddc 848	. . . . . . . 8 |- (DECID ( k + 1 ) e. Prime -> ( ( k + 1 ) e. Prime \/ -. ( k + 1 ) e. Prime ) )
254	199, 253	syl 14	. . . . . . 7 |- ( ( ph /\ k e. NN ) -> ( ( k + 1 ) e. Prime \/ -. ( k + 1 ) e. Prime ) )
255	239, 252, 254	mpjaodan 810	. . . . . 6 |- ( ( ph /\ k e. NN ) -> ( ( seq 1 ( x. , F ) ` k ) <_ ( ( 2 x. N ) ^ (π ` k ) ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) ) )
256	255	expcom 116	. . . . 5 |- ( k e. NN -> ( ph -> ( ( seq 1 ( x. , F ) ` k ) <_ ( ( 2 x. N ) ^ (π ` k ) ) -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) ) ) )
257	256	a2d 26	. . . 4 |- ( k e. NN -> ( ( ph -> ( seq 1 ( x. , F ) ` k ) <_ ( ( 2 x. N ) ^ (π ` k ) ) ) -> ( ph -> ( seq 1 ( x. , F ) ` ( k + 1 ) ) <_ ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) ) ) )
258	99, 104, 109, 114, 150, 257	nnind 9329	. . 3 |- ( M e. NN -> ( ph -> ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^ (π ` M ) ) ) )
259	77, 258	mpcom 36	. 2 |- ( ph -> ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^ (π ` M ) ) )
260	83	nn0zd 9777	. . . 4 |- ( ph -> (π ` M ) e. ZZ )
261		cxpexpnn 16129	. . . 4 |- ( ( ( 2 x. N ) e. NN /\ (π ` M ) e. ZZ ) -> ( ( 2 x. N ) ^c (π ` M ) ) = ( ( 2 x. N ) ^ (π ` M ) ) )
262	20, 260, 261	syl2anc 415	. . 3 |- ( ph -> ( ( 2 x. N ) ^c (π ` M ) ) = ( ( 2 x. N ) ^ (π ` M ) ) )
263	83	nn0red 9632	. . . . 5 |- ( ph -> (π ` M ) e. RR )
264	77	nnred 9326	. . . . . . 7 |- ( ph -> M e. RR )
265		nndivre 9349	. . . . . . 7 |- ( ( M e. RR /\ 3 e. NN ) -> ( M / 3 ) e. RR )
266	264, 16, 265	sylancl 417	. . . . . 6 |- ( ph -> ( M / 3 ) e. RR )
267		readdcl 8311	. . . . . 6 |- ( ( ( M / 3 ) e. RR /\ 2 e. RR ) -> ( ( M / 3 ) + 2 ) e. RR )
268	266, 49, 267	sylancl 417	. . . . 5 |- ( ph -> ( ( M / 3 ) + 2 ) e. RR )
269	77	nnnn0d 9631	. . . . . . 7 |- ( ph -> M e. NN0 )
270	269	nn0ge0d 9634	. . . . . 6 |- ( ph -> 0 <_ M )
271		ppiqub 16293	. . . . . 6 |- ( ( M e. QQ /\ 0 <_ M ) -> (π ` M ) <_ ( ( M / 3 ) + 2 ) )
272	81, 270, 271	syl2anc 415	. . . . 5 |- ( ph -> (π ` M ) <_ ( ( M / 3 ) + 2 ) )
273	49	a1i 9	. . . . . 6 |- ( ph -> 2 e. RR )
274		flaplelt 10730	. . . . . . . . . 10 |- ( ( ( sqr ` ( 2 x. N ) ) e. QQ \/ ( ( sqr ` ( 2 x. N ) ) e. RR /\ A. q e. QQ ( sqr ` ( 2 x. N ) ) # q ) ) -> ( ( |_ ` ( sqr ` ( 2 x. N ) ) ) <_ ( sqr ` ( 2 x. N ) ) /\ ( sqr ` ( 2 x. N ) ) < ( ( |_ ` ( sqr ` ( 2 x. N ) ) ) + 1 ) ) )
275	23, 274	syl 14	. . . . . . . . 9 |- ( ph -> ( ( |_ ` ( sqr ` ( 2 x. N ) ) ) <_ ( sqr ` ( 2 x. N ) ) /\ ( sqr ` ( 2 x. N ) ) < ( ( |_ ` ( sqr ` ( 2 x. N ) ) ) + 1 ) ) )
276	275	simpld 112	. . . . . . . 8 |- ( ph -> ( |_ ` ( sqr ` ( 2 x. N ) ) ) <_ ( sqr ` ( 2 x. N ) ) )
277	17, 276	eqbrtrid 4166	. . . . . . 7 |- ( ph -> M <_ ( sqr ` ( 2 x. N ) ) )
278		3re 9387	. . . . . . . . . 10 |- 3 e. RR
279		3pos 9407	. . . . . . . . . 10 |- 0 < 3
280	278, 279	pm3.2i 272	. . . . . . . . 9 |- ( 3 e. RR /\ 0 < 3 )
281	280	a1i 9	. . . . . . . 8 |- ( ph -> ( 3 e. RR /\ 0 < 3 ) )
282		lediv1 9207	. . . . . . . 8 |- ( ( M e. RR /\ ( sqr ` ( 2 x. N ) ) e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( M <_ ( sqr ` ( 2 x. N ) ) <-> ( M / 3 ) <_ ( ( sqr ` ( 2 x. N ) ) / 3 ) ) )
283	264, 86, 281, 282	syl3anc 1278	. . . . . . 7 |- ( ph -> ( M <_ ( sqr ` ( 2 x. N ) ) <-> ( M / 3 ) <_ ( ( sqr ` ( 2 x. N ) ) / 3 ) ) )
284	277, 283	mpbid 147	. . . . . 6 |- ( ph -> ( M / 3 ) <_ ( ( sqr ` ( 2 x. N ) ) / 3 ) )
285	266, 88, 273, 284	leadd1dd 8894	. . . . 5 |- ( ph -> ( ( M / 3 ) + 2 ) <_ ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) )
286	263, 268, 90, 272, 285	letrd 8457	. . . 4 |- ( ph -> (π ` M ) <_ ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) )
287		2t1e2 9467	. . . . . . . 8 |- ( 2 x. 1 ) = 2
288	6	nnge1d 9356	. . . . . . . . 9 |- ( ph -> 1 <_ N )
289		1re 8331	. . . . . . . . . . 11 |- 1 e. RR
290		lemul2 9195	. . . . . . . . . . 11 |- ( ( 1 e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( 1 <_ N <-> ( 2 x. 1 ) <_ ( 2 x. N ) ) )
291	289, 51, 290	mp3an13 1369	. . . . . . . . . 10 |- ( N e. RR -> ( 1 <_ N <-> ( 2 x. 1 ) <_ ( 2 x. N ) ) )
292	47, 291	syl 14	. . . . . . . . 9 |- ( ph -> ( 1 <_ N <-> ( 2 x. 1 ) <_ ( 2 x. N ) ) )
293	288, 292	mpbid 147	. . . . . . . 8 |- ( ph -> ( 2 x. 1 ) <_ ( 2 x. N ) )
294	287, 293	eqbrtrrid 4167	. . . . . . 7 |- ( ph -> 2 <_ ( 2 x. N ) )
295	31	eluz1i 9945	. . . . . . 7 |- ( ( 2 x. N ) e. ( ZZ>= ` 2 ) <-> ( ( 2 x. N ) e. ZZ /\ 2 <_ ( 2 x. N ) ) )
296	34, 294, 295	sylanbrc 421	. . . . . 6 |- ( ph -> ( 2 x. N ) e. ( ZZ>= ` 2 ) )
297		eluz2gt1 10018	. . . . . 6 |- ( ( 2 x. N ) e. ( ZZ>= ` 2 ) -> 1 < ( 2 x. N ) )
298	296, 297	syl 14	. . . . 5 |- ( ph -> 1 < ( 2 x. N ) )
299	35, 298, 263, 90	cxpled 16164	. . . 4 |- ( ph -> ( (π ` M ) <_ ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) <-> ( ( 2 x. N ) ^c (π ` M ) ) <_ ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) ) )
300	286, 299	mpbid 147	. . 3 |- ( ph -> ( ( 2 x. N ) ^c (π ` M ) ) <_ ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) )
301	262, 300	eqbrtrrd 4155	. 2 |- ( ph -> ( ( 2 x. N ) ^ (π ` M ) ) <_ ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) )
302	79, 85, 92, 259, 301	letrd 8457	1 |- ( ph -> ( seq 1 ( x. , F ) ` M ) <_ ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   \/ wo 720  DECID wdc 846   = wceq 1402   e. wcel 2209   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   # cap 8917   / cdiv 9010   NNcn 9313   2c2 9364   3c3 9365   5c5 9367   9c9 9371   NN0cn0 9574   ZZcz 9655  ;cdc 9788   ZZ>=cuz 9937   QQcq 10035   ...cfz 10428   |_cfl 10720   seqcseq 10905   ^cexp 10996   _C cbc 11207   sqrcsqrt 11784   Primecprime 12910   pCnt cpc 13092   ^c ccxp 16086  πcppi 16234

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-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-ppi 16237

This theorem is used by:  bposlem6  16316