Theorem fsumub

Description: An upper bound for a term of a positive finite sum. (Contributed by Thierry Arnoux, 27-Dec-2021)

	Ref	Expression
Hypotheses	fsumub.1	$$⊢k=K\to B=D$$
	fsumub.2	$$⊢\phi \to A\in \mathrm{Fin}$$
	fsumub.3	$$⊢\phi \to \sum _{k\in A}B=C$$
	fsumub.4	$$⊢\left(\phi \wedge k\in A\right)\to B\in {ℝ}^{+}$$
	fsumub.k	$$⊢\phi \to K\in A$$
Assertion	fsumub	$$⊢\phi \to D\le C$$

Proof

Step	Hyp	Ref	Expression
1		fsumub.1	$$⊢k=K\to B=D$$
2		fsumub.2	$$⊢\phi \to A\in \mathrm{Fin}$$
3		fsumub.3	$$⊢\phi \to \sum _{k\in A}B=C$$
4		fsumub.4	$$⊢\left(\phi \wedge k\in A\right)\to B\in {ℝ}^{+}$$
5		fsumub.k	$$⊢\phi \to K\in A$$
6	4	rpred	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℝ$$
7	4	rpge0d	$$⊢\left(\phi \wedge k\in A\right)\to 0\le B$$
8	2 6 7 1 5	fsumge1	$$⊢\phi \to D\le \sum _{k\in A}B$$
9	8 3	breqtrd	$$⊢\phi \to D\le C$$