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 -> B = D )
	fsumub.2	|- ( ph -> A e. Fin )
	fsumub.3	|- ( ph -> sum_ k e. A B = C )
	fsumub.4	|- ( ( ph /\ k e. A ) -> B e. RR+ )
	fsumub.k	|- ( ph -> K e. A )
Assertion	fsumub	|- ( ph -> D <_ C )

Proof

Step	Hyp	Ref	Expression
1		fsumub.1	|- ( k = K -> B = D )
2		fsumub.2	|- ( ph -> A e. Fin )
3		fsumub.3	|- ( ph -> sum_ k e. A B = C )
4		fsumub.4	|- ( ( ph /\ k e. A ) -> B e. RR+ )
5		fsumub.k	|- ( ph -> K e. A )
6	4	rpred	|- ( ( ph /\ k e. A ) -> B e. RR )
7	4	rpge0d	|- ( ( ph /\ k e. A ) -> 0 <_ B )
8	2 6 7 1 5	fsumge1	|- ( ph -> D <_ sum_ k e. A B )
9	8 3	breqtrd	|- ( ph -> D <_ C )