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