lcmineqlem17 - Mathbox for metakunt

	Mathbox for metakunt		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > lcmineqlem17		Structured version Visualization version GIF version

Theorem lcmineqlem17 42161

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

**Hypothesis**
Ref	Expression
lcmineqlem17.1	⊢ (𝜑 → 𝑁 ∈ ℕ₀)

**Assertion**
Ref	Expression
lcmineqlem17	⊢ (𝜑 → (2↑(2 · 𝑁)) ≤ (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁)))

Proof of Theorem lcmineqlem17 Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2nn0 12407	. . . . . 6 ⊢ 2 ∈ ℕ₀
2	1	a1i 11	. . . . 5 ⊢ (𝜑 → 2 ∈ ℕ₀)
3		lcmineqlem17.1	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
4	2, 3	nn0mulcld 12456	. . . 4 ⊢ (𝜑 → (2 · 𝑁) ∈ ℕ₀)
5		binom11 15743	. . . 4 ⊢ ((2 · 𝑁) ∈ ℕ₀ → (2↑(2 · 𝑁)) = Σ𝑘 ∈ (0...(2 · 𝑁))((2 · 𝑁)C𝑘))
6	4, 5	syl 17	. . 3 ⊢ (𝜑 → (2↑(2 · 𝑁)) = Σ𝑘 ∈ (0...(2 · 𝑁))((2 · 𝑁)C𝑘))
7		fzfid 13884	. . . 4 ⊢ (𝜑 → (0...(2 · 𝑁)) ∈ Fin)
8	4	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(2 · 𝑁))) → (2 · 𝑁) ∈ ℕ₀)
9		elfzelz 13428	. . . . . . . 8 ⊢ (𝑘 ∈ (0...(2 · 𝑁)) → 𝑘 ∈ ℤ)
10	9	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(2 · 𝑁))) → 𝑘 ∈ ℤ)
11	8, 10	jca 511	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(2 · 𝑁))) → ((2 · 𝑁) ∈ ℕ₀ ∧ 𝑘 ∈ ℤ))
12		bccl 14233	. . . . . 6 ⊢ (((2 · 𝑁) ∈ ℕ₀ ∧ 𝑘 ∈ ℤ) → ((2 · 𝑁)C𝑘) ∈ ℕ₀)
13	11, 12	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(2 · 𝑁))) → ((2 · 𝑁)C𝑘) ∈ ℕ₀)
14	13	nn0red 12452	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(2 · 𝑁))) → ((2 · 𝑁)C𝑘) ∈ ℝ)
15	3	nn0zd 12502	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℤ)
16		bccl 14233	. . . . . . 7 ⊢ (((2 · 𝑁) ∈ ℕ₀ ∧ 𝑁 ∈ ℤ) → ((2 · 𝑁)C𝑁) ∈ ℕ₀)
17	4, 15, 16	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℕ₀)
18	17	nn0red 12452	. . . . 5 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℝ)
19	18	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(2 · 𝑁))) → ((2 · 𝑁)C𝑁) ∈ ℝ)
20		bcmax 27219	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑘 ∈ ℤ) → ((2 · 𝑁)C𝑘) ≤ ((2 · 𝑁)C𝑁))
21	3, 9, 20	syl2an 596	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(2 · 𝑁))) → ((2 · 𝑁)C𝑘) ≤ ((2 · 𝑁)C𝑁))
22	7, 14, 19, 21	fsumle 15710	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ (0...(2 · 𝑁))((2 · 𝑁)C𝑘) ≤ Σ𝑘 ∈ (0...(2 · 𝑁))((2 · 𝑁)C𝑁))
23	6, 22	eqbrtrd 5117	. 2 ⊢ (𝜑 → (2↑(2 · 𝑁)) ≤ Σ𝑘 ∈ (0...(2 · 𝑁))((2 · 𝑁)C𝑁))
24	17	nn0cnd 12453	. . . 4 ⊢ (𝜑 → ((2 · 𝑁)C𝑁) ∈ ℂ)
25		fsumconst 15701	. . . 4 ⊢ (((0...(2 · 𝑁)) ∈ Fin ∧ ((2 · 𝑁)C𝑁) ∈ ℂ) → Σ𝑘 ∈ (0...(2 · 𝑁))((2 · 𝑁)C𝑁) = ((♯‘(0...(2 · 𝑁))) · ((2 · 𝑁)C𝑁)))
26	7, 24, 25	syl2anc 584	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ (0...(2 · 𝑁))((2 · 𝑁)C𝑁) = ((♯‘(0...(2 · 𝑁))) · ((2 · 𝑁)C𝑁)))
27		hashfz0 14343	. . . . 5 ⊢ ((2 · 𝑁) ∈ ℕ₀ → (♯‘(0...(2 · 𝑁))) = ((2 · 𝑁) + 1))
28	4, 27	syl 17	. . . 4 ⊢ (𝜑 → (♯‘(0...(2 · 𝑁))) = ((2 · 𝑁) + 1))
29	28	oveq1d 7369	. . 3 ⊢ (𝜑 → ((♯‘(0...(2 · 𝑁))) · ((2 · 𝑁)C𝑁)) = (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁)))
30	26, 29	eqtrd 2768	. 2 ⊢ (𝜑 → Σ𝑘 ∈ (0...(2 · 𝑁))((2 · 𝑁)C𝑁) = (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁)))
31	23, 30	breqtrd 5121	1 ⊢ (𝜑 → (2↑(2 · 𝑁)) ≤ (((2 · 𝑁) + 1) · ((2 · 𝑁)C𝑁)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2113 class class class wbr 5095 ‘cfv 6488 (class class class)co 7354 Fincfn 8877 ℂcc 11013 ℝcr 11014 0cc0 11015 1c1 11016 + caddc 11018 · cmul 11020 ≤ cle 11156 2c2 12189 ℕ₀cn0 12390 ℤcz 12477 ...cfz 13411 ↑cexp 13972 Ccbc 14213 ♯chash 14241 Σcsu 15597

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7676 ax-inf2 9540 ax-cnex 11071 ax-resscn 11072 ax-1cn 11073 ax-icn 11074 ax-addcl 11075 ax-addrcl 11076 ax-mulcl 11077 ax-mulrcl 11078 ax-mulcom 11079 ax-addass 11080 ax-mulass 11081 ax-distr 11082 ax-i2m1 11083 ax-1ne0 11084 ax-1rid 11085 ax-rnegex 11086 ax-rrecex 11087 ax-cnre 11088 ax-pre-lttri 11089 ax-pre-lttrn 11090 ax-pre-ltadd 11091 ax-pre-mulgt0 11092 ax-pre-sup 11093

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-int 4900 df-iun 4945 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-se 5575 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6255 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6444 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-isom 6497 df-riota 7311 df-ov 7357 df-oprab 7358 df-mpo 7359 df-om 7805 df-1st 7929 df-2nd 7930 df-frecs 8219 df-wrecs 8250 df-recs 8299 df-rdg 8337 df-1o 8393 df-er 8630 df-en 8878 df-dom 8879 df-sdom 8880 df-fin 8881 df-sup 9335 df-oi 9405 df-card 9841 df-pnf 11157 df-mnf 11158 df-xr 11159 df-ltxr 11160 df-le 11161 df-sub 11355 df-neg 11356 df-div 11784 df-nn 12135 df-2 12197 df-3 12198 df-n0 12391 df-z 12478 df-uz 12741 df-rp 12895 df-ico 13255 df-fz 13412 df-fzo 13559 df-seq 13913 df-exp 13973 df-fac 14185 df-bc 14214 df-hash 14242 df-cj 15010 df-re 15011 df-im 15012 df-sqrt 15146 df-abs 15147 df-clim 15399 df-sum 15598

This theorem is referenced by: lcmineqlem20 42164

W3C validator