cvgcmp

Description: A comparison test for convergence of a real infinite series. Exercise 3 of Gleason p. 182. (Contributed by NM, 1-May-2005) (Revised 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 ℝ$
	cvgcmp.5	$⊢ φ \to seq M (+ F) \in dom ⇝$
	cvgcmp.6	$⊢ (φ \land k \in ℤ_{\geq N}) \to 0 \leq G (k)$
	cvgcmp.7	$⊢ (φ \land k \in ℤ_{\geq N}) \to G (k) \leq F (k)$
Assertion	cvgcmp	$⊢ φ \to seq M (+ G) \in dom ⇝$

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		cvgcmp.5	$⊢ φ \to seq M (+ F) \in dom ⇝$
6		cvgcmp.6	$⊢ (φ \land k \in ℤ_{\geq N}) \to 0 \leq G (k)$
7		cvgcmp.7	$⊢ (φ \land k \in ℤ_{\geq N}) \to G (k) \leq F (k)$
8		seqex	$⊢ seq M (+ G) \in V$
9	8	a1i	$⊢ φ \to seq M (+ G) \in V$
10	2 1	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
11		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
12	10 11	syl	$⊢ φ \to M \in ℤ$
13	1	climcau	$⊢ (M \in ℤ \land seq M (+ F) \in dom ⇝) \to \forall x \in ℝ^{+} \exists m \in Z \forall n \in ℤ_{\geq m} \|seq M (+ F) (n) - seq M (+ F) (m)\| < x$
14	12 5 13	syl2anc	$⊢ φ \to \forall x \in ℝ^{+} \exists m \in Z \forall n \in ℤ_{\geq m} \|seq M (+ F) (n) - seq M (+ F) (m)\| < x$
15	1 12 3	serfre	$⊢ φ \to seq M (+ F) : Z ⟶ ℝ$
16	15	ffvelcdmda	$⊢ (φ \land n \in Z) \to seq M (+ F) (n) \in ℝ$
17	16	recnd	$⊢ (φ \land n \in Z) \to seq M (+ F) (n) \in ℂ$
18	17	ralrimiva	$⊢ φ \to \forall n \in Z seq M (+ F) (n) \in ℂ$
19	1	r19.29uz	$⊢ (\forall n \in Z seq M (+ F) (n) \in ℂ \land \exists m \in Z \forall n \in ℤ_{\geq m} \|seq M (+ F) (n) - seq M (+ F) (m)\| < x) \to \exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ F) (n) \in ℂ \land \|seq M (+ F) (n) - seq M (+ F) (m)\| < x)$
20	19	ex	$⊢ \forall n \in Z seq M (+ F) (n) \in ℂ \to (\exists m \in Z \forall n \in ℤ_{\geq m} \|seq M (+ F) (n) - seq M (+ F) (m)\| < x \to \exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ F) (n) \in ℂ \land \|seq M (+ F) (n) - seq M (+ F) (m)\| < x))$
21	18 20	syl	$⊢ φ \to (\exists m \in Z \forall n \in ℤ_{\geq m} \|seq M (+ F) (n) - seq M (+ F) (m)\| < x \to \exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ F) (n) \in ℂ \land \|seq M (+ F) (n) - seq M (+ F) (m)\| < x))$
22	21	ralimdv	$⊢ φ \to (\forall x \in ℝ^{+} \exists m \in Z \forall n \in ℤ_{\geq m} \|seq M (+ F) (n) - seq M (+ F) (m)\| < x \to \forall x \in ℝ^{+} \exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ F) (n) \in ℂ \land \|seq M (+ F) (n) - seq M (+ F) (m)\| < x))$
23	14 22	mpd	$⊢ φ \to \forall x \in ℝ^{+} \exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ F) (n) \in ℂ \land \|seq M (+ F) (n) - seq M (+ F) (m)\| < x)$
24	1	uztrn2	$⊢ (N \in Z \land n \in ℤ_{\geq N}) \to n \in Z$
25	2 24	sylan	$⊢ (φ \land n \in ℤ_{\geq N}) \to n \in Z$
26	1 12 4	serfre	$⊢ φ \to seq M (+ G) : Z ⟶ ℝ$
27	26	ffvelcdmda	$⊢ (φ \land n \in Z) \to seq M (+ G) (n) \in ℝ$
28	27	recnd	$⊢ (φ \land n \in Z) \to seq M (+ G) (n) \in ℂ$
29	25 28	syldan	$⊢ (φ \land n \in ℤ_{\geq N}) \to seq M (+ G) (n) \in ℂ$
30	29	ralrimiva	$⊢ φ \to \forall n \in ℤ_{\geq N} seq M (+ G) (n) \in ℂ$
31	30	adantr	$⊢ (φ \land x \in ℝ^{+}) \to \forall n \in ℤ_{\geq N} seq M (+ G) (n) \in ℂ$
32		simpll	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to φ$
33	32 15	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ F) : Z ⟶ ℝ$
34	32 2	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to N \in Z$
35		simprl	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to m \in ℤ_{\geq N}$
36	1	uztrn2	$⊢ (N \in Z \land m \in ℤ_{\geq N}) \to m \in Z$
37	34 35 36	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to m \in Z$
38	33 37	ffvelcdmd	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ F) (m) \in ℝ$
39		eqid	$⊢ ℤ_{\geq N} = ℤ_{\geq N}$
40	39	uztrn2	$⊢ (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m}) \to n \in ℤ_{\geq N}$
41	40	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to n \in ℤ_{\geq N}$
42	34 41 24	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to n \in Z$
43	32 42 16	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ F) (n) \in ℝ$
44	32 42 27	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ G) (n) \in ℝ$
45	32 26	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ G) : Z ⟶ ℝ$
46	45 37	ffvelcdmd	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ G) (m) \in ℝ$
47	44 46	resubcld	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ G) (n) - seq M (+ G) (m) \in ℝ$
48	37 1	eleqtrdi	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to m \in ℤ_{\geq M}$
49		simprr	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to n \in ℤ_{\geq m}$
50		elfzuz	$⊢ k \in (M \dots n) \to k \in ℤ_{\geq M}$
51	50 1	eleqtrrdi	$⊢ k \in (M \dots n) \to k \in Z$
52		fveq2	$⊢ m = k \to F (m) = F (k)$
53		fveq2	$⊢ m = k \to G (m) = G (k)$
54	52 53	oveq12d	$⊢ m = k \to F (m) - G (m) = F (k) - G (k)$
55		eqid	$⊢ (m \in Z ⟼ F (m) - G (m)) = (m \in Z ⟼ F (m) - G (m))$
56		ovex	$⊢ F (k) - G (k) \in V$
57	54 55 56	fvmpt	$⊢ k \in Z \to (m \in Z ⟼ F (m) - G (m)) (k) = F (k) - G (k)$
58	57	adantl	$⊢ (φ \land k \in Z) \to (m \in Z ⟼ F (m) - G (m)) (k) = F (k) - G (k)$
59	3 4	resubcld	$⊢ (φ \land k \in Z) \to F (k) - G (k) \in ℝ$
60	58 59	eqeltrd	$⊢ (φ \land k \in Z) \to (m \in Z ⟼ F (m) - G (m)) (k) \in ℝ$
61	32 51 60	syl2an	$⊢ (((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \land k \in (M \dots n)) \to (m \in Z ⟼ F (m) - G (m)) (k) \in ℝ$
62		elfzuz	$⊢ k \in (m + 1 \dots n) \to k \in ℤ_{\geq (m + 1)}$
63		peano2uz	$⊢ m \in ℤ_{\geq N} \to m + 1 \in ℤ_{\geq N}$
64	35 63	syl	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to m + 1 \in ℤ_{\geq N}$
65	39	uztrn2	$⊢ (m + 1 \in ℤ_{\geq N} \land k \in ℤ_{\geq (m + 1)}) \to k \in ℤ_{\geq N}$
66	64 65	sylan	$⊢ (((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \land k \in ℤ_{\geq (m + 1)}) \to k \in ℤ_{\geq N}$
67	1	uztrn2	$⊢ (N \in Z \land k \in ℤ_{\geq N}) \to k \in Z$
68	2 67	sylan	$⊢ (φ \land k \in ℤ_{\geq N}) \to k \in Z$
69	3 4	subge0d	$⊢ (φ \land k \in Z) \to (0 \leq F (k) - G (k) \leftrightarrow G (k) \leq F (k))$
70	68 69	syldan	$⊢ (φ \land k \in ℤ_{\geq N}) \to (0 \leq F (k) - G (k) \leftrightarrow G (k) \leq F (k))$
71	7 70	mpbird	$⊢ (φ \land k \in ℤ_{\geq N}) \to 0 \leq F (k) - G (k)$
72	68 57	syl	$⊢ (φ \land k \in ℤ_{\geq N}) \to (m \in Z ⟼ F (m) - G (m)) (k) = F (k) - G (k)$
73	71 72	breqtrrd	$⊢ (φ \land k \in ℤ_{\geq N}) \to 0 \leq (m \in Z ⟼ F (m) - G (m)) (k)$
74	32 66 73	syl2an2r	$⊢ (((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \land k \in ℤ_{\geq (m + 1)}) \to 0 \leq (m \in Z ⟼ F (m) - G (m)) (k)$
75	62 74	sylan2	$⊢ (((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \land k \in (m + 1 \dots n)) \to 0 \leq (m \in Z ⟼ F (m) - G (m)) (k)$
76	48 49 61 75	sermono	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ (m \in Z ⟼ F (m) - G (m))) (m) \leq seq M (+ (m \in Z ⟼ F (m) - G (m))) (n)$
77		elfzuz	$⊢ k \in (M \dots m) \to k \in ℤ_{\geq M}$
78	77 1	eleqtrrdi	$⊢ k \in (M \dots m) \to k \in Z$
79	3	recnd	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
80	32 78 79	syl2an	$⊢ (((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \land k \in (M \dots m)) \to F (k) \in ℂ$
81	4	recnd	$⊢ (φ \land k \in Z) \to G (k) \in ℂ$
82	32 78 81	syl2an	$⊢ (((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \land k \in (M \dots m)) \to G (k) \in ℂ$
83	32 78 58	syl2an	$⊢ (((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \land k \in (M \dots m)) \to (m \in Z ⟼ F (m) - G (m)) (k) = F (k) - G (k)$
84	48 80 82 83	sersub	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ (m \in Z ⟼ F (m) - G (m))) (m) = seq M (+ F) (m) - seq M (+ G) (m)$
85	42 1	eleqtrdi	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to n \in ℤ_{\geq M}$
86	32 51 79	syl2an	$⊢ (((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \land k \in (M \dots n)) \to F (k) \in ℂ$
87	32 51 81	syl2an	$⊢ (((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \land k \in (M \dots n)) \to G (k) \in ℂ$
88	32 51 58	syl2an	$⊢ (((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \land k \in (M \dots n)) \to (m \in Z ⟼ F (m) - G (m)) (k) = F (k) - G (k)$
89	85 86 87 88	sersub	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ (m \in Z ⟼ F (m) - G (m))) (n) = seq M (+ F) (n) - seq M (+ G) (n)$
90	76 84 89	3brtr3d	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ F) (m) - seq M (+ G) (m) \leq seq M (+ F) (n) - seq M (+ G) (n)$
91	43 44	resubcld	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ F) (n) - seq M (+ G) (n) \in ℝ$
92	38 46 91	lesubaddd	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to (seq M (+ F) (m) - seq M (+ G) (m) \leq seq M (+ F) (n) - seq M (+ G) (n) \leftrightarrow seq M (+ F) (m) \leq seq M (+ F) (n) - seq M (+ G) (n) + seq M (+ G) (m))$
93	90 92	mpbid	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ F) (m) \leq seq M (+ F) (n) - seq M (+ G) (n) + seq M (+ G) (m)$
94	43	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ F) (n) \in ℂ$
95	44	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ G) (n) \in ℂ$
96	46	recnd	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ G) (m) \in ℂ$
97	94 95 96	subsubd	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ F) (n) - (seq M (+ G) (n) - seq M (+ G) (m)) = seq M (+ F) (n) - seq M (+ G) (n) + seq M (+ G) (m)$
98	93 97	breqtrrd	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ F) (m) \leq seq M (+ F) (n) - (seq M (+ G) (n) - seq M (+ G) (m))$
99	38 43 47 98	lesubd	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ G) (n) - seq M (+ G) (m) \leq seq M (+ F) (n) - seq M (+ F) (m)$
100	43 38	resubcld	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ F) (n) - seq M (+ F) (m) \in ℝ$
101		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
102	101	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to x \in ℝ$
103		lelttr	$⊢ (seq M (+ G) (n) - seq M (+ G) (m) \in ℝ \land seq M (+ F) (n) - seq M (+ F) (m) \in ℝ \land x \in ℝ) \to ((seq M (+ G) (n) - seq M (+ G) (m) \leq seq M (+ F) (n) - seq M (+ F) (m) \land seq M (+ F) (n) - seq M (+ F) (m) < x) \to seq M (+ G) (n) - seq M (+ G) (m) < x)$
104	47 100 102 103	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to ((seq M (+ G) (n) - seq M (+ G) (m) \leq seq M (+ F) (n) - seq M (+ F) (m) \land seq M (+ F) (n) - seq M (+ F) (m) < x) \to seq M (+ G) (n) - seq M (+ G) (m) < x)$
105	99 104	mpand	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to (seq M (+ F) (n) - seq M (+ F) (m) < x \to seq M (+ G) (n) - seq M (+ G) (m) < x)$
106	32 51 3	syl2an	$⊢ (((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \land k \in (M \dots n)) \to F (k) \in ℝ$
107	62 66	sylan2	$⊢ (((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \land k \in (m + 1 \dots n)) \to k \in ℤ_{\geq N}$
108		0red	$⊢ (φ \land k \in ℤ_{\geq N}) \to 0 \in ℝ$
109	68 4	syldan	$⊢ (φ \land k \in ℤ_{\geq N}) \to G (k) \in ℝ$
110	68 3	syldan	$⊢ (φ \land k \in ℤ_{\geq N}) \to F (k) \in ℝ$
111	108 109 110 6 7	letrd	$⊢ (φ \land k \in ℤ_{\geq N}) \to 0 \leq F (k)$
112	32 107 111	syl2an2r	$⊢ (((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \land k \in (m + 1 \dots n)) \to 0 \leq F (k)$
113	48 49 106 112	sermono	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ F) (m) \leq seq M (+ F) (n)$
114	38 43 113	abssubge0d	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to \|seq M (+ F) (n) - seq M (+ F) (m)\| = seq M (+ F) (n) - seq M (+ F) (m)$
115	114	breq1d	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to (\|seq M (+ F) (n) - seq M (+ F) (m)\| < x \leftrightarrow seq M (+ F) (n) - seq M (+ F) (m) < x)$
116	32 51 4	syl2an	$⊢ (((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \land k \in (M \dots n)) \to G (k) \in ℝ$
117	32 66 6	syl2an2r	$⊢ (((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \land k \in ℤ_{\geq (m + 1)}) \to 0 \leq G (k)$
118	62 117	sylan2	$⊢ (((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \land k \in (m + 1 \dots n)) \to 0 \leq G (k)$
119	48 49 116 118	sermono	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to seq M (+ G) (m) \leq seq M (+ G) (n)$
120	46 44 119	abssubge0d	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to \|seq M (+ G) (n) - seq M (+ G) (m)\| = seq M (+ G) (n) - seq M (+ G) (m)$
121	120	breq1d	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to (\|seq M (+ G) (n) - seq M (+ G) (m)\| < x \leftrightarrow seq M (+ G) (n) - seq M (+ G) (m) < x)$
122	105 115 121	3imtr4d	$⊢ ((φ \land x \in ℝ^{+}) \land (m \in ℤ_{\geq N} \land n \in ℤ_{\geq m})) \to (\|seq M (+ F) (n) - seq M (+ F) (m)\| < x \to \|seq M (+ G) (n) - seq M (+ G) (m)\| < x)$
123	122	anassrs	$⊢ (((φ \land x \in ℝ^{+}) \land m \in ℤ_{\geq N}) \land n \in ℤ_{\geq m}) \to (\|seq M (+ F) (n) - seq M (+ F) (m)\| < x \to \|seq M (+ G) (n) - seq M (+ G) (m)\| < x)$
124	123	adantld	$⊢ (((φ \land x \in ℝ^{+}) \land m \in ℤ_{\geq N}) \land n \in ℤ_{\geq m}) \to ((seq M (+ F) (n) \in ℂ \land \|seq M (+ F) (n) - seq M (+ F) (m)\| < x) \to \|seq M (+ G) (n) - seq M (+ G) (m)\| < x)$
125	124	ralimdva	$⊢ ((φ \land x \in ℝ^{+}) \land m \in ℤ_{\geq N}) \to (\forall n \in ℤ_{\geq m} (seq M (+ F) (n) \in ℂ \land \|seq M (+ F) (n) - seq M (+ F) (m)\| < x) \to \forall n \in ℤ_{\geq m} \|seq M (+ G) (n) - seq M (+ G) (m)\| < x)$
126	125	reximdva	$⊢ (φ \land x \in ℝ^{+}) \to (\exists m \in ℤ_{\geq N} \forall n \in ℤ_{\geq m} (seq M (+ F) (n) \in ℂ \land \|seq M (+ F) (n) - seq M (+ F) (m)\| < x) \to \exists m \in ℤ_{\geq N} \forall n \in ℤ_{\geq m} \|seq M (+ G) (n) - seq M (+ G) (m)\| < x)$
127	39	r19.29uz	$⊢ (\forall n \in ℤ_{\geq N} seq M (+ G) (n) \in ℂ \land \exists m \in ℤ_{\geq N} \forall n \in ℤ_{\geq m} \|seq M (+ G) (n) - seq M (+ G) (m)\| < x) \to \exists m \in ℤ_{\geq N} \forall n \in ℤ_{\geq m} (seq M (+ G) (n) \in ℂ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x)$
128	31 126 127	syl6an	$⊢ (φ \land x \in ℝ^{+}) \to (\exists m \in ℤ_{\geq N} \forall n \in ℤ_{\geq m} (seq M (+ F) (n) \in ℂ \land \|seq M (+ F) (n) - seq M (+ F) (m)\| < x) \to \exists m \in ℤ_{\geq N} \forall n \in ℤ_{\geq m} (seq M (+ G) (n) \in ℂ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x))$
129	128	ralimdva	$⊢ φ \to (\forall x \in ℝ^{+} \exists m \in ℤ_{\geq N} \forall n \in ℤ_{\geq m} (seq M (+ F) (n) \in ℂ \land \|seq M (+ F) (n) - seq M (+ F) (m)\| < x) \to \forall x \in ℝ^{+} \exists m \in ℤ_{\geq N} \forall n \in ℤ_{\geq m} (seq M (+ G) (n) \in ℂ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x))$
130	1 39	cau4	$⊢ N \in Z \to (\forall x \in ℝ^{+} \exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ F) (n) \in ℂ \land \|seq M (+ F) (n) - seq M (+ F) (m)\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists m \in ℤ_{\geq N} \forall n \in ℤ_{\geq m} (seq M (+ F) (n) \in ℂ \land \|seq M (+ F) (n) - seq M (+ F) (m)\| < x))$
131	2 130	syl	$⊢ φ \to (\forall x \in ℝ^{+} \exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ F) (n) \in ℂ \land \|seq M (+ F) (n) - seq M (+ F) (m)\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists m \in ℤ_{\geq N} \forall n \in ℤ_{\geq m} (seq M (+ F) (n) \in ℂ \land \|seq M (+ F) (n) - seq M (+ F) (m)\| < x))$
132	1 39	cau4	$⊢ N \in Z \to (\forall x \in ℝ^{+} \exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ G) (n) \in ℂ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists m \in ℤ_{\geq N} \forall n \in ℤ_{\geq m} (seq M (+ G) (n) \in ℂ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x))$
133	2 132	syl	$⊢ φ \to (\forall x \in ℝ^{+} \exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ G) (n) \in ℂ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists m \in ℤ_{\geq N} \forall n \in ℤ_{\geq m} (seq M (+ G) (n) \in ℂ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x))$
134	129 131 133	3imtr4d	$⊢ φ \to (\forall x \in ℝ^{+} \exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ F) (n) \in ℂ \land \|seq M (+ F) (n) - seq M (+ F) (m)\| < x) \to \forall x \in ℝ^{+} \exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ G) (n) \in ℂ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x))$
135	23 134	mpd	$⊢ φ \to \forall x \in ℝ^{+} \exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ G) (n) \in ℂ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x)$
136	1	uztrn2	$⊢ (m \in Z \land n \in ℤ_{\geq m}) \to n \in Z$
137		simpr	$⊢ (seq M (+ G) (n) \in ℂ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x) \to \|seq M (+ G) (n) - seq M (+ G) (m)\| < x$
138	27	biantrurd	$⊢ (φ \land n \in Z) \to (\|seq M (+ G) (n) - seq M (+ G) (m)\| < x \leftrightarrow (seq M (+ G) (n) \in ℝ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x))$
139	137 138	imbitrid	$⊢ (φ \land n \in Z) \to ((seq M (+ G) (n) \in ℂ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x) \to (seq M (+ G) (n) \in ℝ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x))$
140	136 139	sylan2	$⊢ (φ \land (m \in Z \land n \in ℤ_{\geq m})) \to ((seq M (+ G) (n) \in ℂ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x) \to (seq M (+ G) (n) \in ℝ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x))$
141	140	anassrs	$⊢ ((φ \land m \in Z) \land n \in ℤ_{\geq m}) \to ((seq M (+ G) (n) \in ℂ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x) \to (seq M (+ G) (n) \in ℝ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x))$
142	141	ralimdva	$⊢ (φ \land m \in Z) \to (\forall n \in ℤ_{\geq m} (seq M (+ G) (n) \in ℂ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x) \to \forall n \in ℤ_{\geq m} (seq M (+ G) (n) \in ℝ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x))$
143	142	reximdva	$⊢ φ \to (\exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ G) (n) \in ℂ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x) \to \exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ G) (n) \in ℝ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x))$
144	143	ralimdv	$⊢ φ \to (\forall x \in ℝ^{+} \exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ G) (n) \in ℂ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x) \to \forall x \in ℝ^{+} \exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ G) (n) \in ℝ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x))$
145	135 144	mpd	$⊢ φ \to \forall x \in ℝ^{+} \exists m \in Z \forall n \in ℤ_{\geq m} (seq M (+ G) (n) \in ℝ \land \|seq M (+ G) (n) - seq M (+ G) (m)\| < x)$
146	1 9 145	caurcvg2	$⊢ φ \to seq M (+ G) \in dom ⇝$

Metamath Proof Explorer

Theorem cvgcmp

Proof