bposlem1

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

		Ref	Expression
	Assertion	bposlem1	$⊢ (N \in ℕ \land P \in ℙ) \to P^{P pCnt (\binom{2 \cdot N}{N})} \leq 2 \cdot N$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$⊢ (N \in ℕ \land P \in ℙ) \to (1 \dots 2 \cdot N) \in Fin$
2		2nn	$⊢ 2 \in ℕ$
3		nnmulcl	$⊢ (2 \in ℕ \land N \in ℕ) \to 2 \cdot N \in ℕ$
4	2 3	mpan	$⊢ N \in ℕ \to 2 \cdot N \in ℕ$
5	4	ad2antrr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 2 \cdot N \in ℕ$
6		prmnn	$⊢ P \in ℙ \to P \in ℕ$
7	6	ad2antlr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to P \in ℕ$
8		elfznn	$⊢ k \in (1 \dots 2 \cdot N) \to k \in ℕ$
9	8	adantl	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to k \in ℕ$
10	9	nnnn0d	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to k \in ℕ_{0}$
11	7 10	nnexpcld	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to P^{k} \in ℕ$
12		nnrp	$⊢ 2 \cdot N \in ℕ \to 2 \cdot N \in ℝ^{+}$
13		nnrp	$⊢ P^{k} \in ℕ \to P^{k} \in ℝ^{+}$
14		rpdivcl	$⊢ (2 \cdot N \in ℝ^{+} \land P^{k} \in ℝ^{+}) \to \frac{2 \cdot N}{P^{k}} \in ℝ^{+}$
15	12 13 14	syl2an	$⊢ (2 \cdot N \in ℕ \land P^{k} \in ℕ) \to \frac{2 \cdot N}{P^{k}} \in ℝ^{+}$
16	5 11 15	syl2anc	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to \frac{2 \cdot N}{P^{k}} \in ℝ^{+}$
17	16	rpred	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to \frac{2 \cdot N}{P^{k}} \in ℝ$
18	17	flcld	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ \in ℤ$
19		2z	$⊢ 2 \in ℤ$
20		simpll	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to N \in ℕ$
21		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
22		rpdivcl	$⊢ (N \in ℝ^{+} \land P^{k} \in ℝ^{+}) \to \frac{N}{P^{k}} \in ℝ^{+}$
23	21 13 22	syl2an	$⊢ (N \in ℕ \land P^{k} \in ℕ) \to \frac{N}{P^{k}} \in ℝ^{+}$
24	20 11 23	syl2anc	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to \frac{N}{P^{k}} \in ℝ^{+}$
25	24	rpred	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to \frac{N}{P^{k}} \in ℝ$
26	25	flcld	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{N}{P^{k}}⌋ \in ℤ$
27		zmulcl	$⊢ (2 \in ℤ \land ⌊\frac{N}{P^{k}}⌋ \in ℤ) \to 2 ⌊\frac{N}{P^{k}}⌋ \in ℤ$
28	19 26 27	sylancr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 2 ⌊\frac{N}{P^{k}}⌋ \in ℤ$
29	18 28	zsubcld	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \in ℤ$
30	29	zred	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \in ℝ$
31		1re	$⊢ 1 \in ℝ$
32		0re	$⊢ 0 \in ℝ$
33	31 32	ifcli	$⊢ if (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋), 1, 0) \in ℝ$
34	33	a1i	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to if (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋), 1, 0) \in ℝ$
35	28	zred	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 2 ⌊\frac{N}{P^{k}}⌋ \in ℝ$
36	17 35	resubcld	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (\frac{2 \cdot N}{P^{k}}) - 2 ⌊\frac{N}{P^{k}}⌋ \in ℝ$
37		2re	$⊢ 2 \in ℝ$
38	37	a1i	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 2 \in ℝ$
39	18	zred	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ \in ℝ$
40		flle	$⊢ \frac{2 \cdot N}{P^{k}} \in ℝ \to ⌊\frac{2 \cdot N}{P^{k}}⌋ \leq \frac{2 \cdot N}{P^{k}}$
41	17 40	syl	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ \leq \frac{2 \cdot N}{P^{k}}$
42	39 17 35 41	lesub1dd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \leq (\frac{2 \cdot N}{P^{k}}) - 2 ⌊\frac{N}{P^{k}}⌋$
43		resubcl	$⊢ (\frac{N}{P^{k}} \in ℝ \land 1 \in ℝ) \to (\frac{N}{P^{k}}) - 1 \in ℝ$
44	25 31 43	sylancl	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (\frac{N}{P^{k}}) - 1 \in ℝ$
45		remulcl	$⊢ (2 \in ℝ \land (\frac{N}{P^{k}}) - 1 \in ℝ) \to 2 ((\frac{N}{P^{k}}) - 1) \in ℝ$
46	37 44 45	sylancr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 2 ((\frac{N}{P^{k}}) - 1) \in ℝ$
47		flltp1	$⊢ \frac{N}{P^{k}} \in ℝ \to \frac{N}{P^{k}} < ⌊\frac{N}{P^{k}}⌋ + 1$
48	25 47	syl	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to \frac{N}{P^{k}} < ⌊\frac{N}{P^{k}}⌋ + 1$
49		1red	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 1 \in ℝ$
50	26	zred	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{N}{P^{k}}⌋ \in ℝ$
51	25 49 50	ltsubaddd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ((\frac{N}{P^{k}}) - 1 < ⌊\frac{N}{P^{k}}⌋ \leftrightarrow \frac{N}{P^{k}} < ⌊\frac{N}{P^{k}}⌋ + 1)$
52	48 51	mpbird	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (\frac{N}{P^{k}}) - 1 < ⌊\frac{N}{P^{k}}⌋$
53		2pos	$⊢ 0 < 2$
54	37 53	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
55		ltmul2	$⊢ ((\frac{N}{P^{k}}) - 1 \in ℝ \land ⌊\frac{N}{P^{k}}⌋ \in ℝ \land (2 \in ℝ \land 0 < 2)) \to ((\frac{N}{P^{k}}) - 1 < ⌊\frac{N}{P^{k}}⌋ \leftrightarrow 2 ((\frac{N}{P^{k}}) - 1) < 2 ⌊\frac{N}{P^{k}}⌋)$
56	54 55	mp3an3	$⊢ ((\frac{N}{P^{k}}) - 1 \in ℝ \land ⌊\frac{N}{P^{k}}⌋ \in ℝ) \to ((\frac{N}{P^{k}}) - 1 < ⌊\frac{N}{P^{k}}⌋ \leftrightarrow 2 ((\frac{N}{P^{k}}) - 1) < 2 ⌊\frac{N}{P^{k}}⌋)$
57	44 50 56	syl2anc	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ((\frac{N}{P^{k}}) - 1 < ⌊\frac{N}{P^{k}}⌋ \leftrightarrow 2 ((\frac{N}{P^{k}}) - 1) < 2 ⌊\frac{N}{P^{k}}⌋)$
58	52 57	mpbid	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 2 ((\frac{N}{P^{k}}) - 1) < 2 ⌊\frac{N}{P^{k}}⌋$
59	46 35 17 58	ltsub2dd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (\frac{2 \cdot N}{P^{k}}) - 2 ⌊\frac{N}{P^{k}}⌋ < (\frac{2 \cdot N}{P^{k}}) - 2 ((\frac{N}{P^{k}}) - 1)$
60		2cnd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 2 \in ℂ$
61		nncn	$⊢ N \in ℕ \to N \in ℂ$
62	61	ad2antrr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to N \in ℂ$
63	11	nncnd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to P^{k} \in ℂ$
64	11	nnne0d	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to P^{k} \neq 0$
65	60 62 63 64	divassd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to \frac{2 \cdot N}{P^{k}} = 2 (\frac{N}{P^{k}})$
66	25	recnd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to \frac{N}{P^{k}} \in ℂ$
67	60 66	muls1d	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 2 ((\frac{N}{P^{k}}) - 1) = 2 (\frac{N}{P^{k}}) - 2$
68	65 67	oveq12d	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (\frac{2 \cdot N}{P^{k}}) - 2 ((\frac{N}{P^{k}}) - 1) = 2 (\frac{N}{P^{k}}) - (2 (\frac{N}{P^{k}}) - 2)$
69		remulcl	$⊢ (2 \in ℝ \land \frac{N}{P^{k}} \in ℝ) \to 2 (\frac{N}{P^{k}}) \in ℝ$
70	37 25 69	sylancr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 2 (\frac{N}{P^{k}}) \in ℝ$
71	70	recnd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 2 (\frac{N}{P^{k}}) \in ℂ$
72		2cn	$⊢ 2 \in ℂ$
73		nncan	$⊢ (2 (\frac{N}{P^{k}}) \in ℂ \land 2 \in ℂ) \to 2 (\frac{N}{P^{k}}) - (2 (\frac{N}{P^{k}}) - 2) = 2$
74	71 72 73	sylancl	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 2 (\frac{N}{P^{k}}) - (2 (\frac{N}{P^{k}}) - 2) = 2$
75	68 74	eqtrd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (\frac{2 \cdot N}{P^{k}}) - 2 ((\frac{N}{P^{k}}) - 1) = 2$
76	59 75	breqtrd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (\frac{2 \cdot N}{P^{k}}) - 2 ⌊\frac{N}{P^{k}}⌋ < 2$
77	30 36 38 42 76	lelttrd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ < 2$
78		df-2	$⊢ 2 = 1 + 1$
79	77 78	breqtrdi	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ < 1 + 1$
80		1z	$⊢ 1 \in ℤ$
81		zleltp1	$⊢ (⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \in ℤ \land 1 \in ℤ) \to (⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \leq 1 \leftrightarrow ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ < 1 + 1)$
82	29 80 81	sylancl	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \leq 1 \leftrightarrow ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ < 1 + 1)$
83	79 82	mpbird	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \leq 1$
84		iftrue	$⊢ k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋) \to if (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋), 1, 0) = 1$
85	84	breq2d	$⊢ k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋) \to (⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \leq if (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋), 1, 0) \leftrightarrow ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \leq 1)$
86	83 85	syl5ibrcom	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \leq if (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋), 1, 0))$
87	9	nnge1d	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 1 \leq k$
88	87	biantrurd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (k \leq ⌊\frac{\log 2 \cdot N}{\log P}⌋ \leftrightarrow (1 \leq k \land k \leq ⌊\frac{\log 2 \cdot N}{\log P}⌋))$
89	6	adantl	$⊢ (N \in ℕ \land P \in ℙ) \to P \in ℕ$
90	89	nnred	$⊢ (N \in ℕ \land P \in ℙ) \to P \in ℝ$
91		prmuz2	$⊢ P \in ℙ \to P \in ℤ_{\geq 2}$
92	91	adantl	$⊢ (N \in ℕ \land P \in ℙ) \to P \in ℤ_{\geq 2}$
93		eluz2gt1	$⊢ P \in ℤ_{\geq 2} \to 1 < P$
94	92 93	syl	$⊢ (N \in ℕ \land P \in ℙ) \to 1 < P$
95	90 94	jca	$⊢ (N \in ℕ \land P \in ℙ) \to (P \in ℝ \land 1 < P)$
96	95	adantr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (P \in ℝ \land 1 < P)$
97		elfzelz	$⊢ k \in (1 \dots 2 \cdot N) \to k \in ℤ$
98	97	adantl	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to k \in ℤ$
99	4	adantr	$⊢ (N \in ℕ \land P \in ℙ) \to 2 \cdot N \in ℕ$
100	99	nnrpd	$⊢ (N \in ℕ \land P \in ℙ) \to 2 \cdot N \in ℝ^{+}$
101	100	adantr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 2 \cdot N \in ℝ^{+}$
102		efexple	$⊢ ((P \in ℝ \land 1 < P) \land k \in ℤ \land 2 \cdot N \in ℝ^{+}) \to (P^{k} \leq 2 \cdot N \leftrightarrow k \leq ⌊\frac{\log 2 \cdot N}{\log P}⌋)$
103	96 98 101 102	syl3anc	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (P^{k} \leq 2 \cdot N \leftrightarrow k \leq ⌊\frac{\log 2 \cdot N}{\log P}⌋)$
104	9	nnzd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to k \in ℤ$
105	80	a1i	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 1 \in ℤ$
106	99	nnred	$⊢ (N \in ℕ \land P \in ℙ) \to 2 \cdot N \in ℝ$
107		1red	$⊢ (N \in ℕ \land P \in ℙ) \to 1 \in ℝ$
108	37	a1i	$⊢ (N \in ℕ \land P \in ℙ) \to 2 \in ℝ$
109		1lt2	$⊢ 1 < 2$
110	109	a1i	$⊢ (N \in ℕ \land P \in ℙ) \to 1 < 2$
111		2t1e2	$⊢ 2 \cdot 1 = 2$
112		nnre	$⊢ N \in ℕ \to N \in ℝ$
113	112	adantr	$⊢ (N \in ℕ \land P \in ℙ) \to N \in ℝ$
114		0le2	$⊢ 0 \leq 2$
115	37 114	pm3.2i	$⊢ (2 \in ℝ \land 0 \leq 2)$
116	115	a1i	$⊢ (N \in ℕ \land P \in ℙ) \to (2 \in ℝ \land 0 \leq 2)$
117		nnge1	$⊢ N \in ℕ \to 1 \leq N$
118	117	adantr	$⊢ (N \in ℕ \land P \in ℙ) \to 1 \leq N$
119		lemul2a	$⊢ ((1 \in ℝ \land N \in ℝ \land (2 \in ℝ \land 0 \leq 2)) \land 1 \leq N) \to 2 \cdot 1 \leq 2 \cdot N$
120	107 113 116 118 119	syl31anc	$⊢ (N \in ℕ \land P \in ℙ) \to 2 \cdot 1 \leq 2 \cdot N$
121	111 120	eqbrtrrid	$⊢ (N \in ℕ \land P \in ℙ) \to 2 \leq 2 \cdot N$
122	107 108 106 110 121	ltletrd	$⊢ (N \in ℕ \land P \in ℙ) \to 1 < 2 \cdot N$
123	106 122	rplogcld	$⊢ (N \in ℕ \land P \in ℙ) \to \log 2 \cdot N \in ℝ^{+}$
124	90 94	rplogcld	$⊢ (N \in ℕ \land P \in ℙ) \to \log P \in ℝ^{+}$
125	123 124	rpdivcld	$⊢ (N \in ℕ \land P \in ℙ) \to \frac{\log 2 \cdot N}{\log P} \in ℝ^{+}$
126	125	rpred	$⊢ (N \in ℕ \land P \in ℙ) \to \frac{\log 2 \cdot N}{\log P} \in ℝ$
127	126	flcld	$⊢ (N \in ℕ \land P \in ℙ) \to ⌊\frac{\log 2 \cdot N}{\log P}⌋ \in ℤ$
128	127	adantr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{\log 2 \cdot N}{\log P}⌋ \in ℤ$
129		elfz	$⊢ (k \in ℤ \land 1 \in ℤ \land ⌊\frac{\log 2 \cdot N}{\log P}⌋ \in ℤ) \to (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋) \leftrightarrow (1 \leq k \land k \leq ⌊\frac{\log 2 \cdot N}{\log P}⌋))$
130	104 105 128 129	syl3anc	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋) \leftrightarrow (1 \leq k \land k \leq ⌊\frac{\log 2 \cdot N}{\log P}⌋))$
131	88 103 130	3bitr4rd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋) \leftrightarrow P^{k} \leq 2 \cdot N)$
132	131	notbid	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (\neg k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋) \leftrightarrow \neg P^{k} \leq 2 \cdot N)$
133	106	adantr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 2 \cdot N \in ℝ$
134	11	nnred	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to P^{k} \in ℝ$
135	133 134	ltnled	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (2 \cdot N < P^{k} \leftrightarrow \neg P^{k} \leq 2 \cdot N)$
136	132 135	bitr4d	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (\neg k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋) \leftrightarrow 2 \cdot N < P^{k})$
137	16	rpge0d	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 0 \leq \frac{2 \cdot N}{P^{k}}$
138	137	adantrr	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \to 0 \leq \frac{2 \cdot N}{P^{k}}$
139	11	nngt0d	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 0 < P^{k}$
140		ltdivmul	$⊢ (2 \cdot N \in ℝ \land 1 \in ℝ \land (P^{k} \in ℝ \land 0 < P^{k})) \to (\frac{2 \cdot N}{P^{k}} < 1 \leftrightarrow 2 \cdot N < P^{k} \cdot 1)$
141	133 49 134 139 140	syl112anc	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (\frac{2 \cdot N}{P^{k}} < 1 \leftrightarrow 2 \cdot N < P^{k} \cdot 1)$
142	63	mulid1d	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to P^{k} \cdot 1 = P^{k}$
143	142	breq2d	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (2 \cdot N < P^{k} \cdot 1 \leftrightarrow 2 \cdot N < P^{k})$
144	141 143	bitrd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (\frac{2 \cdot N}{P^{k}} < 1 \leftrightarrow 2 \cdot N < P^{k})$
145	144	biimprd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (2 \cdot N < P^{k} \to \frac{2 \cdot N}{P^{k}} < 1)$
146	145	impr	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \to \frac{2 \cdot N}{P^{k}} < 1$
147		0p1e1	$⊢ 0 + 1 = 1$
148	146 147	breqtrrdi	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \to \frac{2 \cdot N}{P^{k}} < 0 + 1$
149	17	adantrr	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \to \frac{2 \cdot N}{P^{k}} \in ℝ$
150		0z	$⊢ 0 \in ℤ$
151		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))$
152	149 150 151	sylancl	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \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))$
153	138 148 152	mpbir2and	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ = 0$
154	24	rpge0d	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to 0 \leq \frac{N}{P^{k}}$
155	154	adantrr	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \to 0 \leq \frac{N}{P^{k}}$
156	112 21	ltaddrp2d	$⊢ N \in ℕ \to N < N + N$
157	61	2timesd	$⊢ N \in ℕ \to 2 \cdot N = N + N$
158	156 157	breqtrrd	$⊢ N \in ℕ \to N < 2 \cdot N$
159	158	ad2antrr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to N < 2 \cdot N$
160	112	ad2antrr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to N \in ℝ$
161		lttr	$⊢ (N \in ℝ \land 2 \cdot N \in ℝ \land P^{k} \in ℝ) \to ((N < 2 \cdot N \land 2 \cdot N < P^{k}) \to N < P^{k})$
162	160 133 134 161	syl3anc	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ((N < 2 \cdot N \land 2 \cdot N < P^{k}) \to N < P^{k})$
163	159 162	mpand	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (2 \cdot N < P^{k} \to N < P^{k})$
164		ltdivmul	$⊢ (N \in ℝ \land 1 \in ℝ \land (P^{k} \in ℝ \land 0 < P^{k})) \to (\frac{N}{P^{k}} < 1 \leftrightarrow N < P^{k} \cdot 1)$
165	160 49 134 139 164	syl112anc	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (\frac{N}{P^{k}} < 1 \leftrightarrow N < P^{k} \cdot 1)$
166	142	breq2d	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (N < P^{k} \cdot 1 \leftrightarrow N < P^{k})$
167	165 166	bitrd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (\frac{N}{P^{k}} < 1 \leftrightarrow N < P^{k})$
168	163 167	sylibrd	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (2 \cdot N < P^{k} \to \frac{N}{P^{k}} < 1)$
169	168	impr	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \to \frac{N}{P^{k}} < 1$
170	169 147	breqtrrdi	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \to \frac{N}{P^{k}} < 0 + 1$
171	25	adantrr	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \to \frac{N}{P^{k}} \in ℝ$
172		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))$
173	171 150 172	sylancl	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \to (⌊\frac{N}{P^{k}}⌋ = 0 \leftrightarrow (0 \leq \frac{N}{P^{k}} \land \frac{N}{P^{k}} < 0 + 1))$
174	155 170 173	mpbir2and	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \to ⌊\frac{N}{P^{k}}⌋ = 0$
175	174	oveq2d	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \to 2 ⌊\frac{N}{P^{k}}⌋ = 2 \cdot 0$
176		2t0e0	$⊢ 2 \cdot 0 = 0$
177	175 176	eqtrdi	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \to 2 ⌊\frac{N}{P^{k}}⌋ = 0$
178	153 177	oveq12d	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ = 0 - 0$
179		0m0e0	$⊢ 0 - 0 = 0$
180	178 179	eqtrdi	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ = 0$
181		0le0	$⊢ 0 \leq 0$
182	180 181	eqbrtrdi	$⊢ ((N \in ℕ \land P \in ℙ) \land (k \in (1 \dots 2 \cdot N) \land 2 \cdot N < P^{k})) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \leq 0$
183	182	expr	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (2 \cdot N < P^{k} \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \leq 0)$
184	136 183	sylbid	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (\neg k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \leq 0)$
185		iffalse	$⊢ \neg k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋) \to if (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋), 1, 0) = 0$
186	185	eqcomd	$⊢ \neg k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋) \to 0 = if (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋), 1, 0)$
187	186	breq2d	$⊢ \neg k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋) \to (⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \leq 0 \leftrightarrow ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \leq if (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋), 1, 0))$
188	184 187	mpbidi	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to (\neg k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \leq if (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋), 1, 0))$
189	86 188	pm2.61d	$⊢ ((N \in ℕ \land P \in ℙ) \land k \in (1 \dots 2 \cdot N)) \to ⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋ \leq if (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋), 1, 0)$
190	1 30 34 189	fsumle	$⊢ (N \in ℕ \land P \in ℙ) \to \sum_{k = 1}^{2 \cdot N} (⌊\frac{2 \cdot N}{P^{k}}⌋ - 2 ⌊\frac{N}{P^{k}}⌋) \leq \sum_{k = 1}^{2 \cdot N} if (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋), 1, 0)$
191		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}}⌋)$
192	127	zred	$⊢ (N \in ℕ \land P \in ℙ) \to ⌊\frac{\log 2 \cdot N}{\log P}⌋ \in ℝ$
193		flle	$⊢ \frac{\log 2 \cdot N}{\log P} \in ℝ \to ⌊\frac{\log 2 \cdot N}{\log P}⌋ \leq \frac{\log 2 \cdot N}{\log P}$
194	126 193	syl	$⊢ (N \in ℕ \land P \in ℙ) \to ⌊\frac{\log 2 \cdot N}{\log P}⌋ \leq \frac{\log 2 \cdot N}{\log P}$
195	99	nnnn0d	$⊢ (N \in ℕ \land P \in ℙ) \to 2 \cdot N \in ℕ_{0}$
196	89 195	nnexpcld	$⊢ (N \in ℕ \land P \in ℙ) \to P^{2 \cdot N} \in ℕ$
197	196	nnred	$⊢ (N \in ℕ \land P \in ℙ) \to P^{2 \cdot N} \in ℝ$
198		bernneq3	$⊢ (P \in ℤ_{\geq 2} \land 2 \cdot N \in ℕ_{0}) \to 2 \cdot N < P^{2 \cdot N}$
199	92 195 198	syl2anc	$⊢ (N \in ℕ \land P \in ℙ) \to 2 \cdot N < P^{2 \cdot N}$
200	106 197 199	ltled	$⊢ (N \in ℕ \land P \in ℙ) \to 2 \cdot N \leq P^{2 \cdot N}$
201	100	reeflogd	$⊢ (N \in ℕ \land P \in ℙ) \to e^{\log 2 \cdot N} = 2 \cdot N$
202	89	nnrpd	$⊢ (N \in ℕ \land P \in ℙ) \to P \in ℝ^{+}$
203	99	nnzd	$⊢ (N \in ℕ \land P \in ℙ) \to 2 \cdot N \in ℤ$
204		reexplog	$⊢ (P \in ℝ^{+} \land 2 \cdot N \in ℤ) \to P^{2 \cdot N} = e^{2 \cdot N \log P}$
205	202 203 204	syl2anc	$⊢ (N \in ℕ \land P \in ℙ) \to P^{2 \cdot N} = e^{2 \cdot N \log P}$
206	205	eqcomd	$⊢ (N \in ℕ \land P \in ℙ) \to e^{2 \cdot N \log P} = P^{2 \cdot N}$
207	200 201 206	3brtr4d	$⊢ (N \in ℕ \land P \in ℙ) \to e^{\log 2 \cdot N} \leq e^{2 \cdot N \log P}$
208	100	relogcld	$⊢ (N \in ℕ \land P \in ℙ) \to \log 2 \cdot N \in ℝ$
209	124	rpred	$⊢ (N \in ℕ \land P \in ℙ) \to \log P \in ℝ$
210	106 209	remulcld	$⊢ (N \in ℕ \land P \in ℙ) \to 2 \cdot N \log P \in ℝ$
211		efle	$⊢ (\log 2 \cdot N \in ℝ \land 2 \cdot N \log P \in ℝ) \to (\log 2 \cdot N \leq 2 \cdot N \log P \leftrightarrow e^{\log 2 \cdot N} \leq e^{2 \cdot N \log P})$
212	208 210 211	syl2anc	$⊢ (N \in ℕ \land P \in ℙ) \to (\log 2 \cdot N \leq 2 \cdot N \log P \leftrightarrow e^{\log 2 \cdot N} \leq e^{2 \cdot N \log P})$
213	207 212	mpbird	$⊢ (N \in ℕ \land P \in ℙ) \to \log 2 \cdot N \leq 2 \cdot N \log P$
214	208 106 124	ledivmul2d	$⊢ (N \in ℕ \land P \in ℙ) \to (\frac{\log 2 \cdot N}{\log P} \leq 2 \cdot N \leftrightarrow \log 2 \cdot N \leq 2 \cdot N \log P)$
215	213 214	mpbird	$⊢ (N \in ℕ \land P \in ℙ) \to \frac{\log 2 \cdot N}{\log P} \leq 2 \cdot N$
216	192 126 106 194 215	letrd	$⊢ (N \in ℕ \land P \in ℙ) \to ⌊\frac{\log 2 \cdot N}{\log P}⌋ \leq 2 \cdot N$
217		eluz	$⊢ (⌊\frac{\log 2 \cdot N}{\log P}⌋ \in ℤ \land 2 \cdot N \in ℤ) \to (2 \cdot N \in ℤ_{\geq ⌊\frac{\log 2 \cdot N}{\log P}⌋} \leftrightarrow ⌊\frac{\log 2 \cdot N}{\log P}⌋ \leq 2 \cdot N)$
218	127 203 217	syl2anc	$⊢ (N \in ℕ \land P \in ℙ) \to (2 \cdot N \in ℤ_{\geq ⌊\frac{\log 2 \cdot N}{\log P}⌋} \leftrightarrow ⌊\frac{\log 2 \cdot N}{\log P}⌋ \leq 2 \cdot N)$
219	216 218	mpbird	$⊢ (N \in ℕ \land P \in ℙ) \to 2 \cdot N \in ℤ_{\geq ⌊\frac{\log 2 \cdot N}{\log P}⌋}$
220		fzss2	$⊢ 2 \cdot N \in ℤ_{\geq ⌊\frac{\log 2 \cdot N}{\log P}⌋} \to (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋) \subseteq (1 \dots 2 \cdot N)$
221	219 220	syl	$⊢ (N \in ℕ \land P \in ℙ) \to (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋) \subseteq (1 \dots 2 \cdot N)$
222		sumhash	$⊢ ((1 \dots 2 \cdot N) \in Fin \land (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋) \subseteq (1 \dots 2 \cdot N)) \to \sum_{k = 1}^{2 \cdot N} if (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋), 1, 0) = \|(1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋)\|$
223	1 221 222	syl2anc	$⊢ (N \in ℕ \land P \in ℙ) \to \sum_{k = 1}^{2 \cdot N} if (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋), 1, 0) = \|(1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋)\|$
224	125	rprege0d	$⊢ (N \in ℕ \land P \in ℙ) \to (\frac{\log 2 \cdot N}{\log P} \in ℝ \land 0 \leq \frac{\log 2 \cdot N}{\log P})$
225		flge0nn0	$⊢ (\frac{\log 2 \cdot N}{\log P} \in ℝ \land 0 \leq \frac{\log 2 \cdot N}{\log P}) \to ⌊\frac{\log 2 \cdot N}{\log P}⌋ \in ℕ_{0}$
226		hashfz1	$⊢ ⌊\frac{\log 2 \cdot N}{\log P}⌋ \in ℕ_{0} \to \|(1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋)\| = ⌊\frac{\log 2 \cdot N}{\log P}⌋$
227	224 225 226	3syl	$⊢ (N \in ℕ \land P \in ℙ) \to \|(1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋)\| = ⌊\frac{\log 2 \cdot N}{\log P}⌋$
228	223 227	eqtr2d	$⊢ (N \in ℕ \land P \in ℙ) \to ⌊\frac{\log 2 \cdot N}{\log P}⌋ = \sum_{k = 1}^{2 \cdot N} if (k \in (1 \dots ⌊\frac{\log 2 \cdot N}{\log P}⌋), 1, 0)$
229	190 191 228	3brtr4d	$⊢ (N \in ℕ \land P \in ℙ) \to P pCnt (\binom{2 \cdot N}{N}) \leq ⌊\frac{\log 2 \cdot N}{\log P}⌋$
230		simpr	$⊢ (N \in ℕ \land P \in ℙ) \to P \in ℙ$
231		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
232		fzctr	$⊢ N \in ℕ_{0} \to N \in (0 \dots 2 \cdot N)$
233		bccl2	$⊢ N \in (0 \dots 2 \cdot N) \to (\binom{2 \cdot N}{N}) \in ℕ$
234	231 232 233	3syl	$⊢ N \in ℕ \to (\binom{2 \cdot N}{N}) \in ℕ$
235	234	adantr	$⊢ (N \in ℕ \land P \in ℙ) \to (\binom{2 \cdot N}{N}) \in ℕ$
236	230 235	pccld	$⊢ (N \in ℕ \land P \in ℙ) \to P pCnt (\binom{2 \cdot N}{N}) \in ℕ_{0}$
237	236	nn0zd	$⊢ (N \in ℕ \land P \in ℙ) \to P pCnt (\binom{2 \cdot N}{N}) \in ℤ$
238		efexple	$⊢ ((P \in ℝ \land 1 < P) \land P pCnt (\binom{2 \cdot N}{N}) \in ℤ \land 2 \cdot N \in ℝ^{+}) \to (P^{P pCnt (\binom{2 \cdot N}{N})} \leq 2 \cdot N \leftrightarrow P pCnt (\binom{2 \cdot N}{N}) \leq ⌊\frac{\log 2 \cdot N}{\log P}⌋)$
239	90 94 237 100 238	syl211anc	$⊢ (N \in ℕ \land P \in ℙ) \to (P^{P pCnt (\binom{2 \cdot N}{N})} \leq 2 \cdot N \leftrightarrow P pCnt (\binom{2 \cdot N}{N}) \leq ⌊\frac{\log 2 \cdot N}{\log P}⌋)$
240	229 239	mpbird	$⊢ (N \in ℕ \land P \in ℙ) \to P^{P pCnt (\binom{2 \cdot N}{N})} \leq 2 \cdot N$

Metamath Proof Explorer

Theorem bposlem1

Proof