Theorem bcmax

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

	Ref	Expression
Assertion	bcmax	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( ( 2 · 𝑁 ) C 𝐾 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		2nn0	⊢ 2 ∈ ℕ0
2		simpll	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑁 ∈ ℕ0 )
3		nn0mulcl	⊢ ( ( 2 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ) → ( 2 · 𝑁 ) ∈ ℕ0 )
4	1 2 3	sylancr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( 2 · 𝑁 ) ∈ ℕ0 )
5		simpr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
6		nn0re	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
7	6	leidd	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ≤ 𝑁 )
8		nn0cn	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℂ )
9		2cn	⊢ 2 ∈ ℂ
10		2ne0	⊢ 2 ≠ 0
11		divcan3	⊢ ( ( 𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 2 · 𝑁 ) / 2 ) = 𝑁 )
12	9 10 11	mp3an23	⊢ ( 𝑁 ∈ ℂ → ( ( 2 · 𝑁 ) / 2 ) = 𝑁 )
13	8 12	syl	⊢ ( 𝑁 ∈ ℕ0 → ( ( 2 · 𝑁 ) / 2 ) = 𝑁 )
14	7 13	breqtrrd	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ≤ ( ( 2 · 𝑁 ) / 2 ) )
15	2 14	syl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → 𝑁 ≤ ( ( 2 · 𝑁 ) / 2 ) )
16		bcmono	⊢ ( ( ( 2 · 𝑁 ) ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ∧ 𝑁 ≤ ( ( 2 · 𝑁 ) / 2 ) ) → ( ( 2 · 𝑁 ) C 𝐾 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) )
17	4 5 15 16	syl3anc	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ) → ( ( 2 · 𝑁 ) C 𝐾 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) )
18		simpll	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℕ0 )
19	1 18 3	sylancr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 · 𝑁 ) ∈ ℕ0 )
20		simplr	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐾 ∈ ℤ )
21		bccmpl	⊢ ( ( ( 2 · 𝑁 ) ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( ( 2 · 𝑁 ) C 𝐾 ) = ( ( 2 · 𝑁 ) C ( ( 2 · 𝑁 ) − 𝐾 ) ) )
22	19 20 21	syl2anc	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 · 𝑁 ) C 𝐾 ) = ( ( 2 · 𝑁 ) C ( ( 2 · 𝑁 ) − 𝐾 ) ) )
23	18	nn0red	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℝ )
24	23	recnd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℂ )
25	24	2timesd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 · 𝑁 ) = ( 𝑁 + 𝑁 ) )
26	20	zred	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝐾 ∈ ℝ )
27		eluzle	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ≤ 𝐾 )
28	27	adantl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ≤ 𝐾 )
29	23 26 23 28	leadd2dd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑁 + 𝑁 ) ≤ ( 𝑁 + 𝐾 ) )
30	25 29	eqbrtrd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 · 𝑁 ) ≤ ( 𝑁 + 𝐾 ) )
31	19	nn0red	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 · 𝑁 ) ∈ ℝ )
32	31 26 23	lesubaddd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( ( 2 · 𝑁 ) − 𝐾 ) ≤ 𝑁 ↔ ( 2 · 𝑁 ) ≤ ( 𝑁 + 𝐾 ) ) )
33	30 32	mpbird	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 · 𝑁 ) − 𝐾 ) ≤ 𝑁 )
34	19	nn0zd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 2 · 𝑁 ) ∈ ℤ )
35	34 20	zsubcld	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 · 𝑁 ) − 𝐾 ) ∈ ℤ )
36	18	nn0zd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ℤ )
37		eluz	⊢ ( ( ( ( 2 · 𝑁 ) − 𝐾 ) ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( ( 2 · 𝑁 ) − 𝐾 ) ) ↔ ( ( 2 · 𝑁 ) − 𝐾 ) ≤ 𝑁 ) )
38	35 36 37	syl2anc	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( 𝑁 ∈ ( ℤ≥ ‘ ( ( 2 · 𝑁 ) − 𝐾 ) ) ↔ ( ( 2 · 𝑁 ) − 𝐾 ) ≤ 𝑁 ) )
39	33 38	mpbird	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ∈ ( ℤ≥ ‘ ( ( 2 · 𝑁 ) − 𝐾 ) ) )
40	18 14	syl	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → 𝑁 ≤ ( ( 2 · 𝑁 ) / 2 ) )
41		bcmono	⊢ ( ( ( 2 · 𝑁 ) ∈ ℕ0 ∧ 𝑁 ∈ ( ℤ≥ ‘ ( ( 2 · 𝑁 ) − 𝐾 ) ) ∧ 𝑁 ≤ ( ( 2 · 𝑁 ) / 2 ) ) → ( ( 2 · 𝑁 ) C ( ( 2 · 𝑁 ) − 𝐾 ) ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) )
42	19 39 40 41	syl3anc	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 · 𝑁 ) C ( ( 2 · 𝑁 ) − 𝐾 ) ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) )
43	22 42	eqbrtrd	⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) ∧ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) → ( ( 2 · 𝑁 ) C 𝐾 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) )
44		simpr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → 𝐾 ∈ ℤ )
45		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
46	45	adantr	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → 𝑁 ∈ ℤ )
47		uztric	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ∨ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
48	44 46 47	syl2anc	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) ∨ 𝐾 ∈ ( ℤ≥ ‘ 𝑁 ) ) )
49	17 43 48	mpjaodan	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐾 ∈ ℤ ) → ( ( 2 · 𝑁 ) C 𝐾 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) )