bposlem3

Description: Lemma for bpos . Since the binomial coefficient does not have any primes in the range ( 2 N / 3 , N ] or ( 2 N , +oo ) by bposlem2 and prmfac1 , respectively, and it does not have any in the range ( N , 2 N ] by hypothesis, the product of the primes up through 2 N / 3 must be sufficient to compose the whole binomial coefficient. (Contributed by Mario Carneiro, 13-Mar-2014)

	Ref	Expression
Hypotheses	bpos.1	$⊢ φ \to N \in ℤ_{\geq 5}$
	bpos.2	$⊢ φ \to \neg \exists p \in ℙ (N < p \land p \leq 2 \cdot N)$
	bpos.3	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, n^{n pCnt (\binom{2 \cdot N}{N})}, 1))$
	bpos.4	$⊢ K = ⌊\frac{2 \cdot N}{3}⌋$
Assertion	bposlem3	$⊢ φ \to seq 1 (\times F) (K) = (\binom{2 \cdot N}{N})$

Proof

Step	Hyp	Ref	Expression
1		bpos.1	$⊢ φ \to N \in ℤ_{\geq 5}$
2		bpos.2	$⊢ φ \to \neg \exists p \in ℙ (N < p \land p \leq 2 \cdot N)$
3		bpos.3	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, n^{n pCnt (\binom{2 \cdot N}{N})}, 1))$
4		bpos.4	$⊢ K = ⌊\frac{2 \cdot N}{3}⌋$
5		simpr	$⊢ (φ \land n \in ℙ) \to n \in ℙ$
6		5nn	$⊢ 5 \in ℕ$
7		eluznn	$⊢ (5 \in ℕ \land N \in ℤ_{\geq 5}) \to N \in ℕ$
8	6 1 7	sylancr	$⊢ φ \to N \in ℕ$
9	8	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
10		fzctr	$⊢ N \in ℕ_{0} \to N \in (0 \dots 2 \cdot N)$
11		bccl2	$⊢ N \in (0 \dots 2 \cdot N) \to (\binom{2 \cdot N}{N}) \in ℕ$
12	9 10 11	3syl	$⊢ φ \to (\binom{2 \cdot N}{N}) \in ℕ$
13	12	adantr	$⊢ (φ \land n \in ℙ) \to (\binom{2 \cdot N}{N}) \in ℕ$
14	5 13	pccld	$⊢ (φ \land n \in ℙ) \to n pCnt (\binom{2 \cdot N}{N}) \in ℕ_{0}$
15	14	ralrimiva	$⊢ φ \to \forall n \in ℙ n pCnt (\binom{2 \cdot N}{N}) \in ℕ_{0}$
16	15	adantr	$⊢ (φ \land p \in ℙ) \to \forall n \in ℙ n pCnt (\binom{2 \cdot N}{N}) \in ℕ_{0}$
17		2nn	$⊢ 2 \in ℕ$
18		nnmulcl	$⊢ (2 \in ℕ \land N \in ℕ) \to 2 \cdot N \in ℕ$
19	17 8 18	sylancr	$⊢ φ \to 2 \cdot N \in ℕ$
20	19	nnred	$⊢ φ \to 2 \cdot N \in ℝ$
21		3nn	$⊢ 3 \in ℕ$
22		nndivre	$⊢ (2 \cdot N \in ℝ \land 3 \in ℕ) \to \frac{2 \cdot N}{3} \in ℝ$
23	20 21 22	sylancl	$⊢ φ \to \frac{2 \cdot N}{3} \in ℝ$
24	23	flcld	$⊢ φ \to ⌊\frac{2 \cdot N}{3}⌋ \in ℤ$
25	4 24	eqeltrid	$⊢ φ \to K \in ℤ$
26		3re	$⊢ 3 \in ℝ$
27	26	a1i	$⊢ φ \to 3 \in ℝ$
28		5re	$⊢ 5 \in ℝ$
29	28	a1i	$⊢ φ \to 5 \in ℝ$
30	8	nnred	$⊢ φ \to N \in ℝ$
31		3lt5	$⊢ 3 < 5$
32	26 28 31	ltleii	$⊢ 3 \leq 5$
33	32	a1i	$⊢ φ \to 3 \leq 5$
34		eluzle	$⊢ N \in ℤ_{\geq 5} \to 5 \leq N$
35	1 34	syl	$⊢ φ \to 5 \leq N$
36	27 29 30 33 35	letrd	$⊢ φ \to 3 \leq N$
37		2re	$⊢ 2 \in ℝ$
38		2pos	$⊢ 0 < 2$
39	37 38	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
40		lemul2	$⊢ (3 \in ℝ \land N \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (3 \leq N \leftrightarrow 2 \cdot 3 \leq 2 \cdot N)$
41	26 39 40	mp3an13	$⊢ N \in ℝ \to (3 \leq N \leftrightarrow 2 \cdot 3 \leq 2 \cdot N)$
42	30 41	syl	$⊢ φ \to (3 \leq N \leftrightarrow 2 \cdot 3 \leq 2 \cdot N)$
43	36 42	mpbid	$⊢ φ \to 2 \cdot 3 \leq 2 \cdot N$
44		3pos	$⊢ 0 < 3$
45	26 44	pm3.2i	$⊢ (3 \in ℝ \land 0 < 3)$
46		lemuldiv	$⊢ (2 \in ℝ \land 2 \cdot N \in ℝ \land (3 \in ℝ \land 0 < 3)) \to (2 \cdot 3 \leq 2 \cdot N \leftrightarrow 2 \leq \frac{2 \cdot N}{3})$
47	37 45 46	mp3an13	$⊢ 2 \cdot N \in ℝ \to (2 \cdot 3 \leq 2 \cdot N \leftrightarrow 2 \leq \frac{2 \cdot N}{3})$
48	20 47	syl	$⊢ φ \to (2 \cdot 3 \leq 2 \cdot N \leftrightarrow 2 \leq \frac{2 \cdot N}{3})$
49	43 48	mpbid	$⊢ φ \to 2 \leq \frac{2 \cdot N}{3}$
50		2z	$⊢ 2 \in ℤ$
51		flge	$⊢ (\frac{2 \cdot N}{3} \in ℝ \land 2 \in ℤ) \to (2 \leq \frac{2 \cdot N}{3} \leftrightarrow 2 \leq ⌊\frac{2 \cdot N}{3}⌋)$
52	23 50 51	sylancl	$⊢ φ \to (2 \leq \frac{2 \cdot N}{3} \leftrightarrow 2 \leq ⌊\frac{2 \cdot N}{3}⌋)$
53	49 52	mpbid	$⊢ φ \to 2 \leq ⌊\frac{2 \cdot N}{3}⌋$
54	53 4	breqtrrdi	$⊢ φ \to 2 \leq K$
55	50	eluz1i	$⊢ K \in ℤ_{\geq 2} \leftrightarrow (K \in ℤ \land 2 \leq K)$
56	25 54 55	sylanbrc	$⊢ φ \to K \in ℤ_{\geq 2}$
57		eluz2nn	$⊢ K \in ℤ_{\geq 2} \to K \in ℕ$
58	56 57	syl	$⊢ φ \to K \in ℕ$
59	58	adantr	$⊢ (φ \land p \in ℙ) \to K \in ℕ$
60		simpr	$⊢ (φ \land p \in ℙ) \to p \in ℙ$
61		oveq1	$⊢ n = p \to n pCnt (\binom{2 \cdot N}{N}) = p pCnt (\binom{2 \cdot N}{N})$
62	3 16 59 60 61	pcmpt	$⊢ (φ \land p \in ℙ) \to p pCnt seq 1 (\times F) (K) = if (p \leq K, p pCnt (\binom{2 \cdot N}{N}), 0)$
63		iftrue	$⊢ p \leq K \to if (p \leq K, p pCnt (\binom{2 \cdot N}{N}), 0) = p pCnt (\binom{2 \cdot N}{N})$
64	63	adantl	$⊢ ((φ \land p \in ℙ) \land p \leq K) \to if (p \leq K, p pCnt (\binom{2 \cdot N}{N}), 0) = p pCnt (\binom{2 \cdot N}{N})$
65		iffalse	$⊢ \neg p \leq K \to if (p \leq K, p pCnt (\binom{2 \cdot N}{N}), 0) = 0$
66	65	adantl	$⊢ ((φ \land p \in ℙ) \land \neg p \leq K) \to if (p \leq K, p pCnt (\binom{2 \cdot N}{N}), 0) = 0$
67	25	zred	$⊢ φ \to K \in ℝ$
68		prmz	$⊢ p \in ℙ \to p \in ℤ$
69	68	zred	$⊢ p \in ℙ \to p \in ℝ$
70		ltnle	$⊢ (K \in ℝ \land p \in ℝ) \to (K < p \leftrightarrow \neg p \leq K)$
71	67 69 70	syl2an	$⊢ (φ \land p \in ℙ) \to (K < p \leftrightarrow \neg p \leq K)$
72	71	biimpar	$⊢ ((φ \land p \in ℙ) \land \neg p \leq K) \to K < p$
73	8	ad2antrr	$⊢ ((φ \land p \in ℙ) \land (K < p \land p \leq N)) \to N \in ℕ$
74		simplr	$⊢ ((φ \land p \in ℙ) \land (K < p \land p \leq N)) \to p \in ℙ$
75	37	a1i	$⊢ ((φ \land p \in ℙ) \land (K < p \land p \leq N)) \to 2 \in ℝ$
76	67	ad2antrr	$⊢ ((φ \land p \in ℙ) \land (K < p \land p \leq N)) \to K \in ℝ$
77	68	ad2antlr	$⊢ ((φ \land p \in ℙ) \land (K < p \land p \leq N)) \to p \in ℤ$
78	77	zred	$⊢ ((φ \land p \in ℙ) \land (K < p \land p \leq N)) \to p \in ℝ$
79	54	ad2antrr	$⊢ ((φ \land p \in ℙ) \land (K < p \land p \leq N)) \to 2 \leq K$
80		simprl	$⊢ ((φ \land p \in ℙ) \land (K < p \land p \leq N)) \to K < p$
81	75 76 78 79 80	lelttrd	$⊢ ((φ \land p \in ℙ) \land (K < p \land p \leq N)) \to 2 < p$
82	4 80	eqbrtrrid	$⊢ ((φ \land p \in ℙ) \land (K < p \land p \leq N)) \to ⌊\frac{2 \cdot N}{3}⌋ < p$
83	23	ad2antrr	$⊢ ((φ \land p \in ℙ) \land (K < p \land p \leq N)) \to \frac{2 \cdot N}{3} \in ℝ$
84		fllt	$⊢ (\frac{2 \cdot N}{3} \in ℝ \land p \in ℤ) \to (\frac{2 \cdot N}{3} < p \leftrightarrow ⌊\frac{2 \cdot N}{3}⌋ < p)$
85	83 77 84	syl2anc	$⊢ ((φ \land p \in ℙ) \land (K < p \land p \leq N)) \to (\frac{2 \cdot N}{3} < p \leftrightarrow ⌊\frac{2 \cdot N}{3}⌋ < p)$
86	82 85	mpbird	$⊢ ((φ \land p \in ℙ) \land (K < p \land p \leq N)) \to \frac{2 \cdot N}{3} < p$
87		simprr	$⊢ ((φ \land p \in ℙ) \land (K < p \land p \leq N)) \to p \leq N$
88	73 74 81 86 87	bposlem2	$⊢ ((φ \land p \in ℙ) \land (K < p \land p \leq N)) \to p pCnt (\binom{2 \cdot N}{N}) = 0$
89	88	expr	$⊢ ((φ \land p \in ℙ) \land K < p) \to (p \leq N \to p pCnt (\binom{2 \cdot N}{N}) = 0)$
90		rspe	$⊢ (p \in ℙ \land (N < p \land p \leq 2 \cdot N)) \to \exists p \in ℙ (N < p \land p \leq 2 \cdot N)$
91	90	adantll	$⊢ ((φ \land p \in ℙ) \land (N < p \land p \leq 2 \cdot N)) \to \exists p \in ℙ (N < p \land p \leq 2 \cdot N)$
92	2	ad2antrr	$⊢ ((φ \land p \in ℙ) \land (N < p \land p \leq 2 \cdot N)) \to \neg \exists p \in ℙ (N < p \land p \leq 2 \cdot N)$
93	91 92	pm2.21dd	$⊢ ((φ \land p \in ℙ) \land (N < p \land p \leq 2 \cdot N)) \to p pCnt (\binom{2 \cdot N}{N}) = 0$
94	93	expr	$⊢ ((φ \land p \in ℙ) \land N < p) \to (p \leq 2 \cdot N \to p pCnt (\binom{2 \cdot N}{N}) = 0)$
95	12	nnzd	$⊢ φ \to (\binom{2 \cdot N}{N}) \in ℤ$
96	9	faccld	$⊢ φ \to N! \in ℕ$
97	96 96	nnmulcld	$⊢ φ \to N! N! \in ℕ$
98	97	nnzd	$⊢ φ \to N! N! \in ℤ$
99		dvdsmul1	$⊢ ((\binom{2 \cdot N}{N}) \in ℤ \land N! N! \in ℤ) \to (\binom{2 \cdot N}{N}) ∥ (\binom{2 \cdot N}{N}) N! N!$
100	95 98 99	syl2anc	$⊢ φ \to (\binom{2 \cdot N}{N}) ∥ (\binom{2 \cdot N}{N}) N! N!$
101		bcctr	$⊢ N \in ℕ_{0} \to (\binom{2 \cdot N}{N}) = \frac{2 \cdot N!}{N! N!}$
102	9 101	syl	$⊢ φ \to (\binom{2 \cdot N}{N}) = \frac{2 \cdot N!}{N! N!}$
103	102	oveq1d	$⊢ φ \to (\binom{2 \cdot N}{N}) N! N! = (\frac{2 \cdot N!}{N! N!}) N! N!$
104	19	nnnn0d	$⊢ φ \to 2 \cdot N \in ℕ_{0}$
105	104	faccld	$⊢ φ \to 2 \cdot N! \in ℕ$
106	105	nncnd	$⊢ φ \to 2 \cdot N! \in ℂ$
107	97	nncnd	$⊢ φ \to N! N! \in ℂ$
108	97	nnne0d	$⊢ φ \to N! N! \neq 0$
109	106 107 108	divcan1d	$⊢ φ \to (\frac{2 \cdot N!}{N! N!}) N! N! = 2 \cdot N!$
110	103 109	eqtrd	$⊢ φ \to (\binom{2 \cdot N}{N}) N! N! = 2 \cdot N!$
111	100 110	breqtrd	$⊢ φ \to (\binom{2 \cdot N}{N}) ∥ 2 \cdot N!$
112	111	adantr	$⊢ (φ \land p \in ℙ) \to (\binom{2 \cdot N}{N}) ∥ 2 \cdot N!$
113	68	adantl	$⊢ (φ \land p \in ℙ) \to p \in ℤ$
114	95	adantr	$⊢ (φ \land p \in ℙ) \to (\binom{2 \cdot N}{N}) \in ℤ$
115	105	nnzd	$⊢ φ \to 2 \cdot N! \in ℤ$
116	115	adantr	$⊢ (φ \land p \in ℙ) \to 2 \cdot N! \in ℤ$
117		dvdstr	$⊢ (p \in ℤ \land (\binom{2 \cdot N}{N}) \in ℤ \land 2 \cdot N! \in ℤ) \to ((p ∥ (\binom{2 \cdot N}{N}) \land (\binom{2 \cdot N}{N}) ∥ 2 \cdot N!) \to p ∥ 2 \cdot N!)$
118	113 114 116 117	syl3anc	$⊢ (φ \land p \in ℙ) \to ((p ∥ (\binom{2 \cdot N}{N}) \land (\binom{2 \cdot N}{N}) ∥ 2 \cdot N!) \to p ∥ 2 \cdot N!)$
119	112 118	mpan2d	$⊢ (φ \land p \in ℙ) \to (p ∥ (\binom{2 \cdot N}{N}) \to p ∥ 2 \cdot N!)$
120		prmfac1	$⊢ (2 \cdot N \in ℕ_{0} \land p \in ℙ \land p ∥ 2 \cdot N!) \to p \leq 2 \cdot N$
121	120	3expia	$⊢ (2 \cdot N \in ℕ_{0} \land p \in ℙ) \to (p ∥ 2 \cdot N! \to p \leq 2 \cdot N)$
122	104 121	sylan	$⊢ (φ \land p \in ℙ) \to (p ∥ 2 \cdot N! \to p \leq 2 \cdot N)$
123	119 122	syld	$⊢ (φ \land p \in ℙ) \to (p ∥ (\binom{2 \cdot N}{N}) \to p \leq 2 \cdot N)$
124	123	con3d	$⊢ (φ \land p \in ℙ) \to (\neg p \leq 2 \cdot N \to \neg p ∥ (\binom{2 \cdot N}{N}))$
125		id	$⊢ p \in ℙ \to p \in ℙ$
126		pceq0	$⊢ (p \in ℙ \land (\binom{2 \cdot N}{N}) \in ℕ) \to (p pCnt (\binom{2 \cdot N}{N}) = 0 \leftrightarrow \neg p ∥ (\binom{2 \cdot N}{N}))$
127	125 12 126	syl2anr	$⊢ (φ \land p \in ℙ) \to (p pCnt (\binom{2 \cdot N}{N}) = 0 \leftrightarrow \neg p ∥ (\binom{2 \cdot N}{N}))$
128	124 127	sylibrd	$⊢ (φ \land p \in ℙ) \to (\neg p \leq 2 \cdot N \to p pCnt (\binom{2 \cdot N}{N}) = 0)$
129	128	adantr	$⊢ ((φ \land p \in ℙ) \land N < p) \to (\neg p \leq 2 \cdot N \to p pCnt (\binom{2 \cdot N}{N}) = 0)$
130	94 129	pm2.61d	$⊢ ((φ \land p \in ℙ) \land N < p) \to p pCnt (\binom{2 \cdot N}{N}) = 0$
131	130	ex	$⊢ (φ \land p \in ℙ) \to (N < p \to p pCnt (\binom{2 \cdot N}{N}) = 0)$
132	131	adantr	$⊢ ((φ \land p \in ℙ) \land K < p) \to (N < p \to p pCnt (\binom{2 \cdot N}{N}) = 0)$
133		lelttric	$⊢ (p \in ℝ \land N \in ℝ) \to (p \leq N \lor N < p)$
134	69 30 133	syl2anr	$⊢ (φ \land p \in ℙ) \to (p \leq N \lor N < p)$
135	134	adantr	$⊢ ((φ \land p \in ℙ) \land K < p) \to (p \leq N \lor N < p)$
136	89 132 135	mpjaod	$⊢ ((φ \land p \in ℙ) \land K < p) \to p pCnt (\binom{2 \cdot N}{N}) = 0$
137	72 136	syldan	$⊢ ((φ \land p \in ℙ) \land \neg p \leq K) \to p pCnt (\binom{2 \cdot N}{N}) = 0$
138	66 137	eqtr4d	$⊢ ((φ \land p \in ℙ) \land \neg p \leq K) \to if (p \leq K, p pCnt (\binom{2 \cdot N}{N}), 0) = p pCnt (\binom{2 \cdot N}{N})$
139	64 138	pm2.61dan	$⊢ (φ \land p \in ℙ) \to if (p \leq K, p pCnt (\binom{2 \cdot N}{N}), 0) = p pCnt (\binom{2 \cdot N}{N})$
140	62 139	eqtrd	$⊢ (φ \land p \in ℙ) \to p pCnt seq 1 (\times F) (K) = p pCnt (\binom{2 \cdot N}{N})$
141	140	ralrimiva	$⊢ φ \to \forall p \in ℙ p pCnt seq 1 (\times F) (K) = p pCnt (\binom{2 \cdot N}{N})$
142	3 15	pcmptcl	$⊢ φ \to (F : ℕ ⟶ ℕ \land seq 1 (\times F) : ℕ ⟶ ℕ)$
143	142	simprd	$⊢ φ \to seq 1 (\times F) : ℕ ⟶ ℕ$
144	143 58	ffvelcdmd	$⊢ φ \to seq 1 (\times F) (K) \in ℕ$
145	144	nnnn0d	$⊢ φ \to seq 1 (\times F) (K) \in ℕ_{0}$
146	12	nnnn0d	$⊢ φ \to (\binom{2 \cdot N}{N}) \in ℕ_{0}$
147		pc11	$⊢ (seq 1 (\times F) (K) \in ℕ_{0} \land (\binom{2 \cdot N}{N}) \in ℕ_{0}) \to (seq 1 (\times F) (K) = (\binom{2 \cdot N}{N}) \leftrightarrow \forall p \in ℙ p pCnt seq 1 (\times F) (K) = p pCnt (\binom{2 \cdot N}{N}))$
148	145 146 147	syl2anc	$⊢ φ \to (seq 1 (\times F) (K) = (\binom{2 \cdot N}{N}) \leftrightarrow \forall p \in ℙ p pCnt seq 1 (\times F) (K) = p pCnt (\binom{2 \cdot N}{N}))$
149	141 148	mpbird	$⊢ φ \to seq 1 (\times F) (K) = (\binom{2 \cdot N}{N})$

Metamath Proof Explorer

Theorem bposlem3

Proof