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 ⊢ k = K → B = D
fsumub.2 ⊢ φ → A ∈ Fin
fsumub.3 ⊢ φ → ∑ k ∈ A B = C
fsumub.4 ⊢ φ ∧ k ∈ A → B ∈ ℝ +
fsumub.k ⊢ φ → K ∈ A
Assertion fsumub ⊢ φ → D ≤ C

Proof

Step Hyp Ref Expression
1 fsumub.1 ⊢ k = K → B = D
2 fsumub.2 ⊢ φ → A ∈ Fin
3 fsumub.3 ⊢ φ → ∑ k ∈ A B = C
4 fsumub.4 ⊢ φ ∧ k ∈ A → B ∈ ℝ +
5 fsumub.k ⊢ φ → K ∈ A
6 4 rpred ⊢ φ ∧ k ∈ A → B ∈ ℝ
7 4 rpge0d ⊢ φ ∧ k ∈ A → 0 ≤ B
8 2 6 7 1 5 fsumge1 ⊢ φ → D ≤ ∑ k ∈ A B
9 8 3 breqtrd ⊢ φ → D ≤ C