bposlem2

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)

	Ref	Expression
Hypotheses	bposlem2.1	$⊢ φ \to N \in ℕ$
	bposlem2.2	$⊢ φ \to P \in ℙ$
	bposlem2.3	$⊢ φ \to 2 < P$
	bposlem2.4	$⊢ φ \to \frac{2 \cdot N}{3} < P$
	bposlem2.5	$⊢ φ \to P \leq N$
Assertion	bposlem2	$⊢ φ \to P pCnt (\binom{2 \cdot N}{N}) = 0$

Proof

Step	Hyp	Ref	Expression
1		bposlem2.1	$⊢ φ \to N \in ℕ$
2		bposlem2.2	$⊢ φ \to P \in ℙ$
3		bposlem2.3	$⊢ φ \to 2 < P$
4		bposlem2.4	$⊢ φ \to \frac{2 \cdot N}{3} < P$
5		bposlem2.5	$⊢ φ \to P \leq N$
6		pcbcctr	$⊢ (N \in ℕ \land P \in ℙ) \to P pCnt (\binom{2 \cdot N}{N}) = \sum_{k = 1}^{2 \cdot N} (⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋)$
7	1 2 6	syl2anc	$⊢ φ \to P pCnt (\binom{2 \cdot N}{N}) = \sum_{k = 1}^{2 \cdot N} (⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋)$
8		elfznn	$⊢ k \in (1 \dots 2 \cdot N) \to k \in ℕ$
9		elnn1uz2	$⊢ k \in ℕ \leftrightarrow (k = 1 \lor k \in ℤ_{\geq 2})$
10	8 9	sylib	$⊢ k \in (1 \dots 2 \cdot N) \to (k = 1 \lor k \in ℤ_{\geq 2})$
11		oveq2	$⊢ k = 1 \to P^{k} = P^{1}$
12		prmnn	$⊢ P \in ℙ \to P \in ℕ$
13	2 12	syl	$⊢ φ \to P \in ℕ$
14	13	nncnd	$⊢ φ \to P \in ℂ$
15	14	exp1d	$⊢ φ \to P^{1} = P$
16	11 15	sylan9eqr	$⊢ (φ \land k = 1) \to P^{k} = P$
17	16	oveq2d	$⊢ (φ \land k = 1) \to \frac{2 \cdot N}{P^{k}} = \frac{2 \cdot N}{P}$
18	17	fveq2d	$⊢ (φ \land k = 1) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ = ⌊\frac{2 \cdot N}{P}⌋$
19		2t1e2	$⊢ 2 \cdot 1 = 2$
20	14	mulid2d	$⊢ φ \to 1 P = P$
21	20 5	eqbrtrd	$⊢ φ \to 1 P \leq N$
22		1red	$⊢ φ \to 1 \in ℝ$
23	1	nnred	$⊢ φ \to N \in ℝ$
24	13	nnred	$⊢ φ \to P \in ℝ$
25	13	nngt0d	$⊢ φ \to 0 < P$
26		lemuldiv	$⊢ (1 \in ℝ \land N \in ℝ \land (P \in ℝ \land 0 < P)) \to (1 P \leq N \leftrightarrow 1 \leq \frac{N}{P})$
27	22 23 24 25 26	syl112anc	$⊢ φ \to (1 P \leq N \leftrightarrow 1 \leq \frac{N}{P})$
28	21 27	mpbid	$⊢ φ \to 1 \leq \frac{N}{P}$
29	23 13	nndivred	$⊢ φ \to \frac{N}{P} \in ℝ$
30		1re	$⊢ 1 \in ℝ$
31		2re	$⊢ 2 \in ℝ$
32		2pos	$⊢ 0 < 2$
33	31 32	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
34		lemul2	$⊢ (1 \in ℝ \land \frac{N}{P} \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (1 \leq \frac{N}{P} \leftrightarrow 2 \cdot 1 \leq 2 (\frac{N}{P}))$
35	30 33 34	mp3an13	$⊢ \frac{N}{P} \in ℝ \to (1 \leq \frac{N}{P} \leftrightarrow 2 \cdot 1 \leq 2 (\frac{N}{P}))$
36	29 35	syl	$⊢ φ \to (1 \leq \frac{N}{P} \leftrightarrow 2 \cdot 1 \leq 2 (\frac{N}{P}))$
37	28 36	mpbid	$⊢ φ \to 2 \cdot 1 \leq 2 (\frac{N}{P})$
38	19 37	eqbrtrrid	$⊢ φ \to 2 \leq 2 (\frac{N}{P})$
39		2cnd	$⊢ φ \to 2 \in ℂ$
40	1	nncnd	$⊢ φ \to N \in ℂ$
41	13	nnne0d	$⊢ φ \to P \neq 0$
42	39 40 14 41	divassd	$⊢ φ \to \frac{2 \cdot N}{P} = 2 (\frac{N}{P})$
43	38 42	breqtrrd	$⊢ φ \to 2 \leq \frac{2 \cdot N}{P}$
44		2nn	$⊢ 2 \in ℕ$
45		nnmulcl	$⊢ (2 \in ℕ \land N \in ℕ) \to 2 \cdot N \in ℕ$
46	44 1 45	sylancr	$⊢ φ \to 2 \cdot N \in ℕ$
47	46	nnred	$⊢ φ \to 2 \cdot N \in ℝ$
48		3re	$⊢ 3 \in ℝ$
49		3pos	$⊢ 0 < 3$
50	48 49	pm3.2i	$⊢ (3 \in ℝ \land 0 < 3)$
51		ltdiv23	$⊢ (2 \cdot N \in ℝ \land (3 \in ℝ \land 0 < 3) \land (P \in ℝ \land 0 < P)) \to (\frac{2 \cdot N}{3} < P \leftrightarrow \frac{2 \cdot N}{P} < 3)$
52	50 51	mp3an2	$⊢ (2 \cdot N \in ℝ \land (P \in ℝ \land 0 < P)) \to (\frac{2 \cdot N}{3} < P \leftrightarrow \frac{2 \cdot N}{P} < 3)$
53	47 24 25 52	syl12anc	$⊢ φ \to (\frac{2 \cdot N}{3} < P \leftrightarrow \frac{2 \cdot N}{P} < 3)$
54	4 53	mpbid	$⊢ φ \to \frac{2 \cdot N}{P} < 3$
55		df-3	$⊢ 3 = 2 + 1$
56	54 55	breqtrdi	$⊢ φ \to \frac{2 \cdot N}{P} < 2 + 1$
57	47 13	nndivred	$⊢ φ \to \frac{2 \cdot N}{P} \in ℝ$
58		2z	$⊢ 2 \in ℤ$
59		flbi	$⊢ (\frac{2 \cdot N}{P} \in ℝ \land 2 \in ℤ) \to (⌊\frac{2 \cdot N}{P}⌋ = 2 \leftrightarrow (2 \leq \frac{2 \cdot N}{P} \land \frac{2 \cdot N}{P} < 2 + 1))$
60	57 58 59	sylancl	$⊢ φ \to (⌊\frac{2 \cdot N}{P}⌋ = 2 \leftrightarrow (2 \leq \frac{2 \cdot N}{P} \land \frac{2 \cdot N}{P} < 2 + 1))$
61	43 56 60	mpbir2and	$⊢ φ \to ⌊\frac{2 \cdot N}{P}⌋ = 2$
62	61	adantr	$⊢ (φ \land k = 1) \to ⌊\frac{2 \cdot N}{P}⌋ = 2$
63	18 62	eqtrd	$⊢ (φ \land k = 1) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ = 2$
64	16	oveq2d	$⊢ (φ \land k = 1) \to \frac{N}{P^{k}} = \frac{N}{P}$
65	64	fveq2d	$⊢ (φ \land k = 1) \to ⌊\frac{N}{P^{k}}⌋ = ⌊\frac{N}{P}⌋$
66		remulcl	$⊢ (2 \in ℝ \land \frac{N}{P} \in ℝ) \to 2 (\frac{N}{P}) \in ℝ$
67	31 29 66	sylancr	$⊢ φ \to 2 (\frac{N}{P}) \in ℝ$
68	48	a1i	$⊢ φ \to 3 \in ℝ$
69		4re	$⊢ 4 \in ℝ$
70	69	a1i	$⊢ φ \to 4 \in ℝ$
71	42 54	eqbrtrrd	$⊢ φ \to 2 (\frac{N}{P}) < 3$
72		3lt4	$⊢ 3 < 4$
73	72	a1i	$⊢ φ \to 3 < 4$
74	67 68 70 71 73	lttrd	$⊢ φ \to 2 (\frac{N}{P}) < 4$
75		2t2e4	$⊢ 2 \cdot 2 = 4$
76	74 75	breqtrrdi	$⊢ φ \to 2 (\frac{N}{P}) < 2 \cdot 2$
77		ltmul2	$⊢ (\frac{N}{P} \in ℝ \land 2 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (\frac{N}{P} < 2 \leftrightarrow 2 (\frac{N}{P}) < 2 \cdot 2)$
78	31 33 77	mp3an23	$⊢ \frac{N}{P} \in ℝ \to (\frac{N}{P} < 2 \leftrightarrow 2 (\frac{N}{P}) < 2 \cdot 2)$
79	29 78	syl	$⊢ φ \to (\frac{N}{P} < 2 \leftrightarrow 2 (\frac{N}{P}) < 2 \cdot 2)$
80	76 79	mpbird	$⊢ φ \to \frac{N}{P} < 2$
81		df-2	$⊢ 2 = 1 + 1$
82	80 81	breqtrdi	$⊢ φ \to \frac{N}{P} < 1 + 1$
83		1z	$⊢ 1 \in ℤ$
84		flbi	$⊢ (\frac{N}{P} \in ℝ \land 1 \in ℤ) \to (⌊\frac{N}{P}⌋ = 1 \leftrightarrow (1 \leq \frac{N}{P} \land \frac{N}{P} < 1 + 1))$
85	29 83 84	sylancl	$⊢ φ \to (⌊\frac{N}{P}⌋ = 1 \leftrightarrow (1 \leq \frac{N}{P} \land \frac{N}{P} < 1 + 1))$
86	28 82 85	mpbir2and	$⊢ φ \to ⌊\frac{N}{P}⌋ = 1$
87	86	adantr	$⊢ (φ \land k = 1) \to ⌊\frac{N}{P}⌋ = 1$
88	65 87	eqtrd	$⊢ (φ \land k = 1) \to ⌊\frac{N}{P^{k}}⌋ = 1$
89	88	oveq2d	$⊢ (φ \land k = 1) \to 2 ⌊\frac{N}{P^{k}}⌋ = 2 \cdot 1$
90	89 19	eqtrdi	$⊢ (φ \land k = 1) \to 2 ⌊\frac{N}{P^{k}}⌋ = 2$
91	63 90	oveq12d	$⊢ (φ \land k = 1) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ = 2 - 2$
92		2cn	$⊢ 2 \in ℂ$
93	92	subidi	$⊢ 2 - 2 = 0$
94	91 93	eqtrdi	$⊢ (φ \land k = 1) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ = 0$
95	46	nnrpd	$⊢ φ \to 2 \cdot N \in ℝ^{+}$
96	95	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 2 \cdot N \in ℝ^{+}$
97		eluzge2nn0	$⊢ k \in ℤ_{\geq 2} \to k \in ℕ_{0}$
98		nnexpcl	$⊢ (P \in ℕ \land k \in ℕ_{0}) \to P^{k} \in ℕ$
99	13 97 98	syl2an	$⊢ (φ \land k \in ℤ_{\geq 2}) \to P^{k} \in ℕ$
100	99	nnrpd	$⊢ (φ \land k \in ℤ_{\geq 2}) \to P^{k} \in ℝ^{+}$
101	96 100	rpdivcld	$⊢ (φ \land k \in ℤ_{\geq 2}) \to \frac{2 \cdot N}{P^{k}} \in ℝ^{+}$
102	101	rpge0d	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 0 \leq \frac{2 \cdot N}{P^{k}}$
103	47	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 2 \cdot N \in ℝ$
104		remulcl	$⊢ (3 \in ℝ \land P \in ℝ) \to 3 P \in ℝ$
105	48 24 104	sylancr	$⊢ φ \to 3 P \in ℝ$
106	105	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 3 P \in ℝ$
107	99	nnred	$⊢ (φ \land k \in ℤ_{\geq 2}) \to P^{k} \in ℝ$
108		ltdivmul	$⊢ (2 \cdot N \in ℝ \land P \in ℝ \land (3 \in ℝ \land 0 < 3)) \to (\frac{2 \cdot N}{3} < P \leftrightarrow 2 \cdot N < 3 P)$
109	50 108	mp3an3	$⊢ (2 \cdot N \in ℝ \land P \in ℝ) \to (\frac{2 \cdot N}{3} < P \leftrightarrow 2 \cdot N < 3 P)$
110	47 24 109	syl2anc	$⊢ φ \to (\frac{2 \cdot N}{3} < P \leftrightarrow 2 \cdot N < 3 P)$
111	4 110	mpbid	$⊢ φ \to 2 \cdot N < 3 P$
112	111	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 2 \cdot N < 3 P$
113	24 24	remulcld	$⊢ φ \to P P \in ℝ$
114	113	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to P P \in ℝ$
115		nnltp1le	$⊢ (2 \in ℕ \land P \in ℕ) \to (2 < P \leftrightarrow 2 + 1 \leq P)$
116	44 13 115	sylancr	$⊢ φ \to (2 < P \leftrightarrow 2 + 1 \leq P)$
117	3 116	mpbid	$⊢ φ \to 2 + 1 \leq P$
118	55 117	eqbrtrid	$⊢ φ \to 3 \leq P$
119		lemul1	$⊢ (3 \in ℝ \land P \in ℝ \land (P \in ℝ \land 0 < P)) \to (3 \leq P \leftrightarrow 3 P \leq P P)$
120	48 119	mp3an1	$⊢ (P \in ℝ \land (P \in ℝ \land 0 < P)) \to (3 \leq P \leftrightarrow 3 P \leq P P)$
121	24 24 25 120	syl12anc	$⊢ φ \to (3 \leq P \leftrightarrow 3 P \leq P P)$
122	118 121	mpbid	$⊢ φ \to 3 P \leq P P$
123	122	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 3 P \leq P P$
124	14	sqvald	$⊢ φ \to P^{2} = P P$
125	124	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to P^{2} = P P$
126	24	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to P \in ℝ$
127	13	nnge1d	$⊢ φ \to 1 \leq P$
128	127	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 1 \leq P$
129		simpr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to k \in ℤ_{\geq 2}$
130	126 128 129	leexp2ad	$⊢ (φ \land k \in ℤ_{\geq 2}) \to P^{2} \leq P^{k}$
131	125 130	eqbrtrrd	$⊢ (φ \land k \in ℤ_{\geq 2}) \to P P \leq P^{k}$
132	106 114 107 123 131	letrd	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 3 P \leq P^{k}$
133	103 106 107 112 132	ltletrd	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 2 \cdot N < P^{k}$
134	99	nncnd	$⊢ (φ \land k \in ℤ_{\geq 2}) \to P^{k} \in ℂ$
135	134	mulid1d	$⊢ (φ \land k \in ℤ_{\geq 2}) \to P^{k} \cdot 1 = P^{k}$
136	133 135	breqtrrd	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 2 \cdot N < P^{k} \cdot 1$
137		1red	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 1 \in ℝ$
138	103 137 100	ltdivmuld	$⊢ (φ \land k \in ℤ_{\geq 2}) \to (\frac{2 \cdot N}{P^{k}} < 1 \leftrightarrow 2 \cdot N < P^{k} \cdot 1)$
139	136 138	mpbird	$⊢ (φ \land k \in ℤ_{\geq 2}) \to \frac{2 \cdot N}{P^{k}} < 1$
140		1e0p1	$⊢ 1 = 0 + 1$
141	139 140	breqtrdi	$⊢ (φ \land k \in ℤ_{\geq 2}) \to \frac{2 \cdot N}{P^{k}} < 0 + 1$
142	101	rpred	$⊢ (φ \land k \in ℤ_{\geq 2}) \to \frac{2 \cdot N}{P^{k}} \in ℝ$
143		0z	$⊢ 0 \in ℤ$
144		flbi	$⊢ (\frac{2 \cdot N}{P^{k}} \in ℝ \land 0 \in ℤ) \to (⌊\frac{2 \cdot N}{P^{k}}⌋ = 0 \leftrightarrow (0 \leq \frac{2 \cdot N}{P^{k}} \land \frac{2 \cdot N}{P^{k}} < 0 + 1))$
145	142 143 144	sylancl	$⊢ (φ \land k \in ℤ_{\geq 2}) \to (⌊\frac{2 \cdot N}{P^{k}}⌋ = 0 \leftrightarrow (0 \leq \frac{2 \cdot N}{P^{k}} \land \frac{2 \cdot N}{P^{k}} < 0 + 1))$
146	102 141 145	mpbir2and	$⊢ (φ \land k \in ℤ_{\geq 2}) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ = 0$
147	1	nnrpd	$⊢ φ \to N \in ℝ^{+}$
148	147	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to N \in ℝ^{+}$
149	148 100	rpdivcld	$⊢ (φ \land k \in ℤ_{\geq 2}) \to \frac{N}{P^{k}} \in ℝ^{+}$
150	149	rpge0d	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 0 \leq \frac{N}{P^{k}}$
151	23	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to N \in ℝ$
152	23 147	ltaddrpd	$⊢ φ \to N < N + N$
153	40	2timesd	$⊢ φ \to 2 \cdot N = N + N$
154	152 153	breqtrrd	$⊢ φ \to N < 2 \cdot N$
155	154	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to N < 2 \cdot N$
156	151 103 107 155 133	lttrd	$⊢ (φ \land k \in ℤ_{\geq 2}) \to N < P^{k}$
157	156 135	breqtrrd	$⊢ (φ \land k \in ℤ_{\geq 2}) \to N < P^{k} \cdot 1$
158	151 137 100	ltdivmuld	$⊢ (φ \land k \in ℤ_{\geq 2}) \to (\frac{N}{P^{k}} < 1 \leftrightarrow N < P^{k} \cdot 1)$
159	157 158	mpbird	$⊢ (φ \land k \in ℤ_{\geq 2}) \to \frac{N}{P^{k}} < 1$
160	159 140	breqtrdi	$⊢ (φ \land k \in ℤ_{\geq 2}) \to \frac{N}{P^{k}} < 0 + 1$
161	149	rpred	$⊢ (φ \land k \in ℤ_{\geq 2}) \to \frac{N}{P^{k}} \in ℝ$
162		flbi	$⊢ (\frac{N}{P^{k}} \in ℝ \land 0 \in ℤ) \to (⌊\frac{N}{P^{k}}⌋ = 0 \leftrightarrow (0 \leq \frac{N}{P^{k}} \land \frac{N}{P^{k}} < 0 + 1))$
163	161 143 162	sylancl	$⊢ (φ \land k \in ℤ_{\geq 2}) \to (⌊\frac{N}{P^{k}}⌋ = 0 \leftrightarrow (0 \leq \frac{N}{P^{k}} \land \frac{N}{P^{k}} < 0 + 1))$
164	150 160 163	mpbir2and	$⊢ (φ \land k \in ℤ_{\geq 2}) \to ⌊\frac{N}{P^{k}}⌋ = 0$
165	164	oveq2d	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 2 ⌊\frac{N}{P^{k}}⌋ = 2 \cdot 0$
166		2t0e0	$⊢ 2 \cdot 0 = 0$
167	165 166	eqtrdi	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 2 ⌊\frac{N}{P^{k}}⌋ = 0$
168	146 167	oveq12d	$⊢ (φ \land k \in ℤ_{\geq 2}) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ = 0 - 0$
169		0m0e0	$⊢ 0 - 0 = 0$
170	168 169	eqtrdi	$⊢ (φ \land k \in ℤ_{\geq 2}) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ = 0$
171	94 170	jaodan	$⊢ (φ \land (k = 1 \lor k \in ℤ_{\geq 2})) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ = 0$
172	10 171	sylan2	$⊢ (φ \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ = 0$
173	172	sumeq2dv	$⊢ φ \to \sum_{k = 1}^{2 \cdot N} (⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋) = \sum_{k = 1}^{2 \cdot N} 0$
174		fzfid	$⊢ φ \to (1 \dots 2 \cdot N) \in Fin$
175		sumz	$⊢ ((1 \dots 2 \cdot N) \subseteq ℤ_{\geq 1} \lor (1 \dots 2 \cdot N) \in Fin) \to \sum_{k = 1}^{2 \cdot N} 0 = 0$
176	175	olcs	$⊢ (1 \dots 2 \cdot N) \in Fin \to \sum_{k = 1}^{2 \cdot N} 0 = 0$
177	174 176	syl	$⊢ φ \to \sum_{k = 1}^{2 \cdot N} 0 = 0$
178	173 177	eqtrd	$⊢ φ \to \sum_{k = 1}^{2 \cdot N} (⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋) = 0$
179	7 178	eqtrd	$⊢ φ \to P pCnt (\binom{2 \cdot N}{N}) = 0$

Metamath Proof Explorer

Theorem bposlem2

Proof