isumless - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > isumless		Structured version Visualization version GIF version

Theorem isumless 14747

Description: A finite sum of nonnegative numbers is less or equal to its limit. (Contributed by Mario Carneiro, 24-Apr-2014.)

**Hypotheses**
Ref	Expression
isumless.1	⊢ 𝑍 = (ℤ_≥‘𝑀)
isumless.2	⊢ (𝜑 → 𝑀 ∈ ℤ)
isumless.3	⊢ (𝜑 → 𝐴 ∈ Fin)
isumless.4	⊢ (𝜑 → 𝐴 ⊆ 𝑍)
isumless.5	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)
isumless.6	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ)
isumless.7	⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ 𝐵)
isumless.8	⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )

**Assertion**
Ref	Expression
isumless	⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ≤ Σ𝑘 ∈ 𝑍 𝐵)

Distinct variable groups: 𝐴,𝑘 𝑘,𝐹 𝑘,𝑀 𝜑,𝑘 𝑘,𝑍 Allowed substitution hint: 𝐵(𝑘)

Proof of Theorem isumless Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		isumless.4	. . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝑍)
2	1	sselda 3732	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑘 ∈ 𝑍)
3		isumless.6	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℝ)
4	3	recnd 10231	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝐵 ∈ ℂ)
5	2, 4	syldan 488	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ)
6	5	ralrimiva 3092	. . 3 ⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ)
7		isumless.1	. . . . . 6 ⊢ 𝑍 = (ℤ_≥‘𝑀)
8	7	eqimssi 3788	. . . . 5 ⊢ 𝑍 ⊆ (ℤ_≥‘𝑀)
9	8	orci 404	. . . 4 ⊢ (𝑍 ⊆ (ℤ_≥‘𝑀) ∨ 𝑍 ∈ Fin)
10	9	a1i 11	. . 3 ⊢ (𝜑 → (𝑍 ⊆ (ℤ_≥‘𝑀) ∨ 𝑍 ∈ Fin))
11		sumss2 14627	. . 3 ⊢ (((𝐴 ⊆ 𝑍 ∧ ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) ∧ (𝑍 ⊆ (ℤ_≥‘𝑀) ∨ 𝑍 ∈ Fin)) → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝑍 if(𝑘 ∈ 𝐴, 𝐵, 0))
12	1, 6, 10, 11	syl21anc 1462	. 2 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ 𝑍 if(𝑘 ∈ 𝐴, 𝐵, 0))
13		isumless.2	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℤ)
14		eleq1 2815	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴))
15		fveq2 6340	. . . . . . 7 ⊢ (𝑗 = 𝑘 → (𝐹‘𝑗) = (𝐹‘𝑘))
16	14, 15	ifbieq1d 4241	. . . . . 6 ⊢ (𝑗 = 𝑘 → if(𝑗 ∈ 𝐴, (𝐹‘𝑗), 0) = if(𝑘 ∈ 𝐴, (𝐹‘𝑘), 0))
17		eqid 2748	. . . . . 6 ⊢ (𝑗 ∈ 𝑍 ↦ if(𝑗 ∈ 𝐴, (𝐹‘𝑗), 0)) = (𝑗 ∈ 𝑍 ↦ if(𝑗 ∈ 𝐴, (𝐹‘𝑗), 0))
18		fvex 6350	. . . . . . 7 ⊢ (𝐹‘𝑘) ∈ V
19		c0ex 10197	. . . . . . 7 ⊢ 0 ∈ V
20	18, 19	ifex 4288	. . . . . 6 ⊢ if(𝑘 ∈ 𝐴, (𝐹‘𝑘), 0) ∈ V
21	16, 17, 20	fvmpt 6432	. . . . 5 ⊢ (𝑘 ∈ 𝑍 → ((𝑗 ∈ 𝑍 ↦ if(𝑗 ∈ 𝐴, (𝐹‘𝑗), 0))‘𝑘) = if(𝑘 ∈ 𝐴, (𝐹‘𝑘), 0))
22	21	adantl 473	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑗 ∈ 𝑍 ↦ if(𝑗 ∈ 𝐴, (𝐹‘𝑗), 0))‘𝑘) = if(𝑘 ∈ 𝐴, (𝐹‘𝑘), 0))
23		isumless.5	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐵)
24	23	ifeq1d 4236	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → if(𝑘 ∈ 𝐴, (𝐹‘𝑘), 0) = if(𝑘 ∈ 𝐴, 𝐵, 0))
25	22, 24	eqtrd 2782	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑗 ∈ 𝑍 ↦ if(𝑗 ∈ 𝐴, (𝐹‘𝑗), 0))‘𝑘) = if(𝑘 ∈ 𝐴, 𝐵, 0))
26		0re 10203	. . . 4 ⊢ 0 ∈ ℝ
27		ifcl 4262	. . . 4 ⊢ ((𝐵 ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℝ)
28	3, 26, 27	sylancl 697	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → if(𝑘 ∈ 𝐴, 𝐵, 0) ∈ ℝ)
29		isumless.7	. . . 4 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 0 ≤ 𝐵)
30		leid 10296	. . . . 5 ⊢ (𝐵 ∈ ℝ → 𝐵 ≤ 𝐵)
31		breq1 4795	. . . . . 6 ⊢ (𝐵 = if(𝑘 ∈ 𝐴, 𝐵, 0) → (𝐵 ≤ 𝐵 ↔ if(𝑘 ∈ 𝐴, 𝐵, 0) ≤ 𝐵))
32		breq1 4795	. . . . . 6 ⊢ (0 = if(𝑘 ∈ 𝐴, 𝐵, 0) → (0 ≤ 𝐵 ↔ if(𝑘 ∈ 𝐴, 𝐵, 0) ≤ 𝐵))
33	31, 32	ifboth 4256	. . . . 5 ⊢ ((𝐵 ≤ 𝐵 ∧ 0 ≤ 𝐵) → if(𝑘 ∈ 𝐴, 𝐵, 0) ≤ 𝐵)
34	30, 33	sylan 489	. . . 4 ⊢ ((𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) → if(𝑘 ∈ 𝐴, 𝐵, 0) ≤ 𝐵)
35	3, 29, 34	syl2anc 696	. . 3 ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → if(𝑘 ∈ 𝐴, 𝐵, 0) ≤ 𝐵)
36		isumless.3	. . . 4 ⊢ (𝜑 → 𝐴 ∈ Fin)
37	7, 13, 36, 1, 25, 5	fsumcvg3 14630	. . 3 ⊢ (𝜑 → seq𝑀( + , (𝑗 ∈ 𝑍 ↦ if(𝑗 ∈ 𝐴, (𝐹‘𝑗), 0))) ∈ dom ⇝ )
38		isumless.8	. . 3 ⊢ (𝜑 → seq𝑀( + , 𝐹) ∈ dom ⇝ )
39	7, 13, 25, 28, 23, 3, 35, 37, 38	isumle 14746	. 2 ⊢ (𝜑 → Σ𝑘 ∈ 𝑍 if(𝑘 ∈ 𝐴, 𝐵, 0) ≤ Σ𝑘 ∈ 𝑍 𝐵)
40	12, 39	eqbrtrd 4814	1 ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ≤ Σ𝑘 ∈ 𝑍 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∨ wo 382 ∧ wa 383 = wceq 1620 ∈ wcel 2127 ∀wral 3038 ⊆ wss 3703 ifcif 4218 class class class wbr 4792 ↦ cmpt 4869 dom cdm 5254 ‘cfv 6037 Fincfn 8109 ℂcc 10097 ℝcr 10098 0cc0 10099 + caddc 10102 ≤ cle 10238 ℤcz 11540 ℤ_≥cuz 11850 seqcseq 12966 ⇝ cli 14385 Σcsu 14586

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1859 ax-4 1874 ax-5 1976 ax-6 2042 ax-7 2078 ax-8 2129 ax-9 2136 ax-10 2156 ax-11 2171 ax-12 2184 ax-13 2379 ax-ext 2728 ax-rep 4911 ax-sep 4921 ax-nul 4929 ax-pow 4980 ax-pr 5043 ax-un 7102 ax-inf2 8699 ax-cnex 10155 ax-resscn 10156 ax-1cn 10157 ax-icn 10158 ax-addcl 10159 ax-addrcl 10160 ax-mulcl 10161 ax-mulrcl 10162 ax-mulcom 10163 ax-addass 10164 ax-mulass 10165 ax-distr 10166 ax-i2m1 10167 ax-1ne0 10168 ax-1rid 10169 ax-rnegex 10170 ax-rrecex 10171 ax-cnre 10172 ax-pre-lttri 10173 ax-pre-lttrn 10174 ax-pre-ltadd 10175 ax-pre-mulgt0 10176 ax-pre-sup 10177

This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3or 1073 df-3an 1074 df-tru 1623 df-fal 1626 df-ex 1842 df-nf 1847 df-sb 2035 df-eu 2599 df-mo 2600 df-clab 2735 df-cleq 2741 df-clel 2744 df-nfc 2879 df-ne 2921 df-nel 3024 df-ral 3043 df-rex 3044 df-reu 3045 df-rmo 3046 df-rab 3047 df-v 3330 df-sbc 3565 df-csb 3663 df-dif 3706 df-un 3708 df-in 3710 df-ss 3717 df-pss 3719 df-nul 4047 df-if 4219 df-pw 4292 df-sn 4310 df-pr 4312 df-tp 4314 df-op 4316 df-uni 4577 df-int 4616 df-iun 4662 df-br 4793 df-opab 4853 df-mpt 4870 df-tr 4893 df-id 5162 df-eprel 5167 df-po 5175 df-so 5176 df-fr 5213 df-se 5214 df-we 5215 df-xp 5260 df-rel 5261 df-cnv 5262 df-co 5263 df-dm 5264 df-rn 5265 df-res 5266 df-ima 5267 df-pred 5829 df-ord 5875 df-on 5876 df-lim 5877 df-suc 5878 df-iota 6000 df-fun 6039 df-fn 6040 df-f 6041 df-f1 6042 df-fo 6043 df-f1o 6044 df-fv 6045 df-isom 6046 df-riota 6762 df-ov 6804 df-oprab 6805 df-mpt2 6806 df-om 7219 df-1st 7321 df-2nd 7322 df-wrecs 7564 df-recs 7625 df-rdg 7663 df-1o 7717 df-oadd 7721 df-er 7899 df-pm 8014 df-en 8110 df-dom 8111 df-sdom 8112 df-fin 8113 df-sup 8501 df-inf 8502 df-oi 8568 df-card 8926 df-pnf 10239 df-mnf 10240 df-xr 10241 df-ltxr 10242 df-le 10243 df-sub 10431 df-neg 10432 df-div 10848 df-nn 11184 df-2 11242 df-3 11243 df-n0 11456 df-z 11541 df-uz 11851 df-rp 11997 df-fz 12491 df-fzo 12631 df-fl 12758 df-seq 12967 df-exp 13026 df-hash 13283 df-cj 14009 df-re 14010 df-im 14011 df-sqrt 14145 df-abs 14146 df-clim 14389 df-rlim 14390 df-sum 14587

This theorem is referenced by: isumltss 14750 climcnds 14753 harmonic 14761 mertenslem1 14786 prmreclem5 15797 ovoliunlem1 23441 ovoliun2 23445 esumpcvgval 30420 eulerpartlems 30702 geomcau 33837

W3C validator