cvgcmpce

Description: A comparison test for convergence of a complex infinite series. (Contributed by NM, 25-Apr-2005) (Revised by Mario Carneiro, 27-May-2014)

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

Proof

Step	Hyp	Ref	Expression
1		cvgcmpce.1	$⊢ Z = ℤ_{\geq M}$
2		cvgcmpce.2	$⊢ φ \to N \in Z$
3		cvgcmpce.3	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
4		cvgcmpce.4	$⊢ (φ \land k \in Z) \to G (k) \in ℂ$
5		cvgcmpce.5	$⊢ φ \to seq M (+ F) \in dom ⇝$
6		cvgcmpce.6	$⊢ φ \to C \in ℝ$
7		cvgcmpce.7	$⊢ (φ \land k \in ℤ_{\geq N}) \to \|G (k)\| \leq C 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	serf	$⊢ φ \to seq M (+ G) : Z ⟶ ℂ$
12	11	ffvelrnda	$⊢ (φ \land n \in Z) \to seq M (+ G) (n) \in ℂ$
13		fveq2	$⊢ m = k \to F (m) = F (k)$
14	13	oveq2d	$⊢ m = k \to C F (m) = C F (k)$
15		eqid	$⊢ (m \in Z ⟼ C F (m)) = (m \in Z ⟼ C F (m))$
16		ovex	$⊢ C F (k) \in V$
17	14 15 16	fvmpt	$⊢ k \in Z \to (m \in Z ⟼ C F (m)) (k) = C F (k)$
18	17	adantl	$⊢ (φ \land k \in Z) \to (m \in Z ⟼ C F (m)) (k) = C F (k)$
19	6	adantr	$⊢ (φ \land k \in Z) \to C \in ℝ$
20	19 3	remulcld	$⊢ (φ \land k \in Z) \to C F (k) \in ℝ$
21	18 20	eqeltrd	$⊢ (φ \land k \in Z) \to (m \in Z ⟼ C F (m)) (k) \in ℝ$
22		2fveq3	$⊢ m = k \to \|G (m)\| = \|G (k)\|$
23		eqid	$⊢ (m \in Z ⟼ \|G (m)\|) = (m \in Z ⟼ \|G (m)\|)$
24		fvex	$⊢ \|G (k)\| \in V$
25	22 23 24	fvmpt	$⊢ k \in Z \to (m \in Z ⟼ \|G (m)\|) (k) = \|G (k)\|$
26	25	adantl	$⊢ (φ \land k \in Z) \to (m \in Z ⟼ \|G (m)\|) (k) = \|G (k)\|$
27	4	abscld	$⊢ (φ \land k \in Z) \to \|G (k)\| \in ℝ$
28	26 27	eqeltrd	$⊢ (φ \land k \in Z) \to (m \in Z ⟼ \|G (m)\|) (k) \in ℝ$
29	6	recnd	$⊢ φ \to C \in ℂ$
30		climdm	$⊢ seq M (+ F) \in dom ⇝ \leftrightarrow seq M (+ F) ⇝ ⇝ (seq M (+ F))$
31	5 30	sylib	$⊢ φ \to seq M (+ F) ⇝ ⇝ (seq M (+ F))$
32	3	recnd	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
33	1 10 29 31 32 18	isermulc2	$⊢ φ \to seq M (+ (m \in Z ⟼ C F (m))) ⇝ C ⇝ (seq M (+ F))$
34		climrel	$⊢ Rel ⇝$
35	34	releldmi	$⊢ seq M (+ (m \in Z ⟼ C F (m))) ⇝ C ⇝ (seq M (+ F)) \to seq M (+ (m \in Z ⟼ C F (m))) \in dom ⇝$
36	33 35	syl	$⊢ φ \to seq M (+ (m \in Z ⟼ C F (m))) \in dom ⇝$
37	1	uztrn2	$⊢ (N \in Z \land k \in ℤ_{\geq N}) \to k \in Z$
38	2 37	sylan	$⊢ (φ \land k \in ℤ_{\geq N}) \to k \in Z$
39	4	absge0d	$⊢ (φ \land k \in Z) \to 0 \leq \|G (k)\|$
40	39 26	breqtrrd	$⊢ (φ \land k \in Z) \to 0 \leq (m \in Z ⟼ \|G (m)\|) (k)$
41	38 40	syldan	$⊢ (φ \land k \in ℤ_{\geq N}) \to 0 \leq (m \in Z ⟼ \|G (m)\|) (k)$
42	38 25	syl	$⊢ (φ \land k \in ℤ_{\geq N}) \to (m \in Z ⟼ \|G (m)\|) (k) = \|G (k)\|$
43	38 17	syl	$⊢ (φ \land k \in ℤ_{\geq N}) \to (m \in Z ⟼ C F (m)) (k) = C F (k)$
44	7 42 43	3brtr4d	$⊢ (φ \land k \in ℤ_{\geq N}) \to (m \in Z ⟼ \|G (m)\|) (k) \leq (m \in Z ⟼ C F (m)) (k)$
45	1 2 21 28 36 41 44	cvgcmp	$⊢ φ \to seq M (+ (m \in Z ⟼ \|G (m)\|)) \in dom ⇝$
46	1	climcau	$⊢ (M \in ℤ \land seq M (+ (m \in Z ⟼ \|G (m)\|)) \in dom ⇝) \to \forall x \in ℝ^{+} \exists j \in Z \forall n \in ℤ_{\geq j} \|seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j)\| < x$
47	10 45 46	syl2anc	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall n \in ℤ_{\geq j} \|seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j)\| < x$
48	1 10 28	serfre	$⊢ φ \to seq M (+ (m \in Z ⟼ \|G (m)\|)) : Z ⟶ ℝ$
49	48	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to seq M (+ (m \in Z ⟼ \|G (m)\|)) : Z ⟶ ℝ$
50	1	uztrn2	$⊢ (j \in Z \land n \in ℤ_{\geq j}) \to n \in Z$
51	50	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to n \in Z$
52	49 51	ffvelrnd	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) \in ℝ$
53		simprl	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to j \in Z$
54	49 53	ffvelrnd	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to seq M (+ (m \in Z ⟼ \|G (m)\|)) (j) \in ℝ$
55	52 54	resubcld	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j) \in ℝ$
56		0red	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to 0 \in ℝ$
57	11	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to seq M (+ G) : Z ⟶ ℂ$
58	57 51	ffvelrnd	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to seq M (+ G) (n) \in ℂ$
59	57 53	ffvelrnd	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to seq M (+ G) (j) \in ℂ$
60	58 59	subcld	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to seq M (+ G) (n) - seq M (+ G) (j) \in ℂ$
61	60	abscld	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \|seq M (+ G) (n) - seq M (+ G) (j)\| \in ℝ$
62	60	absge0d	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to 0 \leq \|seq M (+ G) (n) - seq M (+ G) (j)\|$
63		fzfid	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to (M \dots n) \in Fin$
64		difss	$⊢ (M \dots n) ∖ (M \dots j) \subseteq (M \dots n)$
65		ssfi	$⊢ ((M \dots n) \in Fin \land (M \dots n) ∖ (M \dots j) \subseteq (M \dots n)) \to (M \dots n) ∖ (M \dots j) \in Fin$
66	63 64 65	sylancl	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to (M \dots n) ∖ (M \dots j) \in Fin$
67		eldifi	$⊢ k \in ((M \dots n) ∖ (M \dots j)) \to k \in (M \dots n)$
68		simpll	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to φ$
69		elfzuz	$⊢ k \in (M \dots n) \to k \in ℤ_{\geq M}$
70	69 1	eleqtrrdi	$⊢ k \in (M \dots n) \to k \in Z$
71	68 70 4	syl2an	$⊢ (((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \land k \in (M \dots n)) \to G (k) \in ℂ$
72	67 71	sylan2	$⊢ (((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \land k \in ((M \dots n) ∖ (M \dots j))) \to G (k) \in ℂ$
73	66 72	fsumabs	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \|\sum_{k \in (M \dots n) ∖ (M \dots j)} G (k)\| \leq \sum_{k \in (M \dots n) ∖ (M \dots j)} \|G (k)\|$
74		eqidd	$⊢ (((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \land k \in (M \dots n)) \to G (k) = G (k)$
75	51 1	eleqtrdi	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to n \in ℤ_{\geq M}$
76	74 75 71	fsumser	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \sum_{k = M}^{n} G (k) = seq M (+ G) (n)$
77		eqidd	$⊢ (((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \land k \in (M \dots j)) \to G (k) = G (k)$
78	53 1	eleqtrdi	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to j \in ℤ_{\geq M}$
79		elfzuz	$⊢ k \in (M \dots j) \to k \in ℤ_{\geq M}$
80	79 1	eleqtrrdi	$⊢ k \in (M \dots j) \to k \in Z$
81	68 80 4	syl2an	$⊢ (((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \land k \in (M \dots j)) \to G (k) \in ℂ$
82	77 78 81	fsumser	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \sum_{k = M}^{j} G (k) = seq M (+ G) (j)$
83	76 82	oveq12d	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \sum_{k = M}^{n} G (k) - \sum_{k = M}^{j} G (k) = seq M (+ G) (n) - seq M (+ G) (j)$
84		fzfid	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to (M \dots j) \in Fin$
85	84 81	fsumcl	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \sum_{k = M}^{j} G (k) \in ℂ$
86	66 72	fsumcl	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \sum_{k \in (M \dots n) ∖ (M \dots j)} G (k) \in ℂ$
87		disjdif	$⊢ (M \dots j) \cap ((M \dots n) ∖ (M \dots j)) = \emptyset$
88	87	a1i	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to (M \dots j) \cap ((M \dots n) ∖ (M \dots j)) = \emptyset$
89		undif2	$⊢ (M \dots j) \cup ((M \dots n) ∖ (M \dots j)) = (M \dots j) \cup (M \dots n)$
90		fzss2	$⊢ n \in ℤ_{\geq j} \to (M \dots j) \subseteq (M \dots n)$
91	90	ad2antll	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to (M \dots j) \subseteq (M \dots n)$
92		ssequn1	$⊢ (M \dots j) \subseteq (M \dots n) \leftrightarrow (M \dots j) \cup (M \dots n) = (M \dots n)$
93	91 92	sylib	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to (M \dots j) \cup (M \dots n) = (M \dots n)$
94	89 93	syl5req	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to (M \dots n) = (M \dots j) \cup ((M \dots n) ∖ (M \dots j))$
95	88 94 63 71	fsumsplit	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \sum_{k = M}^{n} G (k) = \sum_{k = M}^{j} G (k) + \sum_{k \in (M \dots n) ∖ (M \dots j)} G (k)$
96	85 86 95	mvrladdd	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \sum_{k = M}^{n} G (k) - \sum_{k = M}^{j} G (k) = \sum_{k \in (M \dots n) ∖ (M \dots j)} G (k)$
97	83 96	eqtr3d	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to seq M (+ G) (n) - seq M (+ G) (j) = \sum_{k \in (M \dots n) ∖ (M \dots j)} G (k)$
98	97	fveq2d	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \|seq M (+ G) (n) - seq M (+ G) (j)\| = \|\sum_{k \in (M \dots n) ∖ (M \dots j)} G (k)\|$
99	70	adantl	$⊢ (((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \land k \in (M \dots n)) \to k \in Z$
100	99 25	syl	$⊢ (((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \land k \in (M \dots n)) \to (m \in Z ⟼ \|G (m)\|) (k) = \|G (k)\|$
101		abscl	$⊢ G (k) \in ℂ \to \|G (k)\| \in ℝ$
102	101	recnd	$⊢ G (k) \in ℂ \to \|G (k)\| \in ℂ$
103	71 102	syl	$⊢ (((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \land k \in (M \dots n)) \to \|G (k)\| \in ℂ$
104	100 75 103	fsumser	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \sum_{k = M}^{n} \|G (k)\| = seq M (+ (m \in Z ⟼ \|G (m)\|)) (n)$
105	80	adantl	$⊢ (((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \land k \in (M \dots j)) \to k \in Z$
106	105 25	syl	$⊢ (((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \land k \in (M \dots j)) \to (m \in Z ⟼ \|G (m)\|) (k) = \|G (k)\|$
107	81 102	syl	$⊢ (((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \land k \in (M \dots j)) \to \|G (k)\| \in ℂ$
108	106 78 107	fsumser	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \sum_{k = M}^{j} \|G (k)\| = seq M (+ (m \in Z ⟼ \|G (m)\|)) (j)$
109	104 108	oveq12d	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \sum_{k = M}^{n} \|G (k)\| - \sum_{k = M}^{j} \|G (k)\| = seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j)$
110	84 107	fsumcl	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \sum_{k = M}^{j} \|G (k)\| \in ℂ$
111	72 102	syl	$⊢ (((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \land k \in ((M \dots n) ∖ (M \dots j))) \to \|G (k)\| \in ℂ$
112	66 111	fsumcl	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \sum_{k \in (M \dots n) ∖ (M \dots j)} \|G (k)\| \in ℂ$
113	88 94 63 103	fsumsplit	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \sum_{k = M}^{n} \|G (k)\| = \sum_{k = M}^{j} \|G (k)\| + \sum_{k \in (M \dots n) ∖ (M \dots j)} \|G (k)\|$
114	110 112 113	mvrladdd	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \sum_{k = M}^{n} \|G (k)\| - \sum_{k = M}^{j} \|G (k)\| = \sum_{k \in (M \dots n) ∖ (M \dots j)} \|G (k)\|$
115	109 114	eqtr3d	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j) = \sum_{k \in (M \dots n) ∖ (M \dots j)} \|G (k)\|$
116	73 98 115	3brtr4d	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \|seq M (+ G) (n) - seq M (+ G) (j)\| \leq seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j)$
117	56 61 55 62 116	letrd	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to 0 \leq seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j)$
118	55 117	absidd	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to \|seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j)\| = seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j)$
119	118	breq1d	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to (\|seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j)\| < x \leftrightarrow seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j) < x)$
120		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
121	120	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to x \in ℝ$
122		lelttr	$⊢ (\|seq M (+ G) (n) - seq M (+ G) (j)\| \in ℝ \land seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j) \in ℝ \land x \in ℝ) \to ((\|seq M (+ G) (n) - seq M (+ G) (j)\| \leq seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j) \land seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j) < x) \to \|seq M (+ G) (n) - seq M (+ G) (j)\| < x)$
123	61 55 121 122	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to ((\|seq M (+ G) (n) - seq M (+ G) (j)\| \leq seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j) \land seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j) < x) \to \|seq M (+ G) (n) - seq M (+ G) (j)\| < x)$
124	116 123	mpand	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to (seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j) < x \to \|seq M (+ G) (n) - seq M (+ G) (j)\| < x)$
125	119 124	sylbid	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land n \in ℤ_{\geq j})) \to (\|seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j)\| < x \to \|seq M (+ G) (n) - seq M (+ G) (j)\| < x)$
126	125	anassrs	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land n \in ℤ_{\geq j}) \to (\|seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j)\| < x \to \|seq M (+ G) (n) - seq M (+ G) (j)\| < x)$
127	126	ralimdva	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to (\forall n \in ℤ_{\geq j} \|seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j)\| < x \to \forall n \in ℤ_{\geq j} \|seq M (+ G) (n) - seq M (+ G) (j)\| < x)$
128	127	reximdva	$⊢ (φ \land x \in ℝ^{+}) \to (\exists j \in Z \forall n \in ℤ_{\geq j} \|seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j)\| < x \to \exists j \in Z \forall n \in ℤ_{\geq j} \|seq M (+ G) (n) - seq M (+ G) (j)\| < x)$
129	128	ralimdva	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall n \in ℤ_{\geq j} \|seq M (+ (m \in Z ⟼ \|G (m)\|)) (n) - seq M (+ (m \in Z ⟼ \|G (m)\|)) (j)\| < x \to \forall x \in ℝ^{+} \exists j \in Z \forall n \in ℤ_{\geq j} \|seq M (+ G) (n) - seq M (+ G) (j)\| < x)$
130	47 129	mpd	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall n \in ℤ_{\geq j} \|seq M (+ G) (n) - seq M (+ G) (j)\| < x$
131		seqex	$⊢ seq M (+ G) \in V$
132	131	a1i	$⊢ φ \to seq M (+ G) \in V$
133	1 12 130 132	caucvg	$⊢ φ \to seq M (+ G) \in dom ⇝$

Metamath Proof Explorer

Theorem cvgcmpce

Proof