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	⊢ ( 𝑘 = 𝐾 → 𝐵 = 𝐷 )
	fsumub.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	fsumub.3	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 = 𝐶 )
	fsumub.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ+ )
	fsumub.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐴 )
Assertion	fsumub	⊢ ( 𝜑 → 𝐷 ≤ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		fsumub.1	⊢ ( 𝑘 = 𝐾 → 𝐵 = 𝐷 )
2		fsumub.2	⊢ ( 𝜑 → 𝐴 ∈ Fin )
3		fsumub.3	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 = 𝐶 )
4		fsumub.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ+ )
5		fsumub.k	⊢ ( 𝜑 → 𝐾 ∈ 𝐴 )
6	4	rpred	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
7	4	rpge0d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
8	2 6 7 1 5	fsumge1	⊢ ( 𝜑 → 𝐷 ≤ Σ 𝑘 ∈ 𝐴 𝐵 )
9	8 3	breqtrd	⊢ ( 𝜑 → 𝐷 ≤ 𝐶 )