Theorem bposlem1 16209

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 9675	. . . . 5 |- ( ( N e. NN /\ P e. Prime ) -> 1 e. ZZ )
2		2z 9676	. . . . . . 7 |- 2 e. ZZ
3	2	a1i 9	. . . . . 6 |- ( ( N e. NN /\ P e. Prime ) -> 2 e. ZZ )
4		nnz 9667	. . . . . . 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 9778	. . . . 5 |- ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. ZZ )
7	1, 6	fzfigd 10881	. . . 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 12904	. . . . . . . . . 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 10470	. . . . . . . . . . 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 9624	. . . . . . . . 9 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> k e. NN0 )
14	10, 13	nnexpcld 11146	. . . . . . . 8 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( P ^ k ) e. NN )
15		znq 10033	. . . . . . . 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 10724	. . . . . 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 9771	. . . . . . . . 9 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> N e. ZZ )
20		znq 10033	. . . . . . . . 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 10724	. . . . . . 7 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( N / ( P ^ k ) ) ) e. ZZ )
23		zmulcl 9702	. . . . . . 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 9777	. . . . 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 9772	. . . 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 8341	. . . . 5 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 1 e. RR )
28		0red 8327	. . . . 5 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 0 e. RR )
29	12	nnzd 9771	. . . . . 6 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> k e. ZZ )
30		1zzd 9675	. . . . . 6 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 1 e. ZZ )
31		2nn 9470	. . . . . . . . . . . 12 |- 2 e. NN
32		nnmulcl 9327	. . . . . . . . . . . 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 16137	. . . . . . . . . 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 12926	. . . . . . . . . . . . 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 10105	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. RR+ )
41		relogbval 16106	. . . . . . . . . . . 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 4140	. . . . . . . . . . . 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 10721	. . . . . . . 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 10454	. . . . . 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 10074	. . . . . . . . . . . . 13 |- ( ( 2 x. N ) e. NN -> ( 2 x. N ) e. RR+ )
58		nnrp 10074	. . . . . . . . . . . . 13 |- ( ( P ^ k ) e. NN -> ( P ^ k ) e. RR+ )
59		rpdivcl 10090	. . . . . . . . . . . . 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 10107	. . . . . . . . . 10 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. RR )
63	24	zred 9772	. . . . . . . . . 10 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) e. RR )
64	62, 63	resubcld 8709	. . . . . . . . 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 9376	. . . . . . . . . 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 9772	. . . . . . . . . 10 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) e. RR )
68		flqle 10725	. . . . . . . . . . 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 8890	. . . . . . . . 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 10074	. . . . . . . . . . . . . . . 16 |- ( N e. NN -> N e. RR+ )
72		rpdivcl 10090	. . . . . . . . . . . . . . . 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 10107	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( N / ( P ^ k ) ) e. RR )
76		1re 8325	. . . . . . . . . . . . 13 |- 1 e. RR
77		resubcl 8591	. . . . . . . . . . . . 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 8307	. . . . . . . . . . . 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 10726	. . . . . . . . . . . . . 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 9772	. . . . . . . . . . . . . 14 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( |_ ` ( N / ( P ^ k ) ) ) e. RR )
84	75, 27, 83	ltsubaddd 8870	. . . . . . . . . . . . 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 9397	. . . . . . . . . . . . . . 15 |- 0 < 2
87	65, 86	pm3.2i 272	. . . . . . . . . . . . . 14 |- ( 2 e. RR /\ 0 < 2 )
88		ltmul2 9188	. . . . . . . . . . . . . 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 8887	. . . . . . . . . 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 9379	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 2 e. CC )
94		nncn 9314	. . . . . . . . . . . . . 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 9320	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( P ^ k ) e. CC )
97	14	nnap0d 9352	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( P ^ k ) # 0 )
98	93, 95, 96, 97	divassapd 9158	. . . . . . . . . . . 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 8354	. . . . . . . . . . . . 13 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( N / ( P ^ k ) ) e. CC )
100	93, 99	muls1d 8746	. . . . . . . . . . . 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 6103	. . . . . . . . . . 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 8307	. . . . . . . . . . . . . 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 8354	. . . . . . . . . . . 12 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( 2 x. ( N / ( P ^ k ) ) ) e. CC )
105		2cn 9377	. . . . . . . . . . . 12 |- 2 e. CC
106		nncan 8556	. . . . . . . . . . . 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 4156	. . . . . . . . 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 8452	. . . . . . . 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 9365	. . . . . . . 8 |- 2 = ( 1 + 1 )
112	110, 111	breqtrdi 4171	. . . . . . 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 9674	. . . . . . . 8 |- 1 e. ZZ
114		zleltp1 9704	. . . . . . . 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 4142	. . . . . 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 9349	. . . . . . . . . . 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 10438	. . . . . . . . . . . 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 16206	. . . . . . . . . . 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 10427	. . . . . . . . . . 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 9771	. . . . . . . . 9 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( P ^ k ) e. ZZ )
132		zltnle 9694	. . . . . . . . 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 10111	. . . . . . . . . . . . 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 9319	. . . . . . . . . . . . . . . . . 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 9319	. . . . . . . . . . . . . . . . 17 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( P ^ k ) e. RR )
140	14	nngt0d 9350	. . . . . . . . . . . . . . . . 17 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> 0 < ( P ^ k ) )
141		ltdivmul 9208	. . . . . . . . . . . . . . . . 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 8343	. . . . . . . . . . . . . . . . 17 |- ( ( ( N e. NN /\ P e. Prime ) /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( P ^ k ) x. 1 ) = ( P ^ k ) )
144	143	breq2d 4142	. . . . . . . . . . . . . . . 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 9420	. . . . . . . . . . . . 13 |- ( 0 + 1 ) = 1
149	147, 148	breqtrrdi 4172	. . . . . . . . . . . 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 9659	. . . . . . . . . . . . 13 |- 0 e. ZZ
152		flqbi 10738	. . . . . . . . . . . . 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 10111	. . . . . . . . . . . . . . 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 9313	. . . . . . . . . . . . . . . . . . . . 21 |- ( N e. NN -> N e. RR )
158	157, 71	ltaddrp2d 10142	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. NN -> N < ( N + N ) )
159	94	2timesd 9552	. . . . . . . . . . . . . . . . . . . 20 |- ( N e. NN -> ( 2 x. N ) = ( N + N ) )
160	158, 159	breqtrrd 4158	. . . . . . . . . . . . . . . . . . 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 8399	. . . . . . . . . . . . . . . . . . 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 9208	. . . . . . . . . . . . . . . . . . 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 4142	. . . . . . . . . . . . . . . . . 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 4172	. . . . . . . . . . . . . 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 10738	. . . . . . . . . . . . . . 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 6101	. . . . . . . . . . . 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 9468	. . . . . . . . . . . 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 6103	. . . . . . . . . 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 9418	. . . . . . . . . 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 9395	. . . . . . . . 9 |- 0 <_ 0
184	182, 183	eqbrtrdi 4169	. . . . . . . 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 4142	. . . . . 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 12246	. . 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 16201	. . 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 9772	. . . . . . . 8 |- ( ( N e. NN /\ P e. Prime ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) e. RR )
197		1red 8341	. . . . . . . . . . . 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 9478	. . . . . . . . . . . . 13 |- 1 < 2
200	199	a1i 9	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> 1 < 2 )
201		2t1e2 9460	. . . . . . . . . . . . 13 |- ( 2 x. 1 ) = 2
202	157	adantr 276	. . . . . . . . . . . . . 14 |- ( ( N e. NN /\ P e. Prime ) -> N e. RR )
203		0le2 9396	. . . . . . . . . . . . . . . 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 9329	. . . . . . . . . . . . . . 15 |- ( N e. NN -> 1 <_ N )
207	206	adantr 276	. . . . . . . . . . . . . 14 |- ( ( N e. NN /\ P e. Prime ) -> 1 <_ N )
208		lemul2a 9191	. . . . . . . . . . . . . 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 4166	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> 2 <_ ( 2 x. N ) )
211	197, 198, 137, 200, 210	ltletrd 8752	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> 1 < ( 2 x. N ) )
212	137, 211	rplogcld 16040	. . . . . . . . . 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 9319	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> P e. RR )
215		eluz2gt1 10011	. . . . . . . . . . . 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 16040	. . . . . . . . . 10 |- ( ( N e. NN /\ P e. Prime ) -> ( log ` P ) e. RR+ )
218	212, 217	rpdivcld 10125	. . . . . . . . 9 |- ( ( N e. NN /\ P e. Prime ) -> ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. RR+ )
219	218	rpred 10107	. . . . . . . 8 |- ( ( N e. NN /\ P e. Prime ) -> ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) e. RR )
220		flaplelt 10723	. . . . . . . . . 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 9624	. . . . . . . . . . . . . 14 |- ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. NN0 )
224	213, 223	nnexpcld 11146	. . . . . . . . . . . . 13 |- ( ( N e. NN /\ P e. Prime ) -> ( P ^ ( 2 x. N ) ) e. NN )
225	224	nnred 9319	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> ( P ^ ( 2 x. N ) ) e. RR )
226		bernneq3 11113	. . . . . . . . . . . . 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 8446	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) <_ ( P ^ ( 2 x. N ) ) )
229	40	reeflogd 16035	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> ( exp ` ( log ` ( 2 x. N ) ) ) = ( 2 x. N ) )
230	213	nnrpd 10105	. . . . . . . . . . . . 13 |- ( ( N e. NN /\ P e. Prime ) -> P e. RR+ )
231	34	nnzd 9771	. . . . . . . . . . . . 13 |- ( ( N e. NN /\ P e. Prime ) -> ( 2 x. N ) e. ZZ )
232		reexplog 16023	. . . . . . . . . . . . 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 4162	. . . . . . . . . 10 |- ( ( N e. NN /\ P e. Prime ) -> ( exp ` ( log ` ( 2 x. N ) ) ) <_ ( exp ` ( ( 2 x. N ) x. ( log ` P ) ) ) )
236	40	relogcld 16034	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> ( log ` ( 2 x. N ) ) e. RR )
237	217	rpred 10107	. . . . . . . . . . . 12 |- ( ( N e. NN /\ P e. Prime ) -> ( log ` P ) e. RR )
238	137, 237	remulcld 8356	. . . . . . . . . . 11 |- ( ( N e. NN /\ P e. Prime ) -> ( ( 2 x. N ) x. ( log ` P ) ) e. RR )
239		efle 15926	. . . . . . . . . . 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 10162	. . . . . . . . 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 8451	. . . . . . 7 |- ( ( N e. NN /\ P e. Prime ) -> ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) <_ ( 2 x. N ) )
245		eluz 9944	. . . . . . . 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 10480	. . . . . 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 10438	. . . . . . . 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 9675	. . . . . . 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 10454	. . . . . . 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 13146	. . . . 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 10111	. . . . . . 7 |- ( ( N e. NN /\ P e. Prime ) -> 0 <_ ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) )
260		flapge 10730	. . . . . . . 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 9661	. . . . . 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 11236	. . . . 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 4162	. 2 |- ( ( N e. NN /\ P e. Prime ) -> ( P pCnt ( ( 2 x. N ) _C N ) ) <_ ( |_ ` ( ( log ` ( 2 x. N ) ) / ( log ` P ) ) ) )
269		nnnn0 9574	. . . . . . 7 |- ( N e. NN -> N e. NN0 )
270		fzctr 10550	. . . . . . 7 |- ( N e. NN0 -> N e. ( 0 ... ( 2 x. N ) ) )
271		bccl2 11220	. . . . . . 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 13099	. . . 4 |- ( ( N e. NN /\ P e. Prime ) -> ( P pCnt ( ( 2 x. N ) _C N ) ) e. NN0 )
275	274	nn0zd 9770	. . 3 |- ( ( N e. NN /\ P e. Prime ) -> ( P pCnt ( ( 2 x. N ) _C N ) ) e. ZZ )
276		prmefexple 16206	. . 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 4130   ` cfv 5377  (class class class)co 6085   Fincfn 7022   CCcc 8177   RRcr 8178   0cc0 8179   1c1 8180   + caddc 8182   x. cmul 8184   < clt 8360   <_ cle 8361   - cmin 8498   # cap 8911   / cdiv 9004   NNcn 9306   2c2 9357   NN0cn0 9567   ZZcz 9648   ZZ>=cuz 9930   QQcq 10028   RR+crp 10064   ...cfz 10421   |_cfl 10713   ^cexp 10988   _C cbc 11199  ♯chash 11228   sum_csu 12135   expce 12425   Primecprime 12901   pCnt cpc 13083   logclog 16007   log_b clogb 16098

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-n0 9568  df-z 9649  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-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

This theorem is used by:  bposlem5  16213