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

Metamath Proof Explorer

Theorem fsumle

Description: If all of the terms of finite sums compare, so do the sums. (Contributed by NM, 11-Dec-2005) (Proof shortened by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsumle.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsumle.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
fsumle.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
fsumle.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
Assertion fsumle ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ≤ Σ 𝑘 ∈ 𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 fsumle.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 fsumle.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
3 fsumle.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
4 fsumle.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ≤ 𝐶 )
5 3 2 resubcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
6 3 2 subge0d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 0 ≤ ( 𝐶 − 𝐵 ) ↔ 𝐵 ≤ 𝐶 ) )
7 4 6 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ ( 𝐶 − 𝐵 ) )
8 1 5 7 fsumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑘 ∈ 𝐴 ( 𝐶 − 𝐵 ) )
9 3 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
10 2 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
11 1 9 10 fsumsub ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 𝐶 − 𝐵 ) = ( Σ 𝑘 ∈ 𝐴 𝐶 − Σ 𝑘 ∈ 𝐴 𝐵 ) )
12 8 11 breqtrd ⊢ ( 𝜑 → 0 ≤ ( Σ 𝑘 ∈ 𝐴 𝐶 − Σ 𝑘 ∈ 𝐴 𝐵 ) )
13 1 3 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐶 ∈ ℝ )
14 1 2 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )
15 13 14 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( Σ 𝑘 ∈ 𝐴 𝐶 − Σ 𝑘 ∈ 𝐴 𝐵 ) ↔ Σ 𝑘 ∈ 𝐴 𝐵 ≤ Σ 𝑘 ∈ 𝐴 𝐶 ) )
16 12 15 mpbid ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ≤ Σ 𝑘 ∈ 𝐴 𝐶 )