iserle

Description: Comparison of the limits of two infinite series. (Contributed by Paul Chapman, 12-Nov-2007) (Revised by Mario Carneiro, 3-Feb-2014)

Step	Hyp	Ref	Expression
1		clim2ser.1	$⊢ Z = ℤ_{\geq M}$
2		iserle.2	$⊢ φ \to M \in ℤ$
3		iserle.4	$⊢ φ \to seq M (+ F) ⇝ A$
4		iserle.5	$⊢ φ \to seq M (+ G) ⇝ B$
5		iserle.6	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
6		iserle.7	$⊢ (φ \land k \in Z) \to G (k) \in ℝ$
7		iserle.8	$⊢ (φ \land k \in Z) \to F (k) \leq G (k)$
8	1 2 5	serfre	$⊢ φ \to seq M (+ F) : Z ⟶ ℝ$
9	8	ffvelcdmda	$⊢ (φ \land j \in Z) \to seq M (+ F) (j) \in ℝ$
10	1 2 6	serfre	$⊢ φ \to seq M (+ G) : Z ⟶ ℝ$
11	10	ffvelcdmda	$⊢ (φ \land j \in Z) \to seq M (+ G) (j) \in ℝ$
12		simpr	$⊢ (φ \land j \in Z) \to j \in Z$
13	12 1	eleqtrdi	$⊢ (φ \land j \in Z) \to j \in ℤ_{\geq M}$
14		simpll	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to φ$
15		elfzuz	$⊢ k \in (M \dots j) \to k \in ℤ_{\geq M}$
16	15 1	eleqtrrdi	$⊢ k \in (M \dots j) \to k \in Z$
17	16	adantl	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to k \in Z$
18	14 17 5	syl2anc	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to F (k) \in ℝ$
19	14 17 6	syl2anc	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to G (k) \in ℝ$
20	14 17 7	syl2anc	$⊢ ((φ \land j \in Z) \land k \in (M \dots j)) \to F (k) \leq G (k)$
21	13 18 19 20	serle	$⊢ (φ \land j \in Z) \to seq M (+ F) (j) \leq seq M (+ G) (j)$
22	1 2 3 4 9 11 21	climle	$⊢ φ \to A \leq B$

Metamath Proof Explorer