Theorem isumless

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

	Ref	Expression
Hypotheses	isumless.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	isumless.2	$$⊢\phi \to M\in \mathbb{Z}$$
	isumless.3	$$⊢\phi \to A\in \mathrm{Fin}$$
	isumless.4	$$⊢\phi \to A\subseteq Z$$
	isumless.5	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=B$$
	isumless.6	$$⊢\left(\phi \wedge k\in Z\right)\to B\in ℝ$$
	isumless.7	$$⊢\left(\phi \wedge k\in Z\right)\to 0\le B$$
	isumless.8	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
Assertion	isumless	$$⊢\phi \to \sum _{k\in A}B\le \sum _{k\in Z}B$$

Proof

Step	Hyp	Ref	Expression
1		isumless.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		isumless.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		isumless.3	$$⊢\phi \to A\in \mathrm{Fin}$$
4		isumless.4	$$⊢\phi \to A\subseteq Z$$
5		isumless.5	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=B$$
6		isumless.6	$$⊢\left(\phi \wedge k\in Z\right)\to B\in ℝ$$
7		isumless.7	$$⊢\left(\phi \wedge k\in Z\right)\to 0\le B$$
8		isumless.8	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
9	4	sselda	$$⊢\left(\phi \wedge k\in A\right)\to k\in Z$$
10	6	recnd	$$⊢\left(\phi \wedge k\in Z\right)\to B\in ℂ$$
11	9 10	syldan	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
12	11	ralrimiva	$$⊢\phi \to \forall k\in AB\in ℂ$$
13	1	eqimssi	$$⊢Z\subseteq {\mathbb{Z}}_{\ge M}$$
14	13	orci	$$⊢\left(Z\subseteq {\mathbb{Z}}_{\ge M}\vee Z\in \mathrm{Fin}\right)$$
15	14	a1i	$$⊢\phi \to \left(Z\subseteq {\mathbb{Z}}_{\ge M}\vee Z\in \mathrm{Fin}\right)$$
16		sumss2	$$⊢\left(\left(A\subseteq Z\wedge \forall k\in AB\in ℂ\right)\wedge \left(Z\subseteq {\mathbb{Z}}_{\ge M}\vee Z\in \mathrm{Fin}\right)\right)\to \sum _{k\in A}B=\sum _{k\in Z}if\left(k\in A,B,0\right)$$
17	4 12 15 16	syl21anc	$$⊢\phi \to \sum _{k\in A}B=\sum _{k\in Z}if\left(k\in A,B,0\right)$$
18		eleq1w	$$⊢j=k\to \left(j\in A\leftrightarrow k\in A\right)$$
19		fveq2	$$⊢j=k\to F\left(j\right)=F\left(k\right)$$
20	18 19	ifbieq1d	$$⊢j=k\to if\left(j\in A,F\left(j\right),0\right)=if\left(k\in A,F\left(k\right),0\right)$$
21		eqid	$$⊢\left(j\in Z⟼if\left(j\in A,F\left(j\right),0\right)\right)=\left(j\in Z⟼if\left(j\in A,F\left(j\right),0\right)\right)$$
22		fvex	$$⊢F\left(k\right)\in \mathrm{V}$$
23		c0ex	$$⊢0\in \mathrm{V}$$
24	22 23	ifex	$$⊢if\left(k\in A,F\left(k\right),0\right)\in \mathrm{V}$$
25	20 21 24	fvmpt	$$⊢k\in Z\to \left(j\in Z⟼if\left(j\in A,F\left(j\right),0\right)\right)\left(k\right)=if\left(k\in A,F\left(k\right),0\right)$$
26	25	adantl	$$⊢\left(\phi \wedge k\in Z\right)\to \left(j\in Z⟼if\left(j\in A,F\left(j\right),0\right)\right)\left(k\right)=if\left(k\in A,F\left(k\right),0\right)$$
27	5	ifeq1d	$$⊢\left(\phi \wedge k\in Z\right)\to if\left(k\in A,F\left(k\right),0\right)=if\left(k\in A,B,0\right)$$
28	26 27	eqtrd	$$⊢\left(\phi \wedge k\in Z\right)\to \left(j\in Z⟼if\left(j\in A,F\left(j\right),0\right)\right)\left(k\right)=if\left(k\in A,B,0\right)$$
29		0re	$$⊢0\in ℝ$$
30		ifcl	$$⊢\left(B\in ℝ\wedge 0\in ℝ\right)\to if\left(k\in A,B,0\right)\in ℝ$$
31	6 29 30	sylancl	$$⊢\left(\phi \wedge k\in Z\right)\to if\left(k\in A,B,0\right)\in ℝ$$
32		leid	$$⊢B\in ℝ\to B\le B$$
33		breq1	$$⊢B=if\left(k\in A,B,0\right)\to \left(B\le B\leftrightarrow if\left(k\in A,B,0\right)\le B\right)$$
34		breq1	$$⊢0=if\left(k\in A,B,0\right)\to \left(0\le B\leftrightarrow if\left(k\in A,B,0\right)\le B\right)$$
35	33 34	ifboth	$$⊢\left(B\le B\wedge 0\le B\right)\to if\left(k\in A,B,0\right)\le B$$
36	32 35	sylan	$$⊢\left(B\in ℝ\wedge 0\le B\right)\to if\left(k\in A,B,0\right)\le B$$
37	6 7 36	syl2anc	$$⊢\left(\phi \wedge k\in Z\right)\to if\left(k\in A,B,0\right)\le B$$
38	1 2 3 4 28 11	fsumcvg3	$$⊢\phi \to seqM\left(+,\left(j\in Z⟼if\left(j\in A,F\left(j\right),0\right)\right)\right)\in \mathrm{dom}⇝$$
39	1 2 28 31 5 6 37 38 8	isumle	$$⊢\phi \to \sum _{k\in Z}if\left(k\in A,B,0\right)\le \sum _{k\in Z}B$$
40	17 39	eqbrtrd	$$⊢\phi \to \sum _{k\in A}B\le \sum _{k\in Z}B$$