lcmineqlem17

		Ref	Expression
	Hypothesis	lcmineqlem17.1	$⊢ φ \to N \in ℕ_{0}$
	Assertion	lcmineqlem17	$⊢ φ \to 2^{2 \cdot N} \leq (2 \cdot N + 1) (\binom{2 \cdot N}{N})$

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem17.1	$⊢ φ \to N \in ℕ_{0}$
2		2nn0	$⊢ 2 \in ℕ_{0}$
3	2	a1i	$⊢ φ \to 2 \in ℕ_{0}$
4	3 1	nn0mulcld	$⊢ φ \to 2 \cdot N \in ℕ_{0}$
5		binom11	$⊢ 2 \cdot N \in ℕ_{0} \to 2^{2 \cdot N} = \sum_{k = 0}^{2 \cdot N} (\binom{2 \cdot N}{k})$
6	4 5	syl	$⊢ φ \to 2^{2 \cdot N} = \sum_{k = 0}^{2 \cdot N} (\binom{2 \cdot N}{k})$
7		fzfid	$⊢ φ \to (0 \dots 2 \cdot N) \in Fin$
8	4	adantr	$⊢ (φ \land k \in (0 \dots 2 \cdot N)) \to 2 \cdot N \in ℕ_{0}$
9		elfzelz	$⊢ k \in (0 \dots 2 \cdot N) \to k \in ℤ$
10	9	adantl	$⊢ (φ \land k \in (0 \dots 2 \cdot N)) \to k \in ℤ$
11	8 10	jca	$⊢ (φ \land k \in (0 \dots 2 \cdot N)) \to (2 \cdot N \in ℕ_{0} \land k \in ℤ)$
12		bccl	$⊢ (2 \cdot N \in ℕ_{0} \land k \in ℤ) \to (\binom{2 \cdot N}{k}) \in ℕ_{0}$
13	11 12	syl	$⊢ (φ \land k \in (0 \dots 2 \cdot N)) \to (\binom{2 \cdot N}{k}) \in ℕ_{0}$
14	13	nn0red	$⊢ (φ \land k \in (0 \dots 2 \cdot N)) \to (\binom{2 \cdot N}{k}) \in ℝ$
15	1	nn0zd	$⊢ φ \to N \in ℤ$
16		bccl	$⊢ (2 \cdot N \in ℕ_{0} \land N \in ℤ) \to (\binom{2 \cdot N}{N}) \in ℕ_{0}$
17	4 15 16	syl2anc	$⊢ φ \to (\binom{2 \cdot N}{N}) \in ℕ_{0}$
18	17	nn0red	$⊢ φ \to (\binom{2 \cdot N}{N}) \in ℝ$
19	18	adantr	$⊢ (φ \land k \in (0 \dots 2 \cdot N)) \to (\binom{2 \cdot N}{N}) \in ℝ$
20		bcmax	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{2 \cdot N}{k}) \leq (\binom{2 \cdot N}{N})$
21	1 9 20	syl2an	$⊢ (φ \land k \in (0 \dots 2 \cdot N)) \to (\binom{2 \cdot N}{k}) \leq (\binom{2 \cdot N}{N})$
22	7 14 19 21	fsumle	$⊢ φ \to \sum_{k = 0}^{2 \cdot N} (\binom{2 \cdot N}{k}) \leq \sum_{k = 0}^{2 \cdot N} (\binom{2 \cdot N}{N})$
23	6 22	eqbrtrd	$⊢ φ \to 2^{2 \cdot N} \leq \sum_{k = 0}^{2 \cdot N} (\binom{2 \cdot N}{N})$
24	17	nn0cnd	$⊢ φ \to (\binom{2 \cdot N}{N}) \in ℂ$
25		fsumconst	$⊢ ((0 \dots 2 \cdot N) \in Fin \land (\binom{2 \cdot N}{N}) \in ℂ) \to \sum_{k = 0}^{2 \cdot N} (\binom{2 \cdot N}{N}) = \|(0 \dots 2 \cdot N)\| (\binom{2 \cdot N}{N})$
26	7 24 25	syl2anc	$⊢ φ \to \sum_{k = 0}^{2 \cdot N} (\binom{2 \cdot N}{N}) = \|(0 \dots 2 \cdot N)\| (\binom{2 \cdot N}{N})$
27		hashfz0	$⊢ 2 \cdot N \in ℕ_{0} \to \|(0 \dots 2 \cdot N)\| = 2 \cdot N + 1$
28	4 27	syl	$⊢ φ \to \|(0 \dots 2 \cdot N)\| = 2 \cdot N + 1$
29	28	oveq1d	$⊢ φ \to \|(0 \dots 2 \cdot N)\| (\binom{2 \cdot N}{N}) = (2 \cdot N + 1) (\binom{2 \cdot N}{N})$
30	26 29	eqtrd	$⊢ φ \to \sum_{k = 0}^{2 \cdot N} (\binom{2 \cdot N}{N}) = (2 \cdot N + 1) (\binom{2 \cdot N}{N})$
31	23 30	breqtrd	$⊢ φ \to 2^{2 \cdot N} \leq (2 \cdot N + 1) (\binom{2 \cdot N}{N})$

Metamath Proof Explorer

Theorem lcmineqlem17

Proof