bccmpl

Description: "Complementing" its second argument doesn't change a binary coefficient. (Contributed by NM, 21-Jun-2005) (Revised by Mario Carneiro, 5-Mar-2014)

		Ref	Expression
	Assertion	bccmpl	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (\binom{N}{K}) = (\binom{N}{N - K})$

Proof

Step	Hyp	Ref	Expression
1		bcval2	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) = \frac{N!}{(N - K)! K!}$
2		fznn0sub2	$⊢ K \in (0 \dots N) \to N - K \in (0 \dots N)$
3		bcval2	$⊢ N - K \in (0 \dots N) \to (\binom{N}{N - K}) = \frac{N!}{(N - (N - K))! (N - K)!}$
4	2 3	syl	$⊢ K \in (0 \dots N) \to (\binom{N}{N - K}) = \frac{N!}{(N - (N - K))! (N - K)!}$
5		elfznn0	$⊢ N - K \in (0 \dots N) \to N - K \in ℕ_{0}$
6	5	faccld	$⊢ N - K \in (0 \dots N) \to (N - K)! \in ℕ$
7	6	nncnd	$⊢ N - K \in (0 \dots N) \to (N - K)! \in ℂ$
8	2 7	syl	$⊢ K \in (0 \dots N) \to (N - K)! \in ℂ$
9		elfznn0	$⊢ K \in (0 \dots N) \to K \in ℕ_{0}$
10	9	faccld	$⊢ K \in (0 \dots N) \to K! \in ℕ$
11	10	nncnd	$⊢ K \in (0 \dots N) \to K! \in ℂ$
12	8 11	mulcomd	$⊢ K \in (0 \dots N) \to (N - K)! K! = K! (N - K)!$
13		elfz3nn0	$⊢ K \in (0 \dots N) \to N \in ℕ_{0}$
14		elfzelz	$⊢ K \in (0 \dots N) \to K \in ℤ$
15		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
16		zcn	$⊢ K \in ℤ \to K \in ℂ$
17		nncan	$⊢ (N \in ℂ \land K \in ℂ) \to N - (N - K) = K$
18	15 16 17	syl2an	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to N - (N - K) = K$
19	13 14 18	syl2anc	$⊢ K \in (0 \dots N) \to N - (N - K) = K$
20	19	fveq2d	$⊢ K \in (0 \dots N) \to (N - (N - K))! = K!$
21	20	oveq1d	$⊢ K \in (0 \dots N) \to (N - (N - K))! (N - K)! = K! (N - K)!$
22	12 21	eqtr4d	$⊢ K \in (0 \dots N) \to (N - K)! K! = (N - (N - K))! (N - K)!$
23	22	oveq2d	$⊢ K \in (0 \dots N) \to \frac{N!}{(N - K)! K!} = \frac{N!}{(N - (N - K))! (N - K)!}$
24	4 23	eqtr4d	$⊢ K \in (0 \dots N) \to (\binom{N}{N - K}) = \frac{N!}{(N - K)! K!}$
25	1 24	eqtr4d	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) = (\binom{N}{N - K})$
26	25	adantl	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in (0 \dots N)) \to (\binom{N}{K}) = (\binom{N}{N - K})$
27		bcval3	$⊢ (N \in ℕ_{0} \land K \in ℤ \land \neg K \in (0 \dots N)) \to (\binom{N}{K}) = 0$
28		simp1	$⊢ (N \in ℕ_{0} \land K \in ℤ \land \neg K \in (0 \dots N)) \to N \in ℕ_{0}$
29		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
30		zsubcl	$⊢ (N \in ℤ \land K \in ℤ) \to N - K \in ℤ$
31	29 30	sylan	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to N - K \in ℤ$
32	31	3adant3	$⊢ (N \in ℕ_{0} \land K \in ℤ \land \neg K \in (0 \dots N)) \to N - K \in ℤ$
33		fznn0sub2	$⊢ N - K \in (0 \dots N) \to N - (N - K) \in (0 \dots N)$
34	18	eleq1d	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (N - (N - K) \in (0 \dots N) \leftrightarrow K \in (0 \dots N))$
35	33 34	imbitrid	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (N - K \in (0 \dots N) \to K \in (0 \dots N))$
36	35	con3d	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (\neg K \in (0 \dots N) \to \neg N - K \in (0 \dots N))$
37	36	3impia	$⊢ (N \in ℕ_{0} \land K \in ℤ \land \neg K \in (0 \dots N)) \to \neg N - K \in (0 \dots N)$
38		bcval3	$⊢ (N \in ℕ_{0} \land N - K \in ℤ \land \neg N - K \in (0 \dots N)) \to (\binom{N}{N - K}) = 0$
39	28 32 37 38	syl3anc	$⊢ (N \in ℕ_{0} \land K \in ℤ \land \neg K \in (0 \dots N)) \to (\binom{N}{N - K}) = 0$
40	27 39	eqtr4d	$⊢ (N \in ℕ_{0} \land K \in ℤ \land \neg K \in (0 \dots N)) \to (\binom{N}{K}) = (\binom{N}{N - K})$
41	40	3expa	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land \neg K \in (0 \dots N)) \to (\binom{N}{K}) = (\binom{N}{N - K})$
42	26 41	pm2.61dan	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (\binom{N}{K}) = (\binom{N}{N - K})$

Metamath Proof Explorer

Theorem bccmpl

Proof