This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑁 ) )