isumle

Description: Comparison of two infinite sums. (Contributed by Paul Chapman, 13-Nov-2007) (Revised by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	isumle.1	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
	isumle.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	isumle.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
	isumle.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
	isumle.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
	isumle.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
	isumle.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ≤ 𝐵 )
	isumle.8	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
	isumle.9	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ dom ⇝ )
Assertion	isumle	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 ≤ Σ 𝑘 ∈ 𝑍 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		isumle.1	⊢ 𝑍 = ( ℤ_≥ ‘ 𝑀 )
2		isumle.2	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		isumle.3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) = 𝐴 )
4		isumle.4	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
5		isumle.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) = 𝐵 )
6		isumle.6	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
7		isumle.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ≤ 𝐵 )
8		isumle.8	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ )
9		isumle.9	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ∈ dom ⇝ )
10		climdm	⊢ ( seq 𝑀 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 𝑀 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
11	8 10	sylib	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
12		climdm	⊢ ( seq 𝑀 ( + , 𝐺 ) ∈ dom ⇝ ↔ seq 𝑀 ( + , 𝐺 ) ⇝ ( ⇝ ‘ seq 𝑀 ( + , 𝐺 ) ) )
13	9 12	sylib	⊢ ( 𝜑 → seq 𝑀 ( + , 𝐺 ) ⇝ ( ⇝ ‘ seq 𝑀 ( + , 𝐺 ) ) )
14	3 4	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
15	5 6	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
16	7 3 5	3brtr4d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ≤ ( 𝐺 ‘ 𝑘 ) )
17	1 2 11 13 14 15 16	iserle	⊢ ( 𝜑 → ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) ≤ ( ⇝ ‘ seq 𝑀 ( + , 𝐺 ) ) )
18	4	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℂ )
19	1 2 3 18	isum	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 = ( ⇝ ‘ seq 𝑀 ( + , 𝐹 ) ) )
20	6	recnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐵 ∈ ℂ )
21	1 2 5 20	isum	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐵 = ( ⇝ ‘ seq 𝑀 ( + , 𝐺 ) ) )
22	17 19 21	3brtr4d	⊢ ( 𝜑 → Σ 𝑘 ∈ 𝑍 𝐴 ≤ Σ 𝑘 ∈ 𝑍 𝐵 )

Metamath Proof Explorer

Theorem isumle

Proof