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	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 < Σ 𝑘 ∈ 𝐴 𝐶 )