cvgcmpub

Description: An upper bound for the limit of a real infinite series. This theorem can also be used to compare two infinite series. (Contributed by Mario Carneiro, 24-Mar-2014)

	Ref	Expression
Hypotheses	cvgcmp.1	$⊢ Z = ℤ_{\geq M}$
	cvgcmp.2	$⊢ φ \to N \in Z$
	cvgcmp.3	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
	cvgcmp.4	$⊢ (φ \land k \in Z) \to G (k) \in ℝ$
	cvgcmpub.5	$⊢ φ \to seq M (+ F) ⇝ A$
	cvgcmpub.6	$⊢ φ \to seq M (+ G) ⇝ B$
	cvgcmpub.7	$⊢ (φ \land k \in Z) \to G (k) \leq F (k)$
Assertion	cvgcmpub	$⊢ φ \to B \leq A$

Proof

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

Metamath Proof Explorer

Theorem cvgcmpub

Proof