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

Metamath Proof Explorer

Theorem fsumlt

Description: If every term in one finite sum is less than the corresponding term in another, then the first sum is less than the second. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 3-Jun-2014)

Ref Expression
Hypotheses fsumlt.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsumlt.2 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
fsumlt.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
fsumlt.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
fsumlt.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 < 𝐶 )
Assertion fsumlt ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 < Σ 𝑘 ∈ 𝐴 𝐶 )

Proof

Step Hyp Ref Expression
1 fsumlt.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 fsumlt.2 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
3 fsumlt.3 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4 fsumlt.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℝ )
5 fsumlt.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 < 𝐶 )
6 difrp ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 < 𝐶 ↔ ( 𝐶 − 𝐵 ) ∈ ℝ+ ) )
7 3 4 6 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐵 < 𝐶 ↔ ( 𝐶 − 𝐵 ) ∈ ℝ+ ) )
8 5 7 mpbid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐶 − 𝐵 ) ∈ ℝ+ )
9 1 2 8 fsumrpcl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 𝐶 − 𝐵 ) ∈ ℝ+ )
10 9 rpgt0d ⊢ ( 𝜑 → 0 < Σ 𝑘 ∈ 𝐴 ( 𝐶 − 𝐵 ) )
11 4 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
12 3 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
13 1 11 12 fsumsub ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 ( 𝐶 − 𝐵 ) = ( Σ 𝑘 ∈ 𝐴 𝐶 − Σ 𝑘 ∈ 𝐴 𝐵 ) )
14 10 13 breqtrd ⊢ ( 𝜑 → 0 < ( Σ 𝑘 ∈ 𝐴 𝐶 − Σ 𝑘 ∈ 𝐴 𝐵 ) )
15 1 3 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )
16 1 4 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐶 ∈ ℝ )
17 15 16 posdifd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ 𝐴 𝐵 < Σ 𝑘 ∈ 𝐴 𝐶 ↔ 0 < ( Σ 𝑘 ∈ 𝐴 𝐶 − Σ 𝑘 ∈ 𝐴 𝐵 ) ) )
18 14 17 mpbird ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 < Σ 𝑘 ∈ 𝐴 𝐶 )