pcbc

Description: Calculate the prime count of a binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014) (Revised by Mario Carneiro, 21-May-2014)

		Ref	Expression
	Assertion	pcbc	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to P pCnt (\binom{N}{K}) = \sum_{k = 1}^{N} (⌊\frac{N}{P^{k}}⌋ - (⌊\frac{N - K}{P^{k}}⌋ + ⌊\frac{K}{P^{k}}⌋))$

Proof

Step	Hyp	Ref	Expression
1		simp3	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to P \in ℙ$
2		nnnn0	$⊢ N \in ℕ \to N \in ℕ_{0}$
3	2	3ad2ant1	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to N \in ℕ_{0}$
4	3	faccld	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to N! \in ℕ$
5	4	nnzd	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to N! \in ℤ$
6	4	nnne0d	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to N! \neq 0$
7		fznn0sub	$⊢ K \in (0 \dots N) \to N - K \in ℕ_{0}$
8	7	3ad2ant2	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to N - K \in ℕ_{0}$
9	8	faccld	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to (N - K)! \in ℕ$
10		elfznn0	$⊢ K \in (0 \dots N) \to K \in ℕ_{0}$
11	10	3ad2ant2	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to K \in ℕ_{0}$
12	11	faccld	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to K! \in ℕ$
13	9 12	nnmulcld	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to (N - K)! K! \in ℕ$
14		pcdiv	$⊢ (P \in ℙ \land (N! \in ℤ \land N! \neq 0) \land (N - K)! K! \in ℕ) \to P pCnt (\frac{N!}{(N - K)! K!}) = (P pCnt N!) - (P pCnt (N - K)! K!)$
15	1 5 6 13 14	syl121anc	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to P pCnt (\frac{N!}{(N - K)! K!}) = (P pCnt N!) - (P pCnt (N - K)! K!)$
16		bcval2	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) = \frac{N!}{(N - K)! K!}$
17	16	3ad2ant2	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to (\binom{N}{K}) = \frac{N!}{(N - K)! K!}$
18	17	oveq2d	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to P pCnt (\binom{N}{K}) = P pCnt (\frac{N!}{(N - K)! K!})$
19		fzfid	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to (1 \dots N) \in Fin$
20		nnre	$⊢ N \in ℕ \to N \in ℝ$
21	20	3ad2ant1	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to N \in ℝ$
22	21	adantr	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to N \in ℝ$
23		simpl3	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to P \in ℙ$
24		prmnn	$⊢ P \in ℙ \to P \in ℕ$
25	23 24	syl	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to P \in ℕ$
26		elfznn	$⊢ k \in (1 \dots N) \to k \in ℕ$
27	26	nnnn0d	$⊢ k \in (1 \dots N) \to k \in ℕ_{0}$
28	27	adantl	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to k \in ℕ_{0}$
29	25 28	nnexpcld	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to P^{k} \in ℕ$
30	22 29	nndivred	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to \frac{N}{P^{k}} \in ℝ$
31	30	flcld	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to ⌊\frac{N}{P^{k}}⌋ \in ℤ$
32	31	zcnd	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to ⌊\frac{N}{P^{k}}⌋ \in ℂ$
33	11	nn0red	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to K \in ℝ$
34	21 33	resubcld	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to N - K \in ℝ$
35	34	adantr	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to N - K \in ℝ$
36	35 29	nndivred	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to \frac{N - K}{P^{k}} \in ℝ$
37	36	flcld	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to ⌊\frac{N - K}{P^{k}}⌋ \in ℤ$
38	37	zcnd	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to ⌊\frac{N - K}{P^{k}}⌋ \in ℂ$
39	33	adantr	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to K \in ℝ$
40	39 29	nndivred	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to \frac{K}{P^{k}} \in ℝ$
41	40	flcld	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to ⌊\frac{K}{P^{k}}⌋ \in ℤ$
42	41	zcnd	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to ⌊\frac{K}{P^{k}}⌋ \in ℂ$
43	38 42	addcld	$⊢ ((N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \land k \in (1 \dots N)) \to ⌊\frac{N - K}{P^{k}}⌋ + ⌊\frac{K}{P^{k}}⌋ \in ℂ$
44	19 32 43	fsumsub	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to \sum_{k = 1}^{N} (⌊\frac{N}{P^{k}}⌋ - (⌊\frac{N - K}{P^{k}}⌋ + ⌊\frac{K}{P^{k}}⌋)) = \sum_{k = 1}^{N} ⌊\frac{N}{P^{k}}⌋ - \sum_{k = 1}^{N} (⌊\frac{N - K}{P^{k}}⌋ + ⌊\frac{K}{P^{k}}⌋)$
45	3	nn0zd	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to N \in ℤ$
46		uzid	$⊢ N \in ℤ \to N \in ℤ_{\geq N}$
47	45 46	syl	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to N \in ℤ_{\geq N}$
48		pcfac	$⊢ (N \in ℕ_{0} \land N \in ℤ_{\geq N} \land P \in ℙ) \to P pCnt N! = \sum_{k = 1}^{N} ⌊\frac{N}{P^{k}}⌋$
49	3 47 1 48	syl3anc	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to P pCnt N! = \sum_{k = 1}^{N} ⌊\frac{N}{P^{k}}⌋$
50	11	nn0ge0d	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to 0 \leq K$
51	21 33	subge02d	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to (0 \leq K \leftrightarrow N - K \leq N)$
52	50 51	mpbid	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to N - K \leq N$
53	11	nn0zd	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to K \in ℤ$
54	45 53	zsubcld	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to N - K \in ℤ$
55		eluz	$⊢ (N - K \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq (N - K)} \leftrightarrow N - K \leq N)$
56	54 45 55	syl2anc	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to (N \in ℤ_{\geq (N - K)} \leftrightarrow N - K \leq N)$
57	52 56	mpbird	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to N \in ℤ_{\geq (N - K)}$
58		pcfac	$⊢ (N - K \in ℕ_{0} \land N \in ℤ_{\geq (N - K)} \land P \in ℙ) \to P pCnt (N - K)! = \sum_{k = 1}^{N} ⌊\frac{N - K}{P^{k}}⌋$
59	8 57 1 58	syl3anc	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to P pCnt (N - K)! = \sum_{k = 1}^{N} ⌊\frac{N - K}{P^{k}}⌋$
60		elfzuz3	$⊢ K \in (0 \dots N) \to N \in ℤ_{\geq K}$
61	60	3ad2ant2	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to N \in ℤ_{\geq K}$
62		pcfac	$⊢ (K \in ℕ_{0} \land N \in ℤ_{\geq K} \land P \in ℙ) \to P pCnt K! = \sum_{k = 1}^{N} ⌊\frac{K}{P^{k}}⌋$
63	11 61 1 62	syl3anc	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to P pCnt K! = \sum_{k = 1}^{N} ⌊\frac{K}{P^{k}}⌋$
64	59 63	oveq12d	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to (P pCnt (N - K)!) + (P pCnt K!) = \sum_{k = 1}^{N} ⌊\frac{N - K}{P^{k}}⌋ + \sum_{k = 1}^{N} ⌊\frac{K}{P^{k}}⌋$
65	9	nnzd	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to (N - K)! \in ℤ$
66	9	nnne0d	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to (N - K)! \neq 0$
67	12	nnzd	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to K! \in ℤ$
68	12	nnne0d	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to K! \neq 0$
69		pcmul	$⊢ (P \in ℙ \land ((N - K)! \in ℤ \land (N - K)! \neq 0) \land (K! \in ℤ \land K! \neq 0)) \to P pCnt (N - K)! K! = (P pCnt (N - K)!) + (P pCnt K!)$
70	1 65 66 67 68 69	syl122anc	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to P pCnt (N - K)! K! = (P pCnt (N - K)!) + (P pCnt K!)$
71	19 38 42	fsumadd	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to \sum_{k = 1}^{N} (⌊\frac{N - K}{P^{k}}⌋ + ⌊\frac{K}{P^{k}}⌋) = \sum_{k = 1}^{N} ⌊\frac{N - K}{P^{k}}⌋ + \sum_{k = 1}^{N} ⌊\frac{K}{P^{k}}⌋$
72	64 70 71	3eqtr4d	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to P pCnt (N - K)! K! = \sum_{k = 1}^{N} (⌊\frac{N - K}{P^{k}}⌋ + ⌊\frac{K}{P^{k}}⌋)$
73	49 72	oveq12d	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to (P pCnt N!) - (P pCnt (N - K)! K!) = \sum_{k = 1}^{N} ⌊\frac{N}{P^{k}}⌋ - \sum_{k = 1}^{N} (⌊\frac{N - K}{P^{k}}⌋ + ⌊\frac{K}{P^{k}}⌋)$
74	44 73	eqtr4d	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to \sum_{k = 1}^{N} (⌊\frac{N}{P^{k}}⌋ - (⌊\frac{N - K}{P^{k}}⌋ + ⌊\frac{K}{P^{k}}⌋)) = (P pCnt N!) - (P pCnt (N - K)! K!)$
75	15 18 74	3eqtr4d	$⊢ (N \in ℕ \land K \in (0 \dots N) \land P \in ℙ) \to P pCnt (\binom{N}{K}) = \sum_{k = 1}^{N} (⌊\frac{N}{P^{k}}⌋ - (⌊\frac{N - K}{P^{k}}⌋ + ⌊\frac{K}{P^{k}}⌋))$

Metamath Proof Explorer

Theorem pcbc

Proof