Metamath Proof Explorer

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