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

Metamath Proof Explorer

Theorem fzctr

Description: Lemma for theorems about the central binomial coefficient. (Contributed by Mario Carneiro, 8-Mar-2014) (Revised by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion fzctr ⊢ N ∈ ℕ 0 → N ∈ 0 … 2 ⋅ N

Proof

Step Hyp Ref Expression
1 nn0ge0 ⊢ N ∈ ℕ 0 → 0 ≤ N
2 nn0re ⊢ N ∈ ℕ 0 → N ∈ ℝ
3 nn0addge1 ⊢ N ∈ ℝ ∧ N ∈ ℕ 0 → N ≤ N + N
4 2 3 mpancom ⊢ N ∈ ℕ 0 → N ≤ N + N
5 nn0cn ⊢ N ∈ ℕ 0 → N ∈ ℂ
6 5 2timesd ⊢ N ∈ ℕ 0 → 2 ⋅ N = N + N
7 4 6 breqtrrd ⊢ N ∈ ℕ 0 → N ≤ 2 ⋅ N
8 nn0z ⊢ N ∈ ℕ 0 → N ∈ ℤ
9 0zd ⊢ N ∈ ℕ 0 → 0 ∈ ℤ
10 2z ⊢ 2 ∈ ℤ
11 zmulcl ⊢ 2 ∈ ℤ ∧ N ∈ ℤ → 2 ⋅ N ∈ ℤ
12 10 8 11 sylancr ⊢ N ∈ ℕ 0 → 2 ⋅ N ∈ ℤ
13 elfz ⊢ N ∈ ℤ ∧ 0 ∈ ℤ ∧ 2 ⋅ N ∈ ℤ → N ∈ 0 … 2 ⋅ N ↔ 0 ≤ N ∧ N ≤ 2 ⋅ N
14 8 9 12 13 syl3anc ⊢ N ∈ ℕ 0 → N ∈ 0 … 2 ⋅ N ↔ 0 ≤ N ∧ N ≤ 2 ⋅ N
15 1 7 14 mpbir2and ⊢ N ∈ ℕ 0 → N ∈ 0 … 2 ⋅ N