Theorem bposlem2 21022

Description: There are no odd primes in the range ( 2 N / 3 , N ] dividing the N-th central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)

Hypotheses

Ref	Expression
bposlem2.1	|- ( ph -> N e. NN )
bposlem2.2	|- ( ph -> P e. Prime )
bposlem2.3	|- ( ph -> 2 < P )
bposlem2.4	|- ( ph -> ( ( 2 x. N ) / 3 ) < P )
bposlem2.5	|- ( ph -> P <_ N )

Assertion

Ref	Expression
bposlem2	|- ( ph -> ( P pCnt ( ( 2 x. N ) _C N ) ) = 0 )

Proof of Theorem bposlem2

Dummy variable k is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bposlem2.1	. . 3 |- ( ph -> N e. NN )
2		bposlem2.2	. . 3 |- ( ph -> P e. Prime )
3		pcbcctr 21013	. . 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 ) ) ) ) ) )
4	1, 2, 3	syl2anc 643	. 2 |- ( ph -> ( P pCnt ( ( 2 x. N ) _C N ) ) = sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) )
5		elfznn 11036	. . . . . 6 |- ( k e. ( 1 ... ( 2 x. N ) ) -> k e. NN )
6		elnn1uz2 10508	. . . . . 6 |- ( k e. NN <-> ( k = 1 \/ k e. ( ZZ>= ` 2 ) ) )
7	5, 6	sylib 189	. . . . 5 |- ( k e. ( 1 ... ( 2 x. N ) ) -> ( k = 1 \/ k e. ( ZZ>= ` 2 ) ) )
8		oveq2 6048	. . . . . . . . . . . 12 |- ( k = 1 -> ( P ^ k ) = ( P ^ 1 ) )
9		prmnn 13037	. . . . . . . . . . . . . . 15 |- ( P e. Prime -> P e. NN )
10	2, 9	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> P e. NN )
11	10	nncnd 9972	. . . . . . . . . . . . 13 |- ( ph -> P e. CC )
12	11	exp1d 11473	. . . . . . . . . . . 12 |- ( ph -> ( P ^ 1 ) = P )
13	8, 12	sylan9eqr 2458	. . . . . . . . . . 11 |- ( ( ph /\ k = 1 ) -> ( P ^ k ) = P )
14	13	oveq2d 6056	. . . . . . . . . 10 |- ( ( ph /\ k = 1 ) -> ( ( 2 x. N ) / ( P ^ k ) ) = ( ( 2 x. N ) / P ) )
15	14	fveq2d 5691	. . . . . . . . 9 |- ( ( ph /\ k = 1 ) -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) = ( |_ ` ( ( 2 x. N ) / P ) ) )
16		2cn 10026	. . . . . . . . . . . . . 14 |- 2 e. CC
17	16	mulid1i 9048	. . . . . . . . . . . . 13 |- ( 2 x. 1 ) = 2
18	11	mulid2d 9062	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 1 x. P ) = P )
19		bposlem2.5	. . . . . . . . . . . . . . . 16 |- ( ph -> P <_ N )
20	18, 19	eqbrtrd 4192	. . . . . . . . . . . . . . 15 |- ( ph -> ( 1 x. P ) <_ N )
21		1re 9046	. . . . . . . . . . . . . . . . 17 |- 1 e. RR
22	21	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> 1 e. RR )
23	1	nnred 9971	. . . . . . . . . . . . . . . 16 |- ( ph -> N e. RR )
24	10	nnred 9971	. . . . . . . . . . . . . . . 16 |- ( ph -> P e. RR )
25	10	nngt0d 9999	. . . . . . . . . . . . . . . 16 |- ( ph -> 0 < P )
26		lemuldiv 9845	. . . . . . . . . . . . . . . 16 |- ( ( 1 e. RR /\ N e. RR /\ ( P e. RR /\ 0 < P ) ) -> ( ( 1 x. P ) <_ N <-> 1 <_ ( N / P ) ) )
27	22, 23, 24, 25, 26	syl112anc 1188	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( 1 x. P ) <_ N <-> 1 <_ ( N / P ) ) )
28	20, 27	mpbid 202	. . . . . . . . . . . . . 14 |- ( ph -> 1 <_ ( N / P ) )
29	23, 10	nndivred 10004	. . . . . . . . . . . . . . 15 |- ( ph -> ( N / P ) e. RR )
30		2re 10025	. . . . . . . . . . . . . . . . 17 |- 2 e. RR
31		2pos 10038	. . . . . . . . . . . . . . . . 17 |- 0 < 2
32	30, 31	pm3.2i 442	. . . . . . . . . . . . . . . 16 |- ( 2 e. RR /\ 0 < 2 )
33		lemul2 9819	. . . . . . . . . . . . . . . 16 |- ( ( 1 e. RR /\ ( N / P ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( 1 <_ ( N / P ) <-> ( 2 x. 1 ) <_ ( 2 x. ( N / P ) ) ) )
34	21, 32, 33	mp3an13 1270	. . . . . . . . . . . . . . 15 |- ( ( N / P ) e. RR -> ( 1 <_ ( N / P ) <-> ( 2 x. 1 ) <_ ( 2 x. ( N / P ) ) ) )
35	29, 34	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 <_ ( N / P ) <-> ( 2 x. 1 ) <_ ( 2 x. ( N / P ) ) ) )
36	28, 35	mpbid 202	. . . . . . . . . . . . 13 |- ( ph -> ( 2 x. 1 ) <_ ( 2 x. ( N / P ) ) )
37	17, 36	syl5eqbrr 4206	. . . . . . . . . . . 12 |- ( ph -> 2 <_ ( 2 x. ( N / P ) ) )
38	16	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> 2 e. CC )
39	1	nncnd 9972	. . . . . . . . . . . . 13 |- ( ph -> N e. CC )
40	10	nnne0d 10000	. . . . . . . . . . . . 13 |- ( ph -> P =/= 0 )
41	38, 39, 11, 40	divassd 9781	. . . . . . . . . . . 12 |- ( ph -> ( ( 2 x. N ) / P ) = ( 2 x. ( N / P ) ) )
42	37, 41	breqtrrd 4198	. . . . . . . . . . 11 |- ( ph -> 2 <_ ( ( 2 x. N ) / P ) )
43		bposlem2.4	. . . . . . . . . . . . 13 |- ( ph -> ( ( 2 x. N ) / 3 ) < P )
44		2nn 10089	. . . . . . . . . . . . . . . 16 |- 2 e. NN
45		nnmulcl 9979	. . . . . . . . . . . . . . . 16 |- ( ( 2 e. NN /\ N e. NN ) -> ( 2 x. N ) e. NN )
46	44, 1, 45	sylancr 645	. . . . . . . . . . . . . . 15 |- ( ph -> ( 2 x. N ) e. NN )
47	46	nnred 9971	. . . . . . . . . . . . . 14 |- ( ph -> ( 2 x. N ) e. RR )
48		3re 10027	. . . . . . . . . . . . . . . 16 |- 3 e. RR
49		3pos 10040	. . . . . . . . . . . . . . . 16 |- 0 < 3
50	48, 49	pm3.2i 442	. . . . . . . . . . . . . . 15 |- ( 3 e. RR /\ 0 < 3 )
51		ltdiv23 9857	. . . . . . . . . . . . . . 15 |- ( ( ( 2 x. N ) e. RR /\ ( 3 e. RR /\ 0 < 3 ) /\ ( P e. RR /\ 0 < P ) ) -> ( ( ( 2 x. N ) / 3 ) < P <-> ( ( 2 x. N ) / P ) < 3 ) )
52	50, 51	mp3an2 1267	. . . . . . . . . . . . . 14 |- ( ( ( 2 x. N ) e. RR /\ ( P e. RR /\ 0 < P ) ) -> ( ( ( 2 x. N ) / 3 ) < P <-> ( ( 2 x. N ) / P ) < 3 ) )
53	47, 24, 25, 52	syl12anc 1182	. . . . . . . . . . . . 13 |- ( ph -> ( ( ( 2 x. N ) / 3 ) < P <-> ( ( 2 x. N ) / P ) < 3 ) )
54	43, 53	mpbid 202	. . . . . . . . . . . 12 |- ( ph -> ( ( 2 x. N ) / P ) < 3 )
55		df-3 10015	. . . . . . . . . . . 12 |- 3 = ( 2 + 1 )
56	54, 55	syl6breq 4211	. . . . . . . . . . 11 |- ( ph -> ( ( 2 x. N ) / P ) < ( 2 + 1 ) )
57	47, 10	nndivred 10004	. . . . . . . . . . . 12 |- ( ph -> ( ( 2 x. N ) / P ) e. RR )
58		2z 10268	. . . . . . . . . . . 12 |- 2 e. ZZ
59		flbi 11178	. . . . . . . . . . . 12 |- ( ( ( ( 2 x. N ) / P ) e. RR /\ 2 e. ZZ ) -> ( ( |_ ` ( ( 2 x. N ) / P ) ) = 2 <-> ( 2 <_ ( ( 2 x. N ) / P ) /\ ( ( 2 x. N ) / P ) < ( 2 + 1 ) ) ) )
60	57, 58, 59	sylancl 644	. . . . . . . . . . 11 |- ( ph -> ( ( |_ ` ( ( 2 x. N ) / P ) ) = 2 <-> ( 2 <_ ( ( 2 x. N ) / P ) /\ ( ( 2 x. N ) / P ) < ( 2 + 1 ) ) ) )
61	42, 56, 60	mpbir2and 889	. . . . . . . . . 10 |- ( ph -> ( |_ ` ( ( 2 x. N ) / P ) ) = 2 )
62	61	adantr 452	. . . . . . . . 9 |- ( ( ph /\ k = 1 ) -> ( |_ ` ( ( 2 x. N ) / P ) ) = 2 )
63	15, 62	eqtrd 2436	. . . . . . . 8 |- ( ( ph /\ k = 1 ) -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) = 2 )
64	13	oveq2d 6056	. . . . . . . . . . . 12 |- ( ( ph /\ k = 1 ) -> ( N / ( P ^ k ) ) = ( N / P ) )
65	64	fveq2d 5691	. . . . . . . . . . 11 |- ( ( ph /\ k = 1 ) -> ( |_ ` ( N / ( P ^ k ) ) ) = ( |_ ` ( N / P ) ) )
66		remulcl 9031	. . . . . . . . . . . . . . . . . 18 |- ( ( 2 e. RR /\ ( N / P ) e. RR ) -> ( 2 x. ( N / P ) ) e. RR )
67	30, 29, 66	sylancr 645	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( 2 x. ( N / P ) ) e. RR )
68	48	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> 3 e. RR )
69		4re 10029	. . . . . . . . . . . . . . . . . 18 |- 4 e. RR
70	69	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> 4 e. RR )
71	41, 54	eqbrtrrd 4194	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( 2 x. ( N / P ) ) < 3 )
72		3lt4 10101	. . . . . . . . . . . . . . . . . 18 |- 3 < 4
73	72	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( ph -> 3 < 4 )
74	67, 68, 70, 71, 73	lttrd 9187	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 2 x. ( N / P ) ) < 4 )
75		2t2e4 10083	. . . . . . . . . . . . . . . 16 |- ( 2 x. 2 ) = 4
76	74, 75	syl6breqr 4212	. . . . . . . . . . . . . . 15 |- ( ph -> ( 2 x. ( N / P ) ) < ( 2 x. 2 ) )
77		ltmul2 9817	. . . . . . . . . . . . . . . . 17 |- ( ( ( N / P ) e. RR /\ 2 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( N / P ) < 2 <-> ( 2 x. ( N / P ) ) < ( 2 x. 2 ) ) )
78	30, 32, 77	mp3an23 1271	. . . . . . . . . . . . . . . 16 |- ( ( N / P ) e. RR -> ( ( N / P ) < 2 <-> ( 2 x. ( N / P ) ) < ( 2 x. 2 ) ) )
79	29, 78	syl 16	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( N / P ) < 2 <-> ( 2 x. ( N / P ) ) < ( 2 x. 2 ) ) )
80	76, 79	mpbird 224	. . . . . . . . . . . . . 14 |- ( ph -> ( N / P ) < 2 )
81		df-2 10014	. . . . . . . . . . . . . 14 |- 2 = ( 1 + 1 )
82	80, 81	syl6breq 4211	. . . . . . . . . . . . 13 |- ( ph -> ( N / P ) < ( 1 + 1 ) )
83		1z 10267	. . . . . . . . . . . . . 14 |- 1 e. ZZ
84		flbi 11178	. . . . . . . . . . . . . 14 |- ( ( ( N / P ) e. RR /\ 1 e. ZZ ) -> ( ( |_ ` ( N / P ) ) = 1 <-> ( 1 <_ ( N / P ) /\ ( N / P ) < ( 1 + 1 ) ) ) )
85	29, 83, 84	sylancl 644	. . . . . . . . . . . . 13 |- ( ph -> ( ( |_ ` ( N / P ) ) = 1 <-> ( 1 <_ ( N / P ) /\ ( N / P ) < ( 1 + 1 ) ) ) )
86	28, 82, 85	mpbir2and 889	. . . . . . . . . . . 12 |- ( ph -> ( |_ ` ( N / P ) ) = 1 )
87	86	adantr 452	. . . . . . . . . . 11 |- ( ( ph /\ k = 1 ) -> ( |_ ` ( N / P ) ) = 1 )
88	65, 87	eqtrd 2436	. . . . . . . . . 10 |- ( ( ph /\ k = 1 ) -> ( |_ ` ( N / ( P ^ k ) ) ) = 1 )
89	88	oveq2d 6056	. . . . . . . . 9 |- ( ( ph /\ k = 1 ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) = ( 2 x. 1 ) )
90	89, 17	syl6eq 2452	. . . . . . . 8 |- ( ( ph /\ k = 1 ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) = 2 )
91	63, 90	oveq12d 6058	. . . . . . 7 |- ( ( ph /\ k = 1 ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = ( 2 - 2 ) )
92	16	subidi 9327	. . . . . . 7 |- ( 2 - 2 ) = 0
93	91, 92	syl6eq 2452	. . . . . 6 |- ( ( ph /\ k = 1 ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = 0 )
94	46	nnrpd 10603	. . . . . . . . . . . 12 |- ( ph -> ( 2 x. N ) e. RR+ )
95	94	adantr 452	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 2 x. N ) e. RR+ )
96		2nn0 10194	. . . . . . . . . . . . . 14 |- 2 e. NN0
97		eluznn0 10502	. . . . . . . . . . . . . 14 |- ( ( 2 e. NN0 /\ k e. ( ZZ>= ` 2 ) ) -> k e. NN0 )
98	96, 97	mpan 652	. . . . . . . . . . . . 13 |- ( k e. ( ZZ>= ` 2 ) -> k e. NN0 )
99		nnexpcl 11349	. . . . . . . . . . . . 13 |- ( ( P e. NN /\ k e. NN0 ) -> ( P ^ k ) e. NN )
100	10, 98, 99	syl2an 464	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( P ^ k ) e. NN )
101	100	nnrpd 10603	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( P ^ k ) e. RR+ )
102	95, 101	rpdivcld 10621	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. RR+ )
103	102	rpge0d 10608	. . . . . . . . 9 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> 0 <_ ( ( 2 x. N ) / ( P ^ k ) ) )
104	47	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 2 x. N ) e. RR )
105		remulcl 9031	. . . . . . . . . . . . . . 15 |- ( ( 3 e. RR /\ P e. RR ) -> ( 3 x. P ) e. RR )
106	48, 24, 105	sylancr 645	. . . . . . . . . . . . . 14 |- ( ph -> ( 3 x. P ) e. RR )
107	106	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 3 x. P ) e. RR )
108	100	nnred 9971	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( P ^ k ) e. RR )
109		ltdivmul 9838	. . . . . . . . . . . . . . . . 17 |- ( ( ( 2 x. N ) e. RR /\ P e. RR /\ ( 3 e. RR /\ 0 < 3 ) ) -> ( ( ( 2 x. N ) / 3 ) < P <-> ( 2 x. N ) < ( 3 x. P ) ) )
110	50, 109	mp3an3 1268	. . . . . . . . . . . . . . . 16 |- ( ( ( 2 x. N ) e. RR /\ P e. RR ) -> ( ( ( 2 x. N ) / 3 ) < P <-> ( 2 x. N ) < ( 3 x. P ) ) )
111	47, 24, 110	syl2anc 643	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ( 2 x. N ) / 3 ) < P <-> ( 2 x. N ) < ( 3 x. P ) ) )
112	43, 111	mpbid 202	. . . . . . . . . . . . . 14 |- ( ph -> ( 2 x. N ) < ( 3 x. P ) )
113	112	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 2 x. N ) < ( 3 x. P ) )
114	24, 24	remulcld 9072	. . . . . . . . . . . . . . 15 |- ( ph -> ( P x. P ) e. RR )
115	114	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( P x. P ) e. RR )
116		bposlem2.3	. . . . . . . . . . . . . . . . . 18 |- ( ph -> 2 < P )
117		nnltp1le 10286	. . . . . . . . . . . . . . . . . . 19 |- ( ( 2 e. NN /\ P e. NN ) -> ( 2 < P <-> ( 2 + 1 ) <_ P ) )
118	44, 10, 117	sylancr 645	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( 2 < P <-> ( 2 + 1 ) <_ P ) )
119	116, 118	mpbid 202	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( 2 + 1 ) <_ P )
120	55, 119	syl5eqbr 4205	. . . . . . . . . . . . . . . 16 |- ( ph -> 3 <_ P )
121		lemul1 9818	. . . . . . . . . . . . . . . . . 18 |- ( ( 3 e. RR /\ P e. RR /\ ( P e. RR /\ 0 < P ) ) -> ( 3 <_ P <-> ( 3 x. P ) <_ ( P x. P ) ) )
122	48, 121	mp3an1 1266	. . . . . . . . . . . . . . . . 17 |- ( ( P e. RR /\ ( P e. RR /\ 0 < P ) ) -> ( 3 <_ P <-> ( 3 x. P ) <_ ( P x. P ) ) )
123	24, 24, 25, 122	syl12anc 1182	. . . . . . . . . . . . . . . 16 |- ( ph -> ( 3 <_ P <-> ( 3 x. P ) <_ ( P x. P ) ) )
124	120, 123	mpbid 202	. . . . . . . . . . . . . . 15 |- ( ph -> ( 3 x. P ) <_ ( P x. P ) )
125	124	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 3 x. P ) <_ ( P x. P ) )
126	11	sqvald 11475	. . . . . . . . . . . . . . . 16 |- ( ph -> ( P ^ 2 ) = ( P x. P ) )
127	126	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( P ^ 2 ) = ( P x. P ) )
128	24	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> P e. RR )
129	10	nnge1d 9998	. . . . . . . . . . . . . . . . 17 |- ( ph -> 1 <_ P )
130	129	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> 1 <_ P )
131		simpr 448	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> k e. ( ZZ>= ` 2 ) )
132	128, 130, 131	leexp2ad 11510	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( P ^ 2 ) <_ ( P ^ k ) )
133	127, 132	eqbrtrrd 4194	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( P x. P ) <_ ( P ^ k ) )
134	107, 115, 108, 125, 133	letrd 9183	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 3 x. P ) <_ ( P ^ k ) )
135	104, 107, 108, 113, 134	ltletrd 9186	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 2 x. N ) < ( P ^ k ) )
136	100	nncnd 9972	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( P ^ k ) e. CC )
137	136	mulid1d 9061	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( P ^ k ) x. 1 ) = ( P ^ k ) )
138	135, 137	breqtrrd 4198	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 2 x. N ) < ( ( P ^ k ) x. 1 ) )
139	21	a1i 11	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> 1 e. RR )
140	104, 139, 101	ltdivmuld 10651	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( ( 2 x. N ) / ( P ^ k ) ) < 1 <-> ( 2 x. N ) < ( ( P ^ k ) x. 1 ) ) )
141	138, 140	mpbird 224	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) < 1 )
142		1e0p1 10366	. . . . . . . . . 10 |- 1 = ( 0 + 1 )
143	141, 142	syl6breq 4211	. . . . . . . . 9 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) < ( 0 + 1 ) )
144	102	rpred 10604	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( 2 x. N ) / ( P ^ k ) ) e. RR )
145		0z 10249	. . . . . . . . . 10 |- 0 e. ZZ
146		flbi 11178	. . . . . . . . . 10 |- ( ( ( ( 2 x. N ) / ( P ^ k ) ) e. RR /\ 0 e. ZZ ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) = 0 <-> ( 0 <_ ( ( 2 x. N ) / ( P ^ k ) ) /\ ( ( 2 x. N ) / ( P ^ k ) ) < ( 0 + 1 ) ) ) )
147	144, 145, 146	sylancl 644	. . . . . . . . 9 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) = 0 <-> ( 0 <_ ( ( 2 x. N ) / ( P ^ k ) ) /\ ( ( 2 x. N ) / ( P ^ k ) ) < ( 0 + 1 ) ) ) )
148	103, 143, 147	mpbir2and 889	. . . . . . . 8 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) = 0 )
149	1	nnrpd 10603	. . . . . . . . . . . . . 14 |- ( ph -> N e. RR+ )
150	149	adantr 452	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> N e. RR+ )
151	150, 101	rpdivcld 10621	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( N / ( P ^ k ) ) e. RR+ )
152	151	rpge0d 10608	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> 0 <_ ( N / ( P ^ k ) ) )
153	23	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> N e. RR )
154	23, 149	ltaddrpd 10633	. . . . . . . . . . . . . . . . 17 |- ( ph -> N < ( N + N ) )
155	39	2timesd 10166	. . . . . . . . . . . . . . . . 17 |- ( ph -> ( 2 x. N ) = ( N + N ) )
156	154, 155	breqtrrd 4198	. . . . . . . . . . . . . . . 16 |- ( ph -> N < ( 2 x. N ) )
157	156	adantr 452	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> N < ( 2 x. N ) )
158	153, 104, 108, 157, 135	lttrd 9187	. . . . . . . . . . . . . 14 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> N < ( P ^ k ) )
159	158, 137	breqtrrd 4198	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> N < ( ( P ^ k ) x. 1 ) )
160	153, 139, 101	ltdivmuld 10651	. . . . . . . . . . . . 13 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( N / ( P ^ k ) ) < 1 <-> N < ( ( P ^ k ) x. 1 ) ) )
161	159, 160	mpbird 224	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( N / ( P ^ k ) ) < 1 )
162	161, 142	syl6breq 4211	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( N / ( P ^ k ) ) < ( 0 + 1 ) )
163	151	rpred 10604	. . . . . . . . . . . 12 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( N / ( P ^ k ) ) e. RR )
164		flbi 11178	. . . . . . . . . . . 12 |- ( ( ( N / ( P ^ k ) ) e. RR /\ 0 e. ZZ ) -> ( ( |_ ` ( N / ( P ^ k ) ) ) = 0 <-> ( 0 <_ ( N / ( P ^ k ) ) /\ ( N / ( P ^ k ) ) < ( 0 + 1 ) ) ) )
165	163, 145, 164	sylancl 644	. . . . . . . . . . 11 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( |_ ` ( N / ( P ^ k ) ) ) = 0 <-> ( 0 <_ ( N / ( P ^ k ) ) /\ ( N / ( P ^ k ) ) < ( 0 + 1 ) ) ) )
166	152, 162, 165	mpbir2and 889	. . . . . . . . . 10 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( |_ ` ( N / ( P ^ k ) ) ) = 0 )
167	166	oveq2d 6056	. . . . . . . . 9 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) = ( 2 x. 0 ) )
168	16	mul01i 9212	. . . . . . . . 9 |- ( 2 x. 0 ) = 0
169	167, 168	syl6eq 2452	. . . . . . . 8 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) = 0 )
170	148, 169	oveq12d 6058	. . . . . . 7 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = ( 0 - 0 ) )
171		0cn 9040	. . . . . . . 8 |- 0 e. CC
172	171	subidi 9327	. . . . . . 7 |- ( 0 - 0 ) = 0
173	170, 172	syl6eq 2452	. . . . . 6 |- ( ( ph /\ k e. ( ZZ>= ` 2 ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = 0 )
174	93, 173	jaodan 761	. . . . 5 |- ( ( ph /\ ( k = 1 \/ k e. ( ZZ>= ` 2 ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = 0 )
175	7, 174	sylan2 461	. . . 4 |- ( ( ph /\ k e. ( 1 ... ( 2 x. N ) ) ) -> ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = 0 )
176	175	sumeq2dv 12452	. . 3 |- ( ph -> sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = sum_ k e. ( 1 ... ( 2 x. N ) ) 0 )
177		fzfid 11267	. . . 4 |- ( ph -> ( 1 ... ( 2 x. N ) ) e. Fin )
178		sumz 12471	. . . . 5 |- ( ( ( 1 ... ( 2 x. N ) ) C_ ( ZZ>= ` 1 ) \/ ( 1 ... ( 2 x. N ) ) e. Fin ) -> sum_ k e. ( 1 ... ( 2 x. N ) ) 0 = 0 )
179	178	olcs 385	. . . 4 |- ( ( 1 ... ( 2 x. N ) ) e. Fin -> sum_ k e. ( 1 ... ( 2 x. N ) ) 0 = 0 )
180	177, 179	syl 16	. . 3 |- ( ph -> sum_ k e. ( 1 ... ( 2 x. N ) ) 0 = 0 )
181	176, 180	eqtrd 2436	. 2 |- ( ph -> sum_ k e. ( 1 ... ( 2 x. N ) ) ( ( |_ ` ( ( 2 x. N ) / ( P ^ k ) ) ) - ( 2 x. ( |_ ` ( N / ( P ^ k ) ) ) ) ) = 0 )
182	4, 181	eqtrd 2436	1 |- ( ph -> ( P pCnt ( ( 2 x. N ) _C N ) ) = 0 )

Syntax hints:   -> wi 4   <-> wb 177   \/ wo 358   /\ wa 359   = wceq 1649   e. wcel 1721   C_ wss 3280   class class class wbr 4172   ` cfv 5413  (class class class)co 6040   Fincfn 7068   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   + caddc 8949   x. cmul 8951   < clt 9076   <_ cle 9077   - cmin 9247   / cdiv 9633   NNcn 9956   2c2 10005   3c3 10006   4c4 10007   NN0cn0 10177   ZZcz 10238   ZZ>=cuz 10444   RR+crp 10568   ...cfz 10999   |_cfl 11156   ^cexp 11337   _C cbc 11548   sum_csu 12434   Primecprime 13034   pCnt cpc 13165

This theorem is referenced by:  bposlem3  21023

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-rep 4280  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-inf2 7552  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-int 4011  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-se 4502  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-isom 5422  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-1st 6308  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-1o 6683  df-2o 6684  df-oadd 6687  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-fin 7072  df-sup 7404  df-oi 7435  df-card 7782  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-3 10015  df-4 10016  df-n0 10178  df-z 10239  df-uz 10445  df-q 10531  df-rp 10569  df-fz 11000  df-fzo 11091  df-fl 11157  df-mod 11206  df-seq 11279  df-exp 11338  df-fac 11522  df-bc 11549  df-hash 11574  df-cj 11859  df-re 11860  df-im 11861  df-sqr 11995  df-abs 11996  df-clim 12237  df-sum 12435  df-dvds 12808  df-gcd 12962  df-prm 13035  df-pc 13166