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

Metamath Proof Explorer

Theorem fsumlessf

Description: A shorter sum of nonnegative terms is smaller than a longer one. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses fsumlessf.k ⊢ Ⅎ k φ
fsumge0.a ⊢ φ → A ∈ Fin
fsumge0.b ⊢ φ ∧ k ∈ A → B ∈ ℝ
fsumge0.l ⊢ φ ∧ k ∈ A → 0 ≤ B
fsumless.c ⊢ φ → C ⊆ A
Assertion fsumlessf ⊢ φ → ∑ k ∈ C B ≤ ∑ k ∈ A B

Proof

Step Hyp Ref Expression
1 fsumlessf.k ⊢ Ⅎ k φ
2 fsumge0.a ⊢ φ → A ∈ Fin
3 fsumge0.b ⊢ φ ∧ k ∈ A → B ∈ ℝ
4 fsumge0.l ⊢ φ ∧ k ∈ A → 0 ≤ B
5 fsumless.c ⊢ φ → C ⊆ A
6 nfv ⊢ Ⅎ k j ∈ A
7 1 6 nfan ⊢ Ⅎ k φ ∧ j ∈ A
8 nfcsb1v ⊢ Ⅎ _ k ⦋ j / k⦌ B
9 8 nfel1 ⊢ Ⅎ k ⦋ j / k⦌ B ∈ ℝ
10 7 9 nfim ⊢ Ⅎ k φ ∧ j ∈ A → ⦋ j / k⦌ B ∈ ℝ
11 eleq1w ⊢ k = j → k ∈ A ↔ j ∈ A
12 11 anbi2d ⊢ k = j → φ ∧ k ∈ A ↔ φ ∧ j ∈ A
13 csbeq1a ⊢ k = j → B = ⦋ j / k⦌ B
14 13 eleq1d ⊢ k = j → B ∈ ℝ ↔ ⦋ j / k⦌ B ∈ ℝ
15 12 14 imbi12d ⊢ k = j → φ ∧ k ∈ A → B ∈ ℝ ↔ φ ∧ j ∈ A → ⦋ j / k⦌ B ∈ ℝ
16 10 15 3 chvarfv ⊢ φ ∧ j ∈ A → ⦋ j / k⦌ B ∈ ℝ
17 nfcv ⊢ Ⅎ _ k 0
18 nfcv ⊢ Ⅎ _ k ≤
19 17 18 8 nfbr ⊢ Ⅎ k 0 ≤ ⦋ j / k⦌ B
20 7 19 nfim ⊢ Ⅎ k φ ∧ j ∈ A → 0 ≤ ⦋ j / k⦌ B
21 13 breq2d ⊢ k = j → 0 ≤ B ↔ 0 ≤ ⦋ j / k⦌ B
22 12 21 imbi12d ⊢ k = j → φ ∧ k ∈ A → 0 ≤ B ↔ φ ∧ j ∈ A → 0 ≤ ⦋ j / k⦌ B
23 20 22 4 chvarfv ⊢ φ ∧ j ∈ A → 0 ≤ ⦋ j / k⦌ B
24 2 16 23 5 fsumless ⊢ φ → ∑ j ∈ C ⦋ j / k⦌ B ≤ ∑ j ∈ A ⦋ j / k⦌ B
25 nfcv ⊢ Ⅎ _ j B
26 13 25 8 cbvsum ⊢ ∑ k ∈ C B = ∑ j ∈ C ⦋ j / k⦌ B
27 13 25 8 cbvsum ⊢ ∑ k ∈ A B = ∑ j ∈ A ⦋ j / k⦌ B
28 26 27 breq12i ⊢ ∑ k ∈ C B ≤ ∑ k ∈ A B ↔ ∑ j ∈ C ⦋ j / k⦌ B ≤ ∑ j ∈ A ⦋ j / k⦌ B
29 24 28 sylibr ⊢ φ → ∑ k ∈ C B ≤ ∑ k ∈ A B