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 ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ( 0 ... ( 2 · 𝑁 ) ) )

Proof

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