Theorem lcmineqlem17

Description: Inequality of 2^{2n}. (Contributed by metakunt, 29-Apr-2024)

	Ref	Expression
Hypothesis	lcmineqlem17.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
Assertion	lcmineqlem17	⊢ ( 𝜑 → ( 2 ↑ ( 2 · 𝑁 ) ) ≤ ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) )

Proof

Step	Hyp	Ref	Expression
1		lcmineqlem17.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2		2nn0	⊢ 2 ∈ ℕ0
3	2	a1i	⊢ ( 𝜑 → 2 ∈ ℕ0 )
4	3 1	nn0mulcld	⊢ ( 𝜑 → ( 2 · 𝑁 ) ∈ ℕ0 )
5		binom11	⊢ ( ( 2 · 𝑁 ) ∈ ℕ0 → ( 2 ↑ ( 2 · 𝑁 ) ) = Σ 𝑘 ∈ ( 0 ... ( 2 · 𝑁 ) ) ( ( 2 · 𝑁 ) C 𝑘 ) )
6	4 5	syl	⊢ ( 𝜑 → ( 2 ↑ ( 2 · 𝑁 ) ) = Σ 𝑘 ∈ ( 0 ... ( 2 · 𝑁 ) ) ( ( 2 · 𝑁 ) C 𝑘 ) )
7		fzfid	⊢ ( 𝜑 → ( 0 ... ( 2 · 𝑁 ) ) ∈ Fin )
8	4	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 2 · 𝑁 ) ) ) → ( 2 · 𝑁 ) ∈ ℕ0 )
9		elfzelz	⊢ ( 𝑘 ∈ ( 0 ... ( 2 · 𝑁 ) ) → 𝑘 ∈ ℤ )
10	9	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 2 · 𝑁 ) ) ) → 𝑘 ∈ ℤ )
11	8 10	jca	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 2 · 𝑁 ) ) ) → ( ( 2 · 𝑁 ) ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) )
12		bccl	⊢ ( ( ( 2 · 𝑁 ) ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( ( 2 · 𝑁 ) C 𝑘 ) ∈ ℕ0 )
13	11 12	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 2 · 𝑁 ) ) ) → ( ( 2 · 𝑁 ) C 𝑘 ) ∈ ℕ0 )
14	13	nn0red	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 2 · 𝑁 ) ) ) → ( ( 2 · 𝑁 ) C 𝑘 ) ∈ ℝ )
15	1	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
16		bccl	⊢ ( ( ( 2 · 𝑁 ) ∈ ℕ0 ∧ 𝑁 ∈ ℤ ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ0 )
17	4 15 16	syl2anc	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℕ0 )
18	17	nn0red	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℝ )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 2 · 𝑁 ) ) ) → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℝ )
20		bcmax	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( ( 2 · 𝑁 ) C 𝑘 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) )
21	1 9 20	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 2 · 𝑁 ) ) ) → ( ( 2 · 𝑁 ) C 𝑘 ) ≤ ( ( 2 · 𝑁 ) C 𝑁 ) )
22	7 14 19 21	fsumle	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 2 · 𝑁 ) ) ( ( 2 · 𝑁 ) C 𝑘 ) ≤ Σ 𝑘 ∈ ( 0 ... ( 2 · 𝑁 ) ) ( ( 2 · 𝑁 ) C 𝑁 ) )
23	6 22	eqbrtrd	⊢ ( 𝜑 → ( 2 ↑ ( 2 · 𝑁 ) ) ≤ Σ 𝑘 ∈ ( 0 ... ( 2 · 𝑁 ) ) ( ( 2 · 𝑁 ) C 𝑁 ) )
24	17	nn0cnd	⊢ ( 𝜑 → ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℂ )
25		fsumconst	⊢ ( ( ( 0 ... ( 2 · 𝑁 ) ) ∈ Fin ∧ ( ( 2 · 𝑁 ) C 𝑁 ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... ( 2 · 𝑁 ) ) ( ( 2 · 𝑁 ) C 𝑁 ) = ( ( ♯ ‘ ( 0 ... ( 2 · 𝑁 ) ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) )
26	7 24 25	syl2anc	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 2 · 𝑁 ) ) ( ( 2 · 𝑁 ) C 𝑁 ) = ( ( ♯ ‘ ( 0 ... ( 2 · 𝑁 ) ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) )
27		hashfz0	⊢ ( ( 2 · 𝑁 ) ∈ ℕ0 → ( ♯ ‘ ( 0 ... ( 2 · 𝑁 ) ) ) = ( ( 2 · 𝑁 ) + 1 ) )
28	4 27	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 0 ... ( 2 · 𝑁 ) ) ) = ( ( 2 · 𝑁 ) + 1 ) )
29	28	oveq1d	⊢ ( 𝜑 → ( ( ♯ ‘ ( 0 ... ( 2 · 𝑁 ) ) ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) = ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) )
30	26 29	eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 2 · 𝑁 ) ) ( ( 2 · 𝑁 ) C 𝑁 ) = ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) )
31	23 30	breqtrd	⊢ ( 𝜑 → ( 2 ↑ ( 2 · 𝑁 ) ) ≤ ( ( ( 2 · 𝑁 ) + 1 ) · ( ( 2 · 𝑁 ) C 𝑁 ) ) )