bcmax

Description: The binomial coefficient takes its maximum value at the center. (Contributed by Mario Carneiro, 5-Mar-2014)

		Ref	Expression
	Assertion	bcmax	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (\binom{2 \cdot N}{K}) \leq (\binom{2 \cdot N}{N})$

Proof

Step	Hyp	Ref	Expression
1		2nn0	$⊢ 2 \in ℕ_{0}$
2		simpll	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land N \in ℤ_{\geq K}) \to N \in ℕ_{0}$
3		nn0mulcl	$⊢ (2 \in ℕ_{0} \land N \in ℕ_{0}) \to 2 \cdot N \in ℕ_{0}$
4	1 2 3	sylancr	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land N \in ℤ_{\geq K}) \to 2 \cdot N \in ℕ_{0}$
5		simpr	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land N \in ℤ_{\geq K}) \to N \in ℤ_{\geq K}$
6		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
7	6	leidd	$⊢ N \in ℕ_{0} \to N \leq N$
8		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
9		2cn	$⊢ 2 \in ℂ$
10		2ne0	$⊢ 2 \neq 0$
11		divcan3	$⊢ (N \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{2 \cdot N}{2} = N$
12	9 10 11	mp3an23	$⊢ N \in ℂ \to \frac{2 \cdot N}{2} = N$
13	8 12	syl	$⊢ N \in ℕ_{0} \to \frac{2 \cdot N}{2} = N$
14	7 13	breqtrrd	$⊢ N \in ℕ_{0} \to N \leq \frac{2 \cdot N}{2}$
15	2 14	syl	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land N \in ℤ_{\geq K}) \to N \leq \frac{2 \cdot N}{2}$
16		bcmono	$⊢ (2 \cdot N \in ℕ_{0} \land N \in ℤ_{\geq K} \land N \leq \frac{2 \cdot N}{2}) \to (\binom{2 \cdot N}{K}) \leq (\binom{2 \cdot N}{N})$
17	4 5 15 16	syl3anc	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land N \in ℤ_{\geq K}) \to (\binom{2 \cdot N}{K}) \leq (\binom{2 \cdot N}{N})$
18		simpll	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to N \in ℕ_{0}$
19	1 18 3	sylancr	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to 2 \cdot N \in ℕ_{0}$
20		simplr	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to K \in ℤ$
21		bccmpl	$⊢ (2 \cdot N \in ℕ_{0} \land K \in ℤ) \to (\binom{2 \cdot N}{K}) = (\binom{2 \cdot N}{2 \cdot N - K})$
22	19 20 21	syl2anc	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to (\binom{2 \cdot N}{K}) = (\binom{2 \cdot N}{2 \cdot N - K})$
23	18	nn0red	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to N \in ℝ$
24	23	recnd	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to N \in ℂ$
25	24	2timesd	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to 2 \cdot N = N + N$
26	20	zred	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to K \in ℝ$
27		eluzle	$⊢ K \in ℤ_{\geq N} \to N \leq K$
28	27	adantl	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to N \leq K$
29	23 26 23 28	leadd2dd	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to N + N \leq N + K$
30	25 29	eqbrtrd	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to 2 \cdot N \leq N + K$
31	19	nn0red	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to 2 \cdot N \in ℝ$
32	31 26 23	lesubaddd	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to (2 \cdot N - K \leq N \leftrightarrow 2 \cdot N \leq N + K)$
33	30 32	mpbird	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to 2 \cdot N - K \leq N$
34	19	nn0zd	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to 2 \cdot N \in ℤ$
35	34 20	zsubcld	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to 2 \cdot N - K \in ℤ$
36	18	nn0zd	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to N \in ℤ$
37		eluz	$⊢ (2 \cdot N - K \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq (2 \cdot N - K)} \leftrightarrow 2 \cdot N - K \leq N)$
38	35 36 37	syl2anc	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to (N \in ℤ_{\geq (2 \cdot N - K)} \leftrightarrow 2 \cdot N - K \leq N)$
39	33 38	mpbird	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to N \in ℤ_{\geq (2 \cdot N - K)}$
40	18 14	syl	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to N \leq \frac{2 \cdot N}{2}$
41		bcmono	$⊢ (2 \cdot N \in ℕ_{0} \land N \in ℤ_{\geq (2 \cdot N - K)} \land N \leq \frac{2 \cdot N}{2}) \to (\binom{2 \cdot N}{2 \cdot N - K}) \leq (\binom{2 \cdot N}{N})$
42	19 39 40 41	syl3anc	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to (\binom{2 \cdot N}{2 \cdot N - K}) \leq (\binom{2 \cdot N}{N})$
43	22 42	eqbrtrd	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land K \in ℤ_{\geq N}) \to (\binom{2 \cdot N}{K}) \leq (\binom{2 \cdot N}{N})$
44		simpr	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to K \in ℤ$
45		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
46	45	adantr	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to N \in ℤ$
47		uztric	$⊢ (K \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq K} \lor K \in ℤ_{\geq N})$
48	44 46 47	syl2anc	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (N \in ℤ_{\geq K} \lor K \in ℤ_{\geq N})$
49	17 43 48	mpjaodan	$⊢ (N \in ℕ_{0} \land K \in ℤ) \to (\binom{2 \cdot N}{K}) \leq (\binom{2 \cdot N}{N})$

Metamath Proof Explorer

Theorem bcmax

Proof