Theorem bposlem5 16213

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 9473	. . . . . . . . . . 11 |- 5 e. NN
4		bpos.1	. . . . . . . . . . 11 |- ( ph -> N e. ( ZZ>= ` 5 ) )
5		eluznn 10009	. . . . . . . . . . 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 9624	. . . . . . . . 9 |- ( ph -> N e. NN0 )
8		fzctr 10550	. . . . . . . . 9 |- ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) )
9		bccl2 11220	. . . . . . . . 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 13098	. . . . . . . 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 13141	. . . . 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 9471	. . . . 5 |- 3 e. NN
17		bpos.5	. . . . . 6 |- M = ( |_ ` ( sqr ` ( 2 x. N ) ) )
18		2nn 9470	. . . . . . . . . . 11 |- 2 e. NN
19		nnmulcl 9327	. . . . . . . . . . 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 9624	. . . . . . . . 9 |- ( ph -> ( 2 x. N ) e. NN0 )
22		sqrtrirr 13005	. . . . . . . . 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 10721	. . . . . . . 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 11828	. . . . . . . . 9 |- ( sqr ` 9 ) = 3
27		9re 9393	. . . . . . . . . . . 12 |- 9 e. RR
28	27	a1i 9	. . . . . . . . . . 11 |- ( ph -> 9 e. RR )
29		10re 9803	. . . . . . . . . . . 12 |- ; 1 0 e. RR
30	29	a1i 9	. . . . . . . . . . 11 |- ( ph -> ; 1 0 e. RR )
31		2z 9676	. . . . . . . . . . . . 13 |- 2 e. ZZ
32	6	nnzd 9771	. . . . . . . . . . . . 13 |- ( ph -> N e. ZZ )
33		zmulcl 9702	. . . . . . . . . . . . 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 9772	. . . . . . . . . . 11 |- ( ph -> ( 2 x. N ) e. RR )
36		lep1 9177	. . . . . . . . . . . . . 14 |- ( 9 e. RR -> 9 <_ ( 9 + 1 ) )
37	27, 36	ax-mp 5	. . . . . . . . . . . . 13 |- 9 <_ ( 9 + 1 )
38		9p1e10 9783	. . . . . . . . . . . . 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 9386	. . . . . . . . . . . . 13 |- 5 e. CC
42		2cn 9377	. . . . . . . . . . . . 13 |- 2 e. CC
43		5t2e10 9885	. . . . . . . . . . . . 13 |- ( 5 x. 2 ) = ; 1 0
44	41, 42, 43	mulcomli 8333	. . . . . . . . . . . 12 |- ( 2 x. 5 ) = ; 1 0
45		eluzle 9943	. . . . . . . . . . . . . 14 |- ( N e. ( ZZ>= ` 5 ) -> 5 <_ N )
46	4, 45	syl 14	. . . . . . . . . . . . 13 |- ( ph -> 5 <_ N )
47	6	nnred 9319	. . . . . . . . . . . . . 14 |- ( ph -> N e. RR )
48		5re 9385	. . . . . . . . . . . . . . 15 |- 5 e. RR
49		2re 9376	. . . . . . . . . . . . . . . 16 |- 2 e. RR
50		2pos 9397	. . . . . . . . . . . . . . . 16 |- 0 < 2
51	49, 50	pm3.2i 272	. . . . . . . . . . . . . . 15 |- ( 2 e. RR /\ 0 < 2 )
52		lemul2 9189	. . . . . . . . . . . . . . 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 8451	. . . . . . . . . 10 |- ( ph -> 9 <_ ( 2 x. N ) )
58		0re 8326	. . . . . . . . . . . . 13 |- 0 e. RR
59		9pos 9410	. . . . . . . . . . . . 13 |- 0 < 9
60	58, 27, 59	ltleii 8429	. . . . . . . . . . . 12 |- 0 <_ 9
61	27, 60	pm3.2i 272	. . . . . . . . . . 11 |- ( 9 e. RR /\ 0 <_ 9 )
62	20	nnrpd 10105	. . . . . . . . . . . . 13 |- ( ph -> ( 2 x. N ) e. RR+ )
63	62	rpge0d 10111	. . . . . . . . . . . 12 |- ( ph -> 0 <_ ( 2 x. N ) )
64	35, 63	jca 306	. . . . . . . . . . 11 |- ( ph -> ( ( 2 x. N ) e. RR /\ 0 <_ ( 2 x. N ) ) )
65		sqrtle 11816	. . . . . . . . . . 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 9677	. . . . . . . . 9 |- 3 e. ZZ
70		flapge 10730	. . . . . . . . 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 9938	. . . . . . 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 10009	. . . . 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 9319	. 2 |- ( ph -> ( seq 1 ( x. , F ) ` M ) e. RR )
80		nnq 10042	. . . . . 6 |- ( M e. NN -> M e. QQ )
81	77, 80	syl 14	. . . . 5 |- ( ph -> M e. QQ )
82		ppiqcl 16163	. . . . 5 |- ( M e. QQ -> (π ` M ) e. NN0 )
83	81, 82	syl 14	. . . 4 |- ( ph -> (π ` M ) e. NN0 )
84	20, 83	nnexpcld 11146	. . 3 |- ( ph -> ( ( 2 x. N ) ^ (π ` M ) ) e. NN )
85	84	nnred 9319	. 2 |- ( ph -> ( ( 2 x. N ) ^ (π ` M ) ) e. RR )
86	35, 63	resqrtcld 11944	. . . . . 6 |- ( ph -> ( sqr ` ( 2 x. N ) ) e. RR )
87		nndivre 9342	. . . . . 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 8305	. . . . 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 16088	. . 3 |- ( ph -> ( ( 2 x. N ) ^c ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) ) e. RR+ )
92	91	rpred 10107	. 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 16176	. . . . . . . 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 9675	. . . . . . . 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 9968	. . . . . . . . . . 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 13099	. . . . . . . . . . . 12 |- ( ( ( ph /\ u e. ( ZZ>= ` 1 ) ) /\ u e. Prime ) -> ( u pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
127	123, 126	nnexpcld 11146	. . . . . . . . . . 11 |- ( ( ( ph /\ u e. ( ZZ>= ` 1 ) ) /\ u e. Prime ) -> ( u ^ ( u pCnt ( ( 2 x. N ) _C N ) ) ) e. NN )
128		1nn 9317	. . . . . . . . . . . 12 |- 1 e. NN
129	128	a1i 9	. . . . . . . . . . 11 |- ( ( ( ph /\ u e. ( ZZ>= ` 1 ) ) /\ -. u e. Prime ) -> 1 e. NN )
130		prmdc 12924	. . . . . . . . . . . 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 9327	. . . . . . . . 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 10912	. . . . . . 7 |- ( ph -> ( seq 1 ( x. , F ) ` 1 ) = ( F ` 1 ) )
138		1nprm 12908	. . . . . . . . . . 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 8321	. . . . . . . . 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 8902	. . . . . 6 |- 1 <_ 1
147	145, 146	eqbrtrdi 4169	. . . . 5 |- ( ph -> ( seq 1 ( x. , F ) ` 1 ) <_ 1 )
148	34	zcnd 9773	. . . . . 6 |- ( ph -> ( 2 x. N ) e. CC )
149	148	exp0d 11118	. . . . 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 9319	. . . . . . . . . . 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 10042	. . . . . . . . . . . . . 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 16163	. . . . . . . . . . . . 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 11146	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( 2 x. N ) ^ (π ` k ) ) e. NN )
160	159	nnred 9319	. . . . . . . . . 10 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( 2 x. N ) ^ (π ` k ) ) e. RR )
161		nnre 9313	. . . . . . . . . . . . 13 |- ( ( 2 x. N ) e. NN -> ( 2 x. N ) e. RR )
162		nngt0 9331	. . . . . . . . . . . . 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 8923	. . . . . . . . . 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 9667	. . . . . . . . . . . . . 14 |- ( k e. NN -> k e. ZZ )
169	168	adantl 277	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. NN ) -> k e. ZZ )
170		ppiprm 16170	. . . . . . . . . . . . 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 11125	. . . . . . . . . . 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 9967	. . . . . . . . . . . . 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 10915	. . . . . . . . . . 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 9318	. . . . . . . . . . . . . . 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 13099	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ k e. NN ) /\ ( k + 1 ) e. Prime ) -> ( ( k + 1 ) pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
196	192, 195	nnexpcld 11146	. . . . . . . . . . . . . . 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 12924	. . . . . . . . . . . . . . . 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 16209	. . . . . . . . . . . . 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 9319	. . . . . . . . . . . . 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 9313	. . . . . . . . . . . . . . 15 |- ( ( seq 1 ( x. , F ) ` k ) e. NN -> ( seq 1 ( x. , F ) ` k ) e. RR )
215		nngt0 9331	. . . . . . . . . . . . . . 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 9189	. . . . . . . . . . . 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 9319	. . . . . . . . . . 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 9355	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) e. NN )
228	227	nnred 9319	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( seq 1 ( x. , F ) ` k ) x. ( 2 x. N ) ) e. RR )
229		nnq 10042	. . . . . . . . . . . . . . 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 16163	. . . . . . . . . . . . . 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 11146	. . . . . . . . . . . 12 |- ( ( ph /\ k e. NN ) -> ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) e. NN )
234	233	nnred 9319	. . . . . . . . . . 11 |- ( ( ph /\ k e. NN ) -> ( ( 2 x. N ) ^ (π ` ( k + 1 ) ) ) e. RR )
235		letr 8408	. . . . . . . . . . 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 9320	. . . . . . . . . . 11 |- ( ( ( ph /\ k e. NN ) /\ -. ( k + 1 ) e. Prime ) -> ( seq 1 ( x. , F ) ` k ) e. CC )
246	245	mulridd 8343	. . . . . . . . . 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 16171	. . . . . . . . . . 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 9322	. . 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 9770	. . . 4 |- ( ph -> (π ` M ) e. ZZ )
261		cxpexpnn 16051	. . . 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 9625	. . . . 5 |- ( ph -> (π ` M ) e. RR )
264	77	nnred 9319	. . . . . . 7 |- ( ph -> M e. RR )
265		nndivre 9342	. . . . . . 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 8305	. . . . . 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 9624	. . . . . . 7 |- ( ph -> M e. NN0 )
270	269	nn0ge0d 9627	. . . . . 6 |- ( ph -> 0 <_ M )
271		ppiqub 16194	. . . . . 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 10723	. . . . . . . . . 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 9380	. . . . . . . . . 10 |- 3 e. RR
279		3pos 9400	. . . . . . . . . 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 9201	. . . . . . . 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 8888	. . . . 5 |- ( ph -> ( ( M / 3 ) + 2 ) <_ ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) )
286	263, 268, 90, 272, 285	letrd 8451	. . . 4 |- ( ph -> (π ` M ) <_ ( ( ( sqr ` ( 2 x. N ) ) / 3 ) + 2 ) )
287		2t1e2 9460	. . . . . . . 8 |- ( 2 x. 1 ) = 2
288	6	nnge1d 9349	. . . . . . . . 9 |- ( ph -> 1 <_ N )
289		1re 8325	. . . . . . . . . . 11 |- 1 e. RR
290		lemul2 9189	. . . . . . . . . . 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 9938	. . . . . . 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 10011	. . . . . 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 16084	. . . 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 8451	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 8177   RRcr 8178   0cc0 8179   1c1 8180   + caddc 8182   x. cmul 8184   < clt 8360   <_ cle 8361   # cap 8911   / cdiv 9004   NNcn 9306   2c2 9357   3c3 9358   5c5 9360   9c9 9364   NN0cn0 9567   ZZcz 9648  ;cdc 9781   ZZ>=cuz 9930   QQcq 10028   ...cfz 10421   |_cfl 10713   seqcseq 10897   ^cexp 10988   _C cbc 11199   sqrcsqrt 11776   Primecprime 12901   pCnt cpc 13083   ^c ccxp 16008  πcppi 16152

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 8270  ax-resscn 8271  ax-1cn 8272  ax-1re 8273  ax-icn 8274  ax-addcl 8275  ax-addrcl 8276  ax-mulcl 8277  ax-mulrcl 8278  ax-addcom 8279  ax-mulcom 8280  ax-addass 8281  ax-mulass 8282  ax-distr 8283  ax-i2m1 8284  ax-0lt1 8285  ax-1rid 8286  ax-0id 8287  ax-rnegex 8288  ax-precex 8289  ax-cnre 8290  ax-pre-ltirr 8291  ax-pre-ltwlin 8292  ax-pre-lttrn 8293  ax-pre-apti 8294  ax-pre-ltadd 8295  ax-pre-mulgt0 8296  ax-pre-mulext 8297  ax-arch 8298  ax-caucvg 8299  ax-pre-suploc 8300  ax-addf 8301  ax-mulf 8302

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 7324  df-inf 7325  df-pnf 8362  df-mnf 8363  df-xr 8364  df-ltxr 8365  df-le 8366  df-sub 8500  df-neg 8501  df-reap 8905  df-ap 8912  df-div 9005  df-inn 9307  df-2 9365  df-3 9366  df-4 9367  df-5 9368  df-6 9369  df-7 9370  df-8 9371  df-9 9372  df-n0 9568  df-z 9649  df-dec 9782  df-uz 9931  df-q 10029  df-rp 10065  df-xneg 10184  df-xadd 10185  df-ioo 10304  df-ico 10306  df-icc 10307  df-fz 10422  df-fzo 10560  df-fl 10715  df-mod 10773  df-seqfrec 10898  df-exp 10989  df-fac 11178  df-bc 11200  df-ihash 11229  df-shft 11594  df-cj 11621  df-re 11622  df-im 11623  df-rsqrt 11778  df-abs 11779  df-clim 12061  df-sumdc 12136  df-ef 12431  df-e 12432  df-dvds 12571  df-gcd 12747  df-prm 12902  df-numer 12979  df-denom 12980  df-pc 13084  df-rest 13644  df-topgen 13663  df-psmet 14929  df-xmet 14930  df-met 14931  df-bl 14932  df-mopn 14933  df-top 15148  df-topon 15161  df-bases 15193  df-ntr 15246  df-cn 15338  df-cnp 15339  df-tx 15403  df-cncf 15721  df-limced 15806  df-dvap 15807  df-relog 16009  df-rpcxp 16010  df-logb 16099  df-ppi 16154

This theorem is used by: (None)