Theorem bposlem1 16311

Description: An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014.)

Assertion

Ref	Expression
bposlem1	|- ( ( N e. NN /\ P e. Prime ) -> ( P ^ ( P pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )

Proof of Theorem bposlem1

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

Step	Hyp	Ref	Expression
1		1zzd 9682	. . . . 5 |- ( ( N e. NN /\ P e. Prime ) -> 1 e. ZZ )
2		2z 9683	. . . . . . 7 |- 2 e. ZZ
3	2	a1i 9	. . . . . 6 |- ( ( N e. NN /\ P e. Prime ) -> 2 e. ZZ )
4		nnz 9674	. . . . . . 7 |- ( N e. NN -> N e. ZZ )
5	4	adantr 276	. . . . . 6 |- ( ( N e. NN /\ P e. Prime ) -> N e. ZZ )
6	3, 5	zmulcld 9785	. . . . 5 |- ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. ZZ )
7	1, 6	fzfigd 10889	. . . 4 |- ( ( N e. NN /\ P e. Prime ) -> ( 1 ... ( 2 x. N ) ) e. Fin )
8	6	adantr 276	. . . . . . . 8 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. N ) e. ZZ )
9		prmnn 12913	. . . . . . . . . 10 |- ( P e. Prime -> P e. NN )
10	9	ad2antlr 493	. . . . . . . . 9 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> P e. NN )
11		elfznn 10477	. . . . . . . . . . 11 |- ( k e. ( 1 ... ( 2 x. N ) ) -> k e. NN )
12	11	adantl 277	. . . . . . . . . 10 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> k e. NN )
13	12	nnnn0d 9631	. . . . . . . . 9 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> k e. NN0 )
14	10, 13	nnexpcld 11154	. . . . . . . 8 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( P ^ k ) e. NN )
15		znq 10040	. . . . . . . 8 |- ( ( ( 2 x. N ) e. ZZ /\ ( P ^ k ) e. NN ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. QQ )
16	8, 14, 15	syl2anc 415	. . . . . . 7 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. QQ )
17	16	flqcld 10731	. . . . . 6 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) e. ZZ )
18		simpll 531	. . . . . . . . . 10 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> N e. NN )
19	18	nnzd 9778	. . . . . . . . 9 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> N e. ZZ )
20		znq 10040	. . . . . . . . 9 |- ( ( N e. ZZ /\ ( P ^ k ) e. NN ) -> ( N / ( P ^ k ) ) e. QQ )
21	19, 14, 20	syl2anc 415	. . . . . . . 8 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( N / ( P ^ k ) ) e. QQ )
22	21	flqcld 10731	. . . . . . 7 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( N / ( P ^ k ) ) ) e. ZZ )
23		zmulcl 9709	. . . . . . 7 |- ( ( 2 e. ZZ /\ ( |_ ` ( N / ( P ^ k ) ) ) e. ZZ ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) e. ZZ )
24	2, 22, 23	sylancr 418	. . . . . 6 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) e. ZZ )
25	17, 24	zsubcld 9784	. . . . 5 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) e. ZZ )
26	25	zred 9779	. . . 4 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) e. RR )
27		1red 8347	. . . . 5 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 1 e. RR )
28		0red 8333	. . . . 5 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 0 e. RR )
29	12	nnzd 9778	. . . . . 6 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> k e. ZZ )
30		1zzd 9682	. . . . . 6 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 1 e. ZZ )
31		2nn 9477	. . . . . . . . . . . 12 |- 2 e. NN
32		nnmulcl 9334	. . . . . . . . . . . 12 |- ( ( 2 e. NN /\ N e. NN ) -> ( 2 x. N ) e. NN )
33	31, 32	mpan 428	. . . . . . . . . . 11 |- ( N e. NN -> ( 2 x. N ) e. NN )
34	33	adantr 276	. . . . . . . . . 10 |- ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. NN )
35		simpr 110	. . . . . . . . . 10 |- ( ( N e. NN /\ P e. Prime ) -> P e. Prime )
36		zprmlogbap 16218	. . . . . . . . . 10 |- ( ( ( 2 x. N ) e. NN /\ P e. Prime ) -> ( ( P logb ( 2 x. N ) ) e. QQ \/ ( ( P logb ( 2 x. N ) ) e. RR /\ A. q e. QQ ( P logb ( 2 x. N ) ) # q ) ) )
37	34, 35, 36	syl2anc 415	. . . . . . . . 9 |- ( ( N e. NN /\ P e. Prime ) -> ( ( P logb ( 2 x. N ) ) e. QQ \/ ( ( P logb ( 2 x. N ) ) e. RR /\ A. q e. QQ ( P logb ( 2 x. N ) ) # q ) ) )
38		prmuz2 12935	. . . . . . . . . . . . 13 |- ( P e. Prime -> P e. ( ZZ>= ` 2 ) )
39	38	adantl 277	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> P e. ( ZZ>= ` 2 ) )
40	34	nnrpd 10112	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. RR+ )
41		relogbval 16187	. . . . . . . . . . . 12 |- ( ( P e. ( ZZ>= ` 2 ) /\ ( 2 x. N ) e. RR+ ) -> ( P logb ( 2 x. N ) ) = ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) )
42	39, 40, 41	syl2anc 415	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> ( P logb ( 2 x. N ) ) = ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) )
43	42	eleq1d 2307	. . . . . . . . . 10 |- ( ( N e. NN /\ P e. Prime ) -> ( ( P logb ( 2 x. N ) ) e. QQ <-> ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. QQ ) )
44	42	eleq1d 2307	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> ( ( P logb ( 2 x. N ) ) e. RR <-> ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. RR ) )
45	42	breq1d 4141	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> ( ( P logb ( 2 x. N ) ) # q <-> ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) # q ) )
46	45	ralbidv 2550	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> ( A. q e. QQ ( P logb ( 2 x. N ) ) # q <-> A. q e. QQ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) # q ) )
47	44, 46	anbi12d 477	. . . . . . . . . 10 |- ( ( N e. NN /\ P e. Prime ) -> ( ( ( P logb ( 2 x. N ) ) e. RR /\ A. q e. QQ ( P logb ( 2 x. N ) ) # q ) <-> ( ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. RR /\ A. q e. QQ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) # q ) ) )
48	43, 47	orbi12d 805	. . . . . . . . 9 |- ( ( N e. NN /\ P e. Prime ) -> ( ( ( P logb ( 2 x. N ) ) e. QQ \/ ( ( P logb ( 2 x. N ) ) e. RR /\ A. q e. QQ ( P logb ( 2 x. N ) ) # q ) ) <-> ( ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. QQ \/ ( ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. RR /\ A. q e. QQ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) # q ) ) ) )
49	37, 48	mpbid 147	. . . . . . . 8 |- ( ( N e. NN /\ P e. Prime ) -> ( ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. QQ \/ ( ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. RR /\ A. q e. QQ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) # q ) ) )
50		flapcl 10728	. . . . . . . 8 |- ( ( ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. QQ \/ ( ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. RR /\ A. q e. QQ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) # q ) ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. ZZ )
51	49, 50	syl 14	. . . . . . 7 |- ( ( N e. NN /\ P e. Prime ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. ZZ )
52	51	adantr 276	. . . . . 6 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. ZZ )
53		fzdcel 10461	. . . . . 6 |- ( ( k e. ZZ /\ 1 e. ZZ /\ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. ZZ ) -> DECID k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
54	29, 30, 52, 53	syl3anc 1278	. . . . 5 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> DECID k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
55	27, 28, 54	ifcldcd 3678	. . . 4 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) e. RR )
56	33	ad2antrr 492	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. N ) e. NN )
57		nnrp 10081	. . . . . . . . . . . . 13 |- ( ( 2 x. N ) e. NN -> ( 2 x. N ) e. RR+ )
58		nnrp 10081	. . . . . . . . . . . . 13 |- ( ( P ^ k ) e. NN -> ( P ^ k ) e. RR+ )
59		rpdivcl 10097	. . . . . . . . . . . . 13 |- ( ( ( 2 x. N ) e. RR+ /\ ( P ^ k ) e. RR+ ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. RR+ )
60	57, 58, 59	syl2an 289	. . . . . . . . . . . 12 |- ( ( ( 2 x. N ) e. NN /\ ( P ^ k ) e. NN ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. RR+ )
61	56, 14, 60	syl2anc 415	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. RR+ )
62	61	rpred 10114	. . . . . . . . . 10 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. RR )
63	24	zred 9779	. . . . . . . . . 10 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) e. RR )
64	62, 63	resubcld 8715	. . . . . . . . 9 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) e. RR )
65		2re 9383	. . . . . . . . . 10 |- 2 e. RR
66	65	a1i 9	. . . . . . . . 9 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 2 e. RR )
67	17	zred 9779	. . . . . . . . . 10 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) e. RR )
68		flqle 10732	. . . . . . . . . . 11 |- ( ( ( 2 x. N ) / ( P ^ k ) ) e. QQ -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) <_ ( ( 2 x. N ) / ( P ^ k ) ) )
69	16, 68	syl 14	. . . . . . . . . 10 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) <_ ( ( 2 x. N ) / ( P ^ k ) ) )
70	67, 62, 63, 69	lesub1dd 8896	. . . . . . . . 9 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ ( ( ( 2 x. N ) / ( P ^ k ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
71		nnrp 10081	. . . . . . . . . . . . . . . 16 |- ( N e. NN -> N e. RR+ )
72		rpdivcl 10097	. . . . . . . . . . . . . . . 16 |- ( ( N e. RR+ /\ ( P ^ k ) e. RR+ ) -> ( N / ( P ^ k ) ) e. RR+ )
73	71, 58, 72	syl2an 289	. . . . . . . . . . . . . . 15 |- ( ( N e. NN /\ ( P ^ k ) e. NN ) -> ( N / ( P ^ k ) ) e. RR+ )
74	18, 14, 73	syl2anc 415	. . . . . . . . . . . . . 14 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( N / ( P ^ k ) ) e. RR+ )
75	74	rpred 10114	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( N / ( P ^ k ) ) e. RR )
76		1re 8331	. . . . . . . . . . . . 13 |- 1 e. RR
77		resubcl 8597	. . . . . . . . . . . . 13 |- ( ( ( N / ( P ^ k ) ) e. RR /\ 1 e. RR ) -> ( ( N / ( P ^ k ) ) - 1 ) e. RR )
78	75, 76, 77	sylancl 417	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( N / ( P ^ k ) ) - 1 ) e. RR )
79		remulcl 8313	. . . . . . . . . . . 12 |- ( ( 2 e. RR /\ ( ( N / ( P ^ k ) ) - 1 ) e. RR ) -> ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) e. RR )
80	65, 78, 79	sylancr 418	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) e. RR )
81		flqltp1 10733	. . . . . . . . . . . . . 14 |- ( ( N / ( P ^ k ) ) e. QQ -> ( N / ( P ^ k ) ) < ( ( |_ ` ( N / ( P ^ k ) ) ) + 1 ) )
82	21, 81	syl 14	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( N / ( P ^ k ) ) < ( ( |_ ` ( N / ( P ^ k ) ) ) + 1 ) )
83	22	zred 9779	. . . . . . . . . . . . . 14 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( N / ( P ^ k ) ) ) e. RR )
84	75, 27, 83	ltsubaddd 8876	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( N / ( P ^ k ) ) - 1 ) < ( |_ ` ( N / ( P ^ k ) ) ) <-> ( N / ( P ^ k ) ) < ( ( |_ ` ( N / ( P ^ k ) ) ) + 1 ) ) )
85	82, 84	mpbird 167	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( N / ( P ^ k ) ) - 1 ) < ( |_ ` ( N / ( P ^ k ) ) ) )
86		2pos 9404	. . . . . . . . . . . . . . 15 |- 0 < 2
87	65, 86	pm3.2i 272	. . . . . . . . . . . . . 14 |- ( 2 e. RR /\ 0 < 2 )
88		ltmul2 9194	. . . . . . . . . . . . . 14 |- ( ( ( ( N / ( P ^ k ) ) - 1 ) e. RR /\ ( |_ ` ( N / ( P ^ k ) ) ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( N / ( P ^ k ) ) - 1 ) < ( |_ ` ( N / ( P ^ k ) ) ) <-> ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) < ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
89	87, 88	mp3an3 1367	. . . . . . . . . . . . 13 |- ( ( ( ( N / ( P ^ k ) ) - 1 ) e. RR /\ ( |_ ` ( N / ( P ^ k ) ) ) e. RR ) -> ( ( ( N / ( P ^ k ) ) - 1 ) < ( |_ ` ( N / ( P ^ k ) ) ) <-> ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) < ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
90	78, 83, 89	syl2anc 415	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( N / ( P ^ k ) ) - 1 ) < ( |_ ` ( N / ( P ^ k ) ) ) <-> ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) < ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
91	85, 90	mpbid 147	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) < ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) )
92	80, 63, 62, 91	ltsub2dd 8893	. . . . . . . . . 10 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) < ( ( ( 2 x. N ) / ( P ^ k ) ) - ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) ) )
93		2cnd 9386	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 2 e. CC )
94		nncn 9321	. . . . . . . . . . . . . 14 |- ( N e. NN -> N e. CC )
95	94	ad2antrr 492	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> N e. CC )
96	14	nncnd 9327	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( P ^ k ) e. CC )
97	14	nnap0d 9359	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( P ^ k ) # 0 )
98	93, 95, 96, 97	divassapd 9164	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) = ( 2 x. ( N / ( P ^ k ) ) ) )
99	75	recnd 8360	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( N / ( P ^ k ) ) e. CC )
100	93, 99	muls1d 8752	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) = ( ( 2 x. ( N / ( P ^ k ) ) ) - 2 ) )
101	98, 100	oveq12d 6106	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) - ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) ) = ( ( 2 x. ( N / ( P ^ k ) ) ) - ( ( 2 x. ( N / ( P ^ k ) ) ) - 2 ) ) )
102		remulcl 8313	. . . . . . . . . . . . . 14 |- ( ( 2 e. RR /\ ( N / ( P ^ k ) ) e. RR ) -> ( 2 x. ( N / ( P ^ k ) ) ) e. RR )
103	65, 75, 102	sylancr 418	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( N / ( P ^ k ) ) ) e. RR )
104	103	recnd 8360	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( N / ( P ^ k ) ) ) e. CC )
105		2cn 9384	. . . . . . . . . . . 12 |- 2 e. CC
106		nncan 8562	. . . . . . . . . . . 12 |- ( ( ( 2 x. ( N / ( P ^ k ) ) ) e. CC /\ 2 e. CC ) -> ( ( 2 x. ( N / ( P ^ k ) ) ) - ( ( 2 x. ( N / ( P ^ k ) ) ) - 2 ) ) = 2 )
107	104, 105, 106	sylancl 417	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. ( N / ( P ^ k ) ) ) - ( ( 2 x. ( N / ( P ^ k ) ) ) - 2 ) ) = 2 )
108	101, 107	eqtrd 2271	. . . . . . . . . 10 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) - ( 2 x. ( ( N / ( P ^ k ) ) - 1 ) ) ) = 2 )
109	92, 108	breqtrd 4157	. . . . . . . . 9 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) < 2 )
110	26, 64, 66, 70, 109	lelttrd 8458	. . . . . . . 8 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) < 2 )
111		df-2 9372	. . . . . . . 8 |- 2 = ( 1 + 1 )
112	110, 111	breqtrdi 4172	. . . . . . 7 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) < ( 1 + 1 ) )
113		1z 9681	. . . . . . . 8 |- 1 e. ZZ
114		zleltp1 9711	. . . . . . . 8 |- ( ( ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) e. ZZ /\ 1 e. ZZ ) -> ( ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ 1 <-> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) < ( 1 + 1 ) ) )
115	25, 113, 114	sylancl 417	. . . . . . 7 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ 1 <-> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) < ( 1 + 1 ) ) )
116	112, 115	mpbird 167	. . . . . 6 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ 1 )
117		iftrue 3645	. . . . . . 7 |- ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) = 1 )
118	117	breq2d 4143	. . . . . 6 |- ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> ( ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) <-> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ 1 ) )
119	116, 118	syl5ibrcom 157	. . . . 5 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) ) )
120	12	nnge1d 9356	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 1 <_ k )
121	120	biantrurd 305	. . . . . . . . . 10 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( k <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) <-> ( 1 <_ k /\ k <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) )
122	35	adantr 276	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> P e. Prime )
123		elfzelz 10445	. . . . . . . . . . . 12 |- ( k e. ( 1 ... ( 2 x. N ) ) -> k e. ZZ )
124	123	adantl 277	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> k e. ZZ )
125		prmefexple 16308	. . . . . . . . . . 11 |- ( ( P e. Prime /\ k e. ZZ /\ ( 2 x. N ) e. NN ) -> ( ( P ^ k ) <_ ( 2 x. N ) <-> k <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
126	122, 124, 56, 125	syl3anc 1278	. . . . . . . . . 10 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( P ^ k ) <_ ( 2 x. N ) <-> k <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
127		elfz 10434	. . . . . . . . . . 11 |- ( ( k e. ZZ /\ 1 e. ZZ /\ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. ZZ ) -> ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) <-> ( 1 <_ k /\ k <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) )
128	29, 30, 52, 127	syl3anc 1278	. . . . . . . . . 10 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) <-> ( 1 <_ k /\ k <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) )
129	121, 126, 128	3bitr4rd 221	. . . . . . . . 9 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) <-> ( P ^ k ) <_ ( 2 x. N ) ) )
130	129	notbid 677	. . . . . . . 8 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( -. k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) <-> -. ( P ^ k ) <_ ( 2 x. N ) ) )
131	14	nnzd 9778	. . . . . . . . 9 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( P ^ k ) e. ZZ )
132		zltnle 9701	. . . . . . . . 9 |- ( ( ( 2 x. N ) e. ZZ /\ ( P ^ k ) e. ZZ ) -> ( ( 2 x. N ) < ( P ^ k ) <-> -. ( P ^ k ) <_ ( 2 x. N ) ) )
133	8, 131, 132	syl2anc 415	. . . . . . . 8 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) < ( P ^ k ) <-> -. ( P ^ k ) <_ ( 2 x. N ) ) )
134	130, 133	bitr4d 191	. . . . . . 7 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( -. k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) <-> ( 2 x. N ) < ( P ^ k ) ) )
135	61	rpge0d 10118	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 0 <_ ( ( 2 x. N ) / ( P ^ k ) ) )
136	135	adantrr 483	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> 0 <_ ( ( 2 x. N ) / ( P ^ k ) ) )
137	34	nnred 9326	. . . . . . . . . . . . . . . . . 18 |- ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. RR )
138	137	adantr 276	. . . . . . . . . . . . . . . . 17 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. N ) e. RR )
139	14	nnred 9326	. . . . . . . . . . . . . . . . 17 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( P ^ k ) e. RR )
140	14	nngt0d 9357	. . . . . . . . . . . . . . . . 17 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 0 < ( P ^ k ) )
141		ltdivmul 9214	. . . . . . . . . . . . . . . . 17 |- ( ( ( 2 x. N ) e. RR /\ 1 e. RR /\ ( ( P ^ k ) e. RR /\ 0 < ( P ^ k ) ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) < 1 <-> ( 2 x. N ) < ( ( P ^ k ) x. 1 ) ) )
142	138, 27, 139, 140, 141	syl112anc 1282	. . . . . . . . . . . . . . . 16 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) < 1 <-> ( 2 x. N ) < ( ( P ^ k ) x. 1 ) ) )
143	96	mulridd 8349	. . . . . . . . . . . . . . . . 17 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( P ^ k ) x. 1 ) = ( P ^ k ) )
144	143	breq2d 4143	. . . . . . . . . . . . . . . 16 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) < ( ( P ^ k ) x. 1 ) <-> ( 2 x. N ) < ( P ^ k ) ) )
145	142, 144	bitrd 188	. . . . . . . . . . . . . . 15 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) < 1 <-> ( 2 x. N ) < ( P ^ k ) ) )
146	145	biimprd 158	. . . . . . . . . . . . . 14 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) < ( P ^ k ) -> ( ( 2 x. N ) / ( P ^ k ) ) < 1 ) )
147	146	impr 379	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) < 1 )
148		0p1e1 9427	. . . . . . . . . . . . 13 |- ( 0 + 1 ) = 1
149	147, 148	breqtrrdi 4173	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) < ( 0 + 1 ) )
150	16	adantrr 483	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. QQ )
151		0z 9666	. . . . . . . . . . . . 13 |- 0 e. ZZ
152		flqbi 10746	. . . . . . . . . . . . 13 |- ( ( ( ( 2 x. N ) / ( P ^ k ) ) e. QQ /\ 0 e. ZZ ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) = 0 <-> ( 0 <_ ( ( 2 x. N ) / ( P ^ k ) ) /\ ( ( 2 x. N ) / ( P ^ k ) ) < ( 0 + 1 ) ) ) )
153	150, 151, 152	sylancl 417	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) = 0 <-> ( 0 <_ ( ( 2 x. N ) / ( P ^ k ) ) /\ ( ( 2 x. N ) / ( P ^ k ) ) < ( 0 + 1 ) ) ) )
154	136, 149, 153	mpbir2and 957	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) = 0 )
155	74	rpge0d 10118	. . . . . . . . . . . . . . 15 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 0 <_ ( N / ( P ^ k ) ) )
156	155	adantrr 483	. . . . . . . . . . . . . 14 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> 0 <_ ( N / ( P ^ k ) ) )
157		nnre 9320	. . . . . . . . . . . . . . . . . . . . 21 |- ( N e. NN -> N e. RR )
158	157, 71	ltaddrp2d 10149	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. NN -> N < ( N + N ) )
159	94	2timesd 9559	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. NN -> ( 2 x. N ) = ( N + N ) )
160	158, 159	breqtrrd 4159	. . . . . . . . . . . . . . . . . . 19 |- ( N e. NN -> N < ( 2 x. N ) )
161	160	ad2antrr 492	. . . . . . . . . . . . . . . . . 18 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> N < ( 2 x. N ) )
162	157	ad2antrr 492	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> N e. RR )
163		lttr 8405	. . . . . . . . . . . . . . . . . . 19 |- ( ( N e. RR /\ ( 2 x. N ) e. RR /\ ( P ^ k ) e. RR ) -> ( ( N < ( 2 x. N ) /\ ( 2 x. N ) < ( P ^ k ) ) -> N < ( P ^ k ) ) )
164	162, 138, 139, 163	syl3anc 1278	. . . . . . . . . . . . . . . . . 18 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( N < ( 2 x. N ) /\ ( 2 x. N ) < ( P ^ k ) ) -> N < ( P ^ k ) ) )
165	161, 164	mpand 433	. . . . . . . . . . . . . . . . 17 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) < ( P ^ k ) -> N < ( P ^ k ) ) )
166		ltdivmul 9214	. . . . . . . . . . . . . . . . . . 19 |- ( ( N e. RR /\ 1 e. RR /\ ( ( P ^ k ) e. RR /\ 0 < ( P ^ k ) ) ) -> ( ( N / ( P ^ k ) ) < 1 <-> N < ( ( P ^ k ) x. 1 ) ) )
167	162, 27, 139, 140, 166	syl112anc 1282	. . . . . . . . . . . . . . . . . 18 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( N / ( P ^ k ) ) < 1 <-> N < ( ( P ^ k ) x. 1 ) ) )
168	143	breq2d 4143	. . . . . . . . . . . . . . . . . 18 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( N < ( ( P ^ k ) x. 1 ) <-> N < ( P ^ k ) ) )
169	167, 168	bitrd 188	. . . . . . . . . . . . . . . . 17 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( N / ( P ^ k ) ) < 1 <-> N < ( P ^ k ) ) )
170	165, 169	sylibrd 169	. . . . . . . . . . . . . . . 16 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) < ( P ^ k ) -> ( N / ( P ^ k ) ) < 1 ) )
171	170	impr 379	. . . . . . . . . . . . . . 15 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( N / ( P ^ k ) ) < 1 )
172	171, 148	breqtrrdi 4173	. . . . . . . . . . . . . 14 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( N / ( P ^ k ) ) < ( 0 + 1 ) )
173	21	adantrr 483	. . . . . . . . . . . . . . 15 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( N / ( P ^ k ) ) e. QQ )
174		flqbi 10746	. . . . . . . . . . . . . . 15 |- ( ( ( N / ( P ^ k ) ) e. QQ /\ 0 e. ZZ ) -> ( ( |_ ` ( N / ( P ^ k ) ) ) = 0 <-> ( 0 <_ ( N / ( P ^ k ) ) /\ ( N / ( P ^ k ) ) < ( 0 + 1 ) ) ) )
175	173, 151, 174	sylancl 417	. . . . . . . . . . . . . 14 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( ( |_ ` ( N / ( P ^ k ) ) ) = 0 <-> ( 0 <_ ( N / ( P ^ k ) ) /\ ( N / ( P ^ k ) ) < ( 0 + 1 ) ) ) )
176	156, 172, 175	mpbir2and 957	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( |_ ` ( N / ( P ^ k ) ) ) = 0 )
177	176	oveq2d 6104	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) = ( 2 x. 0 ) )
178		2t0e0 9475	. . . . . . . . . . . 12 |- ( 2 x. 0 ) = 0
179	177, 178	eqtrdi 2287	. . . . . . . . . . 11 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) = 0 )
180	154, 179	oveq12d 6106	. . . . . . . . . 10 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = ( 0 - 0 ) )
181		0m0e0 9425	. . . . . . . . . 10 |- ( 0 - 0 ) = 0
182	180, 181	eqtrdi 2287	. . . . . . . . 9 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = 0 )
183		0le0 9402	. . . . . . . . 9 |- 0 <_ 0
184	182, 183	eqbrtrdi 4170	. . . . . . . 8 |- ( ( ( N e. NN /\ P e. Prime ) /\ ( k e. ( 1 ... ( 2 x. N ) ) /\ ( 2 x. N ) < ( P ^ k ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ 0 )
185	184	expr 375	. . . . . . 7 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) < ( P ^ k ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ 0 ) )
186	134, 185	sylbid 150	. . . . . 6 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( -. k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ 0 ) )
187		iffalse 3648	. . . . . . . 8 |- ( -. k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) = 0 )
188	187	eqcomd 2244	. . . . . . 7 |- ( -. k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> 0 = if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) )
189	188	breq2d 4143	. . . . . 6 |- ( -. k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> ( ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ 0 <-> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) ) )
190	186, 189	mpbidi 151	. . . . 5 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( -. k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) ) )
191		exmiddc 848	. . . . . 6 |- (DECID k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) \/ -. k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) )
192	54, 191	syl 14	. . . . 5 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) \/ -. k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) )
193	119, 190, 192	mpjaod 730	. . . 4 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) )
194	7, 26, 55, 193	fsumle 12255	. . 3 |- ( ( N e. NN /\ P e. Prime ) -> sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) <_ sum_ k e. ( 1 ... ( 2 x. N ) ) if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) )
195		pcbcctr 16303	. . 3 |- ( ( N e. NN /\ P e. Prime ) -> ( P pCnt ( ( 2 x. N ) _C N ) ) = sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
196	51	zred 9779	. . . . . . . 8 |- ( ( N e. NN /\ P e. Prime ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. RR )
197		1red 8347	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> 1 e. RR )
198	65	a1i 9	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> 2 e. RR )
199		1lt2 9485	. . . . . . . . . . . . 13 |- 1 < 2
200	199	a1i 9	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> 1 < 2 )
201		2t1e2 9467	. . . . . . . . . . . . 13 |- ( 2 x. 1 ) = 2
202	157	adantr 276	. . . . . . . . . . . . . 14 |- ( ( N e. NN /\ P e. Prime ) -> N e. RR )
203		0le2 9403	. . . . . . . . . . . . . . . 16 |- 0 <_ 2
204	65, 203	pm3.2i 272	. . . . . . . . . . . . . . 15 |- ( 2 e. RR /\ 0 <_ 2 )
205	204	a1i 9	. . . . . . . . . . . . . 14 |- ( ( N e. NN /\ P e. Prime ) -> ( 2 e. RR /\ 0 <_ 2 ) )
206		nnge1 9336	. . . . . . . . . . . . . . 15 |- ( N e. NN -> 1 <_ N )
207	206	adantr 276	. . . . . . . . . . . . . 14 |- ( ( N e. NN /\ P e. Prime ) -> 1 <_ N )
208		lemul2a 9197	. . . . . . . . . . . . . 14 |- ( ( ( 1 e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 <_ 2 ) ) /\ 1 <_ N ) -> ( 2 x. 1 ) <_ ( 2 x. N ) )
209	197, 202, 205, 207, 208	syl31anc 1281	. . . . . . . . . . . . 13 |- ( ( N e. NN /\ P e. Prime ) -> ( 2 x. 1 ) <_ ( 2 x. N ) )
210	201, 209	eqbrtrrid 4167	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> 2 <_ ( 2 x. N ) )
211	197, 198, 137, 200, 210	ltletrd 8758	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> 1 < ( 2 x. N ) )
212	137, 211	rplogcld 16118	. . . . . . . . . 10 |- ( ( N e. NN /\ P e. Prime ) -> ( log ` ( 2 x. N ) ) e. RR+ )
213	9	adantl 277	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> P e. NN )
214	213	nnred 9326	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> P e. RR )
215		eluz2gt1 10018	. . . . . . . . . . . 12 |- ( P e. ( ZZ>= ` 2 ) -> 1 < P )
216	39, 215	syl 14	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> 1 < P )
217	214, 216	rplogcld 16118	. . . . . . . . . 10 |- ( ( N e. NN /\ P e. Prime ) -> ( log ` P ) e. RR+ )
218	212, 217	rpdivcld 10132	. . . . . . . . 9 |- ( ( N e. NN /\ P e. Prime ) -> ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. RR+ )
219	218	rpred 10114	. . . . . . . 8 |- ( ( N e. NN /\ P e. Prime ) -> ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. RR )
220		flaplelt 10730	. . . . . . . . . 10 |- ( ( ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. QQ \/ ( ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. RR /\ A. q e. QQ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) # q ) ) -> ( ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) <_ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) /\ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) < ( ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) + 1 ) ) )
221	49, 220	syl 14	. . . . . . . . 9 |- ( ( N e. NN /\ P e. Prime ) -> ( ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) <_ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) /\ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) < ( ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) + 1 ) ) )
222	221	simpld 112	. . . . . . . 8 |- ( ( N e. NN /\ P e. Prime ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) <_ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) )
223	34	nnnn0d 9631	. . . . . . . . . . . . . 14 |- ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. NN0 )
224	213, 223	nnexpcld 11154	. . . . . . . . . . . . 13 |- ( ( N e. NN /\ P e. Prime ) -> ( P ^ ( 2 x. N ) ) e. NN )
225	224	nnred 9326	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> ( P ^ ( 2 x. N ) ) e. RR )
226		bernneq3 11121	. . . . . . . . . . . . 13 |- ( ( P e. ( ZZ>= ` 2 ) /\ ( 2 x. N ) e. NN0 ) -> ( 2 x. N ) < ( P ^ ( 2 x. N ) ) )
227	39, 223, 226	syl2anc 415	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) < ( P ^ ( 2 x. N ) ) )
228	137, 225, 227	ltled 8452	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) <_ ( P ^ ( 2 x. N ) ) )
229	40	reeflogd 16113	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> ( exp ` ( log ` ( 2 x. N ) ) ) = ( 2 x. N ) )
230	213	nnrpd 10112	. . . . . . . . . . . . 13 |- ( ( N e. NN /\ P e. Prime ) -> P e. RR+ )
231	34	nnzd 9778	. . . . . . . . . . . . 13 |- ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. ZZ )
232		reexplog 16101	. . . . . . . . . . . . 13 |- ( ( P e. RR+ /\ ( 2 x. N ) e. ZZ ) -> ( P ^ ( 2 x. N ) ) = ( exp ` ( ( 2 x. N ) x. ( log ` P ) ) ) )
233	230, 231, 232	syl2anc 415	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> ( P ^ ( 2 x. N ) ) = ( exp ` ( ( 2 x. N ) x. ( log ` P ) ) ) )
234	233	eqcomd 2244	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> ( exp ` ( ( 2 x. N ) x. ( log ` P ) ) ) = ( P ^ ( 2 x. N ) ) )
235	228, 229, 234	3brtr4d 4163	. . . . . . . . . 10 |- ( ( N e. NN /\ P e. Prime ) -> ( exp ` ( log ` ( 2 x. N ) ) ) <_ ( exp ` ( ( 2 x. N ) x. ( log ` P ) ) ) )
236	40	relogcld 16112	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> ( log ` ( 2 x. N ) ) e. RR )
237	217	rpred 10114	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> ( log ` P ) e. RR )
238	137, 237	remulcld 8362	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> ( ( 2 x. N ) x. ( log ` P ) ) e. RR )
239		efle 16002	. . . . . . . . . . 11 |- ( ( ( log ` ( 2 x. N ) ) e. RR /\ ( ( 2 x. N ) x. ( log ` P ) ) e. RR ) -> ( ( log ` ( 2 x. N ) ) <_ ( ( 2 x. N ) x. ( log ` P ) ) <-> ( exp ` ( log ` ( 2 x. N ) ) ) <_ ( exp ` ( ( 2 x. N ) x. ( log ` P ) ) ) ) )
240	236, 238, 239	syl2anc 415	. . . . . . . . . 10 |- ( ( N e. NN /\ P e. Prime ) -> ( ( log ` ( 2 x. N ) ) <_ ( ( 2 x. N ) x. ( log ` P ) ) <-> ( exp ` ( log ` ( 2 x. N ) ) ) <_ ( exp ` ( ( 2 x. N ) x. ( log ` P ) ) ) ) )
241	235, 240	mpbird 167	. . . . . . . . 9 |- ( ( N e. NN /\ P e. Prime ) -> ( log ` ( 2 x. N ) ) <_ ( ( 2 x. N ) x. ( log ` P ) ) )
242	236, 137, 217	ledivmul2d 10169	. . . . . . . . 9 |- ( ( N e. NN /\ P e. Prime ) -> ( ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) <_ ( 2 x. N ) <-> ( log ` ( 2 x. N ) ) <_ ( ( 2 x. N ) x. ( log ` P ) ) ) )
243	241, 242	mpbird 167	. . . . . . . 8 |- ( ( N e. NN /\ P e. Prime ) -> ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) <_ ( 2 x. N ) )
244	196, 219, 137, 222, 243	letrd 8457	. . . . . . 7 |- ( ( N e. NN /\ P e. Prime ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) <_ ( 2 x. N ) )
245		eluz 9951	. . . . . . . 8 |- ( ( ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. ZZ /\ ( 2 x. N ) e. ZZ ) -> ( ( 2 x. N ) e. ( ZZ>= ` ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) <-> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) <_ ( 2 x. N ) ) )
246	51, 231, 245	syl2anc 415	. . . . . . 7 |- ( ( N e. NN /\ P e. Prime ) -> ( ( 2 x. N ) e. ( ZZ>= ` ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) <-> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) <_ ( 2 x. N ) ) )
247	244, 246	mpbird 167	. . . . . 6 |- ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. ( ZZ>= ` ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
248		fzss2 10487	. . . . . 6 |- ( ( 2 x. N ) e. ( ZZ>= ` ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) -> ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) C_ ( 1 ... ( 2 x. N ) ) )
249	247, 248	syl 14	. . . . 5 |- ( ( N e. NN /\ P e. Prime ) -> ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) C_ ( 1 ... ( 2 x. N ) ) )
250		elfzelz 10445	. . . . . . . 8 |- ( u e. ( 1 ... ( 2 x. N ) ) -> u e. ZZ )
251	250	adantl 277	. . . . . . 7 |- ( ( ( N e. NN /\ P e. Prime ) /\ u e. ( 1 ... ( 2 x. N ) ) ) -> u e. ZZ )
252		1zzd 9682	. . . . . . 7 |- ( ( ( N e. NN /\ P e. Prime ) /\ u e. ( 1 ... ( 2 x. N ) ) ) -> 1 e. ZZ )
253	51	adantr 276	. . . . . . 7 |- ( ( ( N e. NN /\ P e. Prime ) /\ u e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. ZZ )
254		fzdcel 10461	. . . . . . 7 |- ( ( u e. ZZ /\ 1 e. ZZ /\ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. ZZ ) -> DECID u e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
255	251, 252, 253, 254	syl3anc 1278	. . . . . 6 |- ( ( ( N e. NN /\ P e. Prime ) /\ u e. ( 1 ... ( 2 x. N ) ) ) -> DECID u e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
256	255	ralrimiva 2623	. . . . 5 |- ( ( N e. NN /\ P e. Prime ) -> A. u e. ( 1 ... ( 2 x. N ) )DECID u e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
257		sumhashdc 13155	. . . . 5 |- ( ( ( 1 ... ( 2 x. N ) ) e. Fin /\ ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) C_ ( 1 ... ( 2 x. N ) ) /\ A. u e. ( 1 ... ( 2 x. N ) )DECID u e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) -> sum_ k e. ( 1 ... ( 2 x. N ) ) if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) = (♯ ` ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) )
258	7, 249, 256, 257	syl3anc 1278	. . . 4 |- ( ( N e. NN /\ P e. Prime ) -> sum_ k e. ( 1 ... ( 2 x. N ) ) if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) = (♯ ` ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) )
259	218	rpge0d 10118	. . . . . . 7 |- ( ( N e. NN /\ P e. Prime ) -> 0 <_ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) )
260		flapge 10737	. . . . . . . 8 |- ( ( ( ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. QQ \/ ( ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. RR /\ A. q e. QQ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) # q ) ) /\ 0 e. ZZ ) -> ( 0 <_ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) <-> 0 <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
261	49, 151, 260	sylancl 417	. . . . . . 7 |- ( ( N e. NN /\ P e. Prime ) -> ( 0 <_ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) <-> 0 <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
262	259, 261	mpbid 147	. . . . . 6 |- ( ( N e. NN /\ P e. Prime ) -> 0 <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) )
263		elnn0z 9668	. . . . . 6 |- ( ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. NN0 <-> ( ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. ZZ /\ 0 <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
264	51, 262, 263	sylanbrc 421	. . . . 5 |- ( ( N e. NN /\ P e. Prime ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. NN0 )
265		hashfz1 11244	. . . . 5 |- ( ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. NN0 -> (♯ ` ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) = ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) )
266	264, 265	syl 14	. . . 4 |- ( ( N e. NN /\ P e. Prime ) -> (♯ ` ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) ) = ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) )
267	258, 266	eqtr2d 2272	. . 3 |- ( ( N e. NN /\ P e. Prime ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) = sum_ k e. ( 1 ... ( 2 x. N ) ) if ( k e. ( 1 ... ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) , 1 , 0 ) )
268	194, 195, 267	3brtr4d 4163	. 2 |- ( ( N e. NN /\ P e. Prime ) -> ( P pCnt ( ( 2 x. N ) _C N ) ) <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) )
269		nnnn0 9581	. . . . . . 7 |- ( N e. NN -> N e. NN0 )
270		fzctr 10557	. . . . . . 7 |- ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) )
271		bccl2 11228	. . . . . . 7 |- ( N e. ( 0 ... ( 2 x. N ) ) -> ( ( 2 x. N ) _C N ) e. NN )
272	269, 270, 271	3syl 17	. . . . . 6 |- ( N e. NN -> ( ( 2 x. N ) _C N ) e. NN )
273	272	adantr 276	. . . . 5 |- ( ( N e. NN /\ P e. Prime ) -> ( ( 2 x. N ) _C N ) e. NN )
274	35, 273	pccld 13108	. . . 4 |- ( ( N e. NN /\ P e. Prime ) -> ( P pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
275	274	nn0zd 9777	. . 3 |- ( ( N e. NN /\ P e. Prime ) -> ( P pCnt ( ( 2 x. N ) _C N ) ) e. ZZ )
276		prmefexple 16308	. . 3 |- ( ( P e. Prime /\ ( P pCnt ( ( 2 x. N ) _C N ) ) e. ZZ /\ ( 2 x. N ) e. NN ) -> ( ( P ^ ( P pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) <-> ( P pCnt ( ( 2 x. N ) _C N ) ) <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
277	35, 275, 34, 276	syl3anc 1278	. 2 |- ( ( N e. NN /\ P e. Prime ) -> ( ( P ^ ( P pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) <-> ( P pCnt ( ( 2 x. N ) _C N ) ) <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) ) )
278	268, 277	mpbird 167	1 |- ( ( N e. NN /\ P e. Prime ) -> ( P ^ ( P pCnt ( ( 2 x. N ) _C N ) ) ) <_ ( 2 x. N ) )

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   C_ wss 3220   ifcif 3638   class class class wbr 4131   ` cfv 5380  (class class class)co 6088   Fincfn 7026   CCcc 8183   RRcr 8184   0cc0 8185   1c1 8186   + caddc 8188   x. cmul 8190   < clt 8366   <_ cle 8367   - cmin 8504   # cap 8917   / cdiv 9010   NNcn 9313   2c2 9364   NN0cn0 9574   ZZcz 9655   ZZ>=cuz 9937   QQcq 10035   RR+crp 10071   ...cfz 10428   |_cfl 10720   ^cexp 10996   _C cbc 11207  ♯chash 11236   sum_csu 12144   expce 12434   Primecprime 12910   pCnt cpc 13092   logclog 16085   log_b clogb 16179

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-n0 9575  df-z 9656  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-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

This theorem is used by:  bposlem5  16315  bposlem6  16316