This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → 𝐷 ≤ 𝐶 )