Theorem bposlem5 16276

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 9474	. . . . . . . . . . 11 |- 5 e. NN
4		bpos.1	. . . . . . . . . . 11 |- ( ph -> N e. ( ZZ>= ` 5 ) )
5		eluznn 10010	. . . . . . . . . . 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 9625	. . . . . . . . 9 |- ( ph -> N e. NN0 )
8		fzctr 10551	. . . . . . . . 9 |- ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) )
9		bccl2 11222	. . . . . . . . 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 13101	. . . . . . . 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 13144	. . . . 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 9472	. . . . 5 |- 3 e. NN
17		bpos.5	. . . . . 6 |- M = ( |_ ` ( sqr ` ( 2 x. N ) ) )
18		2nn 9471	. . . . . . . . . . 11 |- 2 e. NN
19		nnmulcl 9328	. . . . . . . . . . 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 9625	. . . . . . . . 9 |- ( ph -> ( 2 x. N ) e. NN0 )
22		sqrtrirr 13008	. . . . . . . . 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 10722	. . . . . . . 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 11830	. . . . . . . . 9 |- ( sqr ` 9 ) = 3
27		9re 9394	. . . . . . . . . . . 12 |- 9 e. RR
28	27	a1i 9	. . . . . . . . . . 11 |- ( ph -> 9 e. RR )
29		10re 9804	. . . . . . . . . . . 12 |- ; 1 0 e. RR
30	29	a1i 9	. . . . . . . . . . 11 |- ( ph -> ; 1 0 e. RR )
31		2z 9677	. . . . . . . . . . . . 13 |- 2 e. ZZ
32	6	nnzd 9772	. . . . . . . . . . . . 13 |- ( ph -> N e. ZZ )
33		zmulcl 9703	. . . . . . . . . . . . 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 9773	. . . . . . . . . . 11 |- ( ph -> ( 2 x. N ) e. RR )
36		lep1 9178	. . . . . . . . . . . . . 14 |- ( 9 e. RR -> 9 <_ ( 9 + 1 ) )
37	27, 36	ax-mp 5	. . . . . . . . . . . . 13 |- 9 <_ ( 9 + 1 )
38		9p1e10 9784	. . . . . . . . . . . . 13 |- ( 9 + 1 ) = ; 1 0
39	37, 38	breqtri 4155	. . . . . . . . . . . 12 |- 9 <_ ; 1 0
40	39	a1i 9	. . . . . . . . . . 11 |- ( ph -> 9 <_ ; 1 0 )
41		5cn 9387	. . . . . . . . . . . . 13 |- 5 e. CC
42		2cn 9378	. . . . . . . . . . . . 13 |- 2 e. CC
43		5t2e10 9886	. . . . . . . . . . . . 13 |- ( 5 x. 2 ) = ; 1 0
44	41, 42, 43	mulcomli 8334	. . . . . . . . . . . 12 |- ( 2 x. 5 ) = ; 1 0
45		eluzle 9944	. . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` 5 ) -> 5 <_ N )
46	4, 45	syl 14	. . . . . . . . . . . . 13 |- ( ph -> 5 <_ N )
47	6	nnred 9320	. . . . . . . . . . . . . 14 |- ( ph -> N e. RR )
48		5re 9386	. . . . . . . . . . . . . . 15 |- 5 e. RR
49		2re 9377	. . . . . . . . . . . . . . . 16 |- 2 e. RR
50		2pos 9398	. . . . . . . . . . . . . . . 16 |- 0 < 2
51	49, 50	pm3.2i 272	. . . . . . . . . . . . . . 15 |- ( 2 e. RR /\ 0 < 2 )
52		lemul2 9190	. . . . . . . . . . . . . . 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 4166	. . . . . . . . . . 11 |- ( ph -> ; 1 0 <_ ( 2 x. N ) )
57	28, 30, 35, 40, 56	letrd 8452	. . . . . . . . . 10 |- ( ph -> 9 <_ ( 2 x. N ) )
58		0re 8327	. . . . . . . . . . . . 13 |- 0 e. RR
59		9pos 9411	. . . . . . . . . . . . 13 |- 0 < 9
60	58, 27, 59	ltleii 8430	. . . . . . . . . . . 12 |- 0 <_ 9
61	27, 60	pm3.2i 272	. . . . . . . . . . 11 |- ( 9 e. RR /\ 0 <_ 9 )
62	20	nnrpd 10106	. . . . . . . . . . . . 13 |- ( ph -> ( 2 x. N ) e. RR+ )
63	62	rpge0d 10112	. . . . . . . . . . . 12 |- ( ph -> 0 <_ ( 2 x. N ) )
64	35, 63	jca 306	. . . . . . . . . . 11 |- ( ph -> ( ( 2 x. N ) e. RR /\ 0 <_ ( 2 x. N ) ) )
65		sqrtle 11818	. . . . . . . . . . 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 4166	. . . . . . . 8 |- ( ph -> 3 <_ ( sqr ` ( 2 x. N ) ) )
69		3z 9678	. . . . . . . . 9 |- 3 e. ZZ
70		flapge 10731	. . . . . . . . 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 9939	. . . . . . 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 10010	. . . . 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 5844	. . 3 |- ( ph -> ( seq 1 ( x. , F ) ` M ) e. NN )
79	78	nnred 9320	. 2 |- ( ph -> ( seq 1 ( x. , F ) ` M ) e. RR )
80		nnq 10043	. . . . . 6 |- ( M e. NN -> M e. QQ )
81	77, 80	syl 14	. . . . 5 |- ( ph -> M e. QQ )
82		ppiqcl 16212	. . . . 5 |- ( M e. QQ -> (π ` M ) e. NN0 )
83	81, 82	syl 14	. . . 4 |- ( ph -> (π ` M ) e. NN0 )
84	20, 83	nnexpcld 11148	. . 3 |- ( ph -> ( ( 2 x. N ) ^ (π ` M ) ) e. NN )
85	84	nnred 9320	. 2 |- ( ph -> ( ( 2 x. N ) ^ (π ` M ) ) e. RR )
86	35, 63	resqrtcld 11946	. . . . . 6 |- ( ph -> ( sqr ` ( 2 x. N ) ) e. RR )
87		nndivre 9343	. . . . . 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 8306	. . . . 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 16130	. . 3 |- ( ph -> ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) e. RR+ )
92	91	rpred 10108	. 2 |- ( ph -> ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) e. RR )
93		fveq2 5695	. . . . . 6 |- ( x = 1 -> ( seq 1 ( x. , F ) ` x ) = ( seq 1 ( x. , F ) ` 1 ) )
94		fveq2 5695	. . . . . . . 8 |- ( x = 1 -> (π ` x ) = (π ` 1 ) )
95		ppi1 16231	. . . . . . . 8 |- (π ` 1 ) = 0
96	94, 95	eqtrdi 2287	. . . . . . 7 |- ( x = 1 -> (π ` x ) = 0 )
97	96	oveq2d 6101	. . . . . 6 |- ( x = 1 -> ( ( 2 x. N ) ^ (π ` x ) ) = ( ( 2 x. N ) ^ 0 ) )
98	93, 97	breq12d 4143	. . . . 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 5695	. . . . . 6 |- ( x = k -> ( seq 1 ( x. , F ) ` x ) = ( seq 1 ( x. , F ) ` k ) )
101		fveq2 5695	. . . . . . 7 |- ( x = k -> (π ` x ) = (π ` k ) )
102	101	oveq2d 6101	. . . . . 6 |- ( x = k -> ( ( 2 x. N ) ^ (π ` x ) ) = ( ( 2 x. N ) ^ (π ` k ) ) )
103	100, 102	breq12d 4143	. . . . 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 5695	. . . . . 6 |- ( x = ( k + 1 ) -> ( seq 1 ( x. , F ) ` x ) = ( seq 1 ( x. , F ) ` ( k + 1 ) ) )
106		fveq2 5695	. . . . . . 7 |- ( x = ( k + 1 ) -> (π ` x ) = (π ` ( k + 1 ) ) )
107	106	oveq2d 6101	. . . . . 6 |- ( x = ( k + 1 ) -> ( ( 2 x. N ) ^ (π ` x ) ) = ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) )
108	105, 107	breq12d 4143	. . . . 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 5695	. . . . . 6 |- ( x = M -> ( seq 1 ( x. , F ) ` x ) = ( seq 1 ( x. , F ) ` M ) )
111		fveq2 5695	. . . . . . 7 |- ( x = M -> (π ` x ) = (π ` M ) )
112	111	oveq2d 6101	. . . . . 6 |- ( x = M -> ( ( 2 x. N ) ^ (π ` x ) ) = ( ( 2 x. N ) ^ (π ` M ) ) )
113	110, 112	breq12d 4143	. . . . 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 9676	. . . . . . . 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 6092	. . . . . . . . . . . 12 |- ( n = u -> ( n pCnt ( ( 2 x. N ) _C N ) ) = ( u pCnt ( ( 2 x. N ) _C N ) ) )
119	117, 118	oveq12d 6103	. . . . . . . . . . 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 9969	. . . . . . . . . . 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 13102	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. ( ZZ>= ` 1 ) ) /\ u e. Prime ) -> ( u pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
127	123, 126	nnexpcld 11148	. . . . . . . . . . 11 |- ( ( ( ph /\ u e. ( ZZ>= ` 1 ) ) /\ u e. Prime ) -> ( u ^ ( u pCnt ( ( 2 x. N ) _C N ) ) ) e. NN )
128		1nn 9318	. . . . . . . . . . . 12 |- 1 e. NN
129	128	a1i 9	. . . . . . . . . . 11 |- ( ( ( ph /\ u e. ( ZZ>= ` 1 ) ) /\ -. u e. Prime ) -> 1 e. NN )
130		prmdc 12927	. . . . . . . . . . . 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 5799	. . . . . . . . 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 9328	. . . . . . . . 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 10914	. . . . . . 7 |- ( ph -> ( seq 1 ( x. , F ) ` 1 ) = ( F ` 1 ) )
138		1nprm 12911	. . . . . . . . . . 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 8322	. . . . . . . . 9 |- 1 e. _V
143	141, 1, 142	fvmpt 5782	. . . . . . . 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 8903	. . . . . 6 |- 1 <_ 1
147	145, 146	eqbrtrdi 4169	. . . . 5 |- ( ph -> ( seq 1 ( x. , F ) ` 1 ) <_ 1 )
148	34	zcnd 9774	. . . . . 6 |- ( ph -> ( 2 x. N ) e. CC )
149	148	exp0d 11120	. . . . 5 |- ( ph -> ( ( 2 x. N ) ^ 0 ) = 1 )
150	147, 149	breqtrrd 4158	. . . 4 |- ( ph -> ( seq 1 ( x. , F ) ` 1 ) <_ ( ( 2 x. N ) ^ 0 ) )
151	15	ffvelcdmda 5843	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( seq 1 ( x. , F ) ` k ) e. NN )
152	151	nnred 9320	. . . . . . . . . . 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 10043	. . . . . . . . . . . . . 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 16212	. . . . . . . . . . . . 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 11148	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( 2 x. N ) ^ (π ` k ) ) e. NN )
160	159	nnred 9320	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( 2 x. N ) ^ (π ` k ) ) e. RR )
161		nnre 9314	. . . . . . . . . . . . 13 |- ( ( 2 x. N ) e. NN -> ( 2 x. N ) e. RR )
162		nngt0 9332	. . . . . . . . . . . . 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 8924	. . . . . . . . . 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 9668	. . . . . . . . . . . . . 14 |- ( k e. NN -> k e. ZZ )
169	168	adantl 277	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> k e. ZZ )
170		ppiprm 16220	. . . . . . . . . . . . 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 6101	. . . . . . . . . . 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 11127	. . . . . . . . . . 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 4142	. . . . . . . . 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 9968	. . . . . . . . . . . . 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 10917	. . . . . . . . . . 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 6092	. . . . . . . . . . . . . . . 16 |- ( n = ( k + 1 ) -> ( n pCnt ( ( 2 x. N ) _C N ) ) = ( ( k + 1 ) pCnt ( ( 2 x. N ) _C N ) ) )
188	186, 187	oveq12d 6103	. . . . . . . . . . . . . . 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 9319	. . . . . . . . . . . . . . 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 13102	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( k + 1 ) pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
196	192, 195	nnexpcld 11148	. . . . . . . . . . . . . . 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 12927	. . . . . . . . . . . . . . . 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 5799	. . . . . . . . . . . . 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 16272	. . . . . . . . . . . . 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 4152	. . . . . . . . . . 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 5841	. . . . . . . . . . . . . . 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 9320	. . . . . . . . . . . . 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 9314	. . . . . . . . . . . . . . 15 |- ( ( seq 1 ( x. , F ) ` k ) e. NN -> ( seq 1 ( x. , F ) ` k ) e. RR )
215		nngt0 9332	. . . . . . . . . . . . . . 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 9190	. . . . . . . . . . . 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 4152	. . . . . . . . 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 5841	. . . . . . . . . . . . 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 9320	. . . . . . . . . . 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 9356	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) e. NN )
228	227	nnred 9320	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) e. RR )
229		nnq 10043	. . . . . . . . . . . . . . 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 16212	. . . . . . . . . . . . . 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 11148	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) e. NN )
234	233	nnred 9320	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) e. RR )
235		letr 8409	. . . . . . . . . . 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 6101	. . . . . . . . . 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 9321	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. NN ) /\ -. ( k + 1 ) e. Prime ) -> ( seq 1 ( x. , F ) ` k ) e. CC )
246	245	mulridd 8344	. . . . . . . . . 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 16221	. . . . . . . . . . 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 6101	. . . . . . . . 9 |- ( ( ( ph /\ k e. NN ) /\ -. ( k + 1 ) e. Prime ) -> ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) = ( ( 2 x. N ) ^ (π ` k ) ) )
251	247, 250	breq12d 4143	. . . . . . . 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 9323	. . 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 9771	. . . 4 |- ( ph -> (π ` M ) e. ZZ )
261		cxpexpnn 16093	. . . 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 9626	. . . . 5 |- ( ph -> (π ` M ) e. RR )
264	77	nnred 9320	. . . . . . 7 |- ( ph -> M e. RR )
265		nndivre 9343	. . . . . . 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 8306	. . . . . 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 9625	. . . . . . 7 |- ( ph -> M e. NN0 )
270	269	nn0ge0d 9628	. . . . . 6 |- ( ph -> 0 <_ M )
271		ppiqub 16254	. . . . . 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 10724	. . . . . . . . . 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 4165	. . . . . . 7 |- ( ph -> M <_ ( sqr ` ( 2 x. N ) ) )
278		3re 9381	. . . . . . . . . 10 |- 3 e. RR
279		3pos 9401	. . . . . . . . . 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 9202	. . . . . . . 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 8889	. . . . 5 |- ( ph -> ( ( M / 3 ) + 2 ) <_ ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) )
286	263, 268, 90, 272, 285	letrd 8452	. . . 4 |- ( ph -> (π ` M ) <_ ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) )
287		2t1e2 9461	. . . . . . . 8 |- ( 2 x. 1 ) = 2
288	6	nnge1d 9350	. . . . . . . . 9 |- ( ph -> 1 <_ N )
289		1re 8326	. . . . . . . . . . 11 |- 1 e. RR
290		lemul2 9190	. . . . . . . . . . 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 4166	. . . . . . 7 |- ( ph -> 2 <_ ( 2 x. N ) )
295	31	eluz1i 9939	. . . . . . 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 10012	. . . . . 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 16126	. . . 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 4154	. 2 |- ( ph -> ( ( 2 x. N ) ^ (π ` M ) ) <_ ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) )
302	79, 85, 92, 259, 301	letrd 8452	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 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   # cap 8912   / cdiv 9005   NNcn 9307   2c2 9358   3c3 9359   5c5 9361   9c9 9365   NN0cn0 9568   ZZcz 9649  ;cdc 9782   ZZ>=cuz 9931   QQcq 10029   ...cfz 10422   |_cfl 10714   seqcseq 10899   ^cexp 10990   _C cbc 11201   sqrcsqrt 11778   Primecprime 12904   pCnt cpc 13086   ^c ccxp 16050  πcppi 16195

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-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 13648  df-topgen 13667  df-psmet 14964  df-xmet 14965  df-met 14966  df-bl 14967  df-mopn 14968  df-top 15190  df-topon 15203  df-bases 15235  df-ntr 15288  df-cn 15380  df-cnp 15381  df-tx 15445  df-cncf 15763  df-limced 15848  df-dvap 15849  df-relog 16051  df-rpcxp 16052  df-logb 16141  df-ppi 16198

This theorem is used by:  bposlem6  16277