mtest

Description: The Weierstrass M-test. If F is a sequence of functions which are uniformly bounded by the convergent sequence M ( k ) , then the series generated by the sequence F converges uniformly. (Contributed by Mario Carneiro, 3-Mar-2015)

	Ref	Expression
Hypotheses	mtest.z	$⊢ Z = ℤ_{\geq N}$
	mtest.n	$⊢ φ \to N \in ℤ$
	mtest.s	$⊢ φ \to S \in V$
	mtest.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
	mtest.m	$⊢ φ \to M \in W$
	mtest.c	$⊢ (φ \land k \in Z) \to M (k) \in ℝ$
	mtest.l	$⊢ (φ \land (k \in Z \land z \in S)) \to \|F (k) (z)\| \leq M (k)$
	mtest.d	$⊢ φ \to seq N (+ M) \in dom ⇝$
Assertion	mtest	$⊢ φ \to seq N (\circ_{f} +, F) \in dom \underset{u}{⇝} (S)$

Proof

Step	Hyp	Ref	Expression
1		mtest.z	$⊢ Z = ℤ_{\geq N}$
2		mtest.n	$⊢ φ \to N \in ℤ$
3		mtest.s	$⊢ φ \to S \in V$
4		mtest.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
5		mtest.m	$⊢ φ \to M \in W$
6		mtest.c	$⊢ (φ \land k \in Z) \to M (k) \in ℝ$
7		mtest.l	$⊢ (φ \land (k \in Z \land z \in S)) \to \|F (k) (z)\| \leq M (k)$
8		mtest.d	$⊢ φ \to seq N (+ M) \in dom ⇝$
9	1	climcau	$⊢ (N \in ℤ \land seq N (+ M) \in dom ⇝) \to \forall r \in ℝ^{+} \exists j \in Z \forall i \in ℤ_{\geq j} \|seq N (+ M) (i) - seq N (+ M) (j)\| < r$
10	2 8 9	syl2anc	$⊢ φ \to \forall r \in ℝ^{+} \exists j \in Z \forall i \in ℤ_{\geq j} \|seq N (+ M) (i) - seq N (+ M) (j)\| < r$
11		seqfn	$⊢ N \in ℤ \to seq N (\circ_{f} +, F) Fn ℤ_{\geq N}$
12	2 11	syl	$⊢ φ \to seq N (\circ_{f} +, F) Fn ℤ_{\geq N}$
13	1	fneq2i	$⊢ seq N (\circ_{f} +, F) Fn Z \leftrightarrow seq N (\circ_{f} +, F) Fn ℤ_{\geq N}$
14	12 13	sylibr	$⊢ φ \to seq N (\circ_{f} +, F) Fn Z$
15	3	elexd	$⊢ φ \to S \in V$
16	15	adantr	$⊢ (φ \land i \in Z) \to S \in V$
17		simpr	$⊢ (φ \land i \in Z) \to i \in Z$
18	17 1	eleqtrdi	$⊢ (φ \land i \in Z) \to i \in ℤ_{\geq N}$
19	4	adantr	$⊢ (φ \land i \in Z) \to F : Z ⟶ ℂ^{S}$
20		elfzuz	$⊢ k \in (N \dots i) \to k \in ℤ_{\geq N}$
21	20 1	eleqtrrdi	$⊢ k \in (N \dots i) \to k \in Z$
22		ffvelrn	$⊢ (F : Z ⟶ ℂ^{S} \land k \in Z) \to F (k) \in (ℂ^{S})$
23	19 21 22	syl2an	$⊢ ((φ \land i \in Z) \land k \in (N \dots i)) \to F (k) \in (ℂ^{S})$
24		elmapi	$⊢ F (k) \in (ℂ^{S}) \to F (k) : S ⟶ ℂ$
25	23 24	syl	$⊢ ((φ \land i \in Z) \land k \in (N \dots i)) \to F (k) : S ⟶ ℂ$
26	25	feqmptd	$⊢ ((φ \land i \in Z) \land k \in (N \dots i)) \to F (k) = (z \in S ⟼ F (k) (z))$
27	21	adantl	$⊢ ((φ \land i \in Z) \land k \in (N \dots i)) \to k \in Z$
28		fveq2	$⊢ n = k \to F (n) = F (k)$
29	28	fveq1d	$⊢ n = k \to F (n) (z) = F (k) (z)$
30		eqid	$⊢ (n \in Z ⟼ F (n) (z)) = (n \in Z ⟼ F (n) (z))$
31		fvex	$⊢ F (k) (z) \in V$
32	29 30 31	fvmpt	$⊢ k \in Z \to (n \in Z ⟼ F (n) (z)) (k) = F (k) (z)$
33	27 32	syl	$⊢ ((φ \land i \in Z) \land k \in (N \dots i)) \to (n \in Z ⟼ F (n) (z)) (k) = F (k) (z)$
34	33	mpteq2dv	$⊢ ((φ \land i \in Z) \land k \in (N \dots i)) \to (z \in S ⟼ (n \in Z ⟼ F (n) (z)) (k)) = (z \in S ⟼ F (k) (z))$
35	26 34	eqtr4d	$⊢ ((φ \land i \in Z) \land k \in (N \dots i)) \to F (k) = (z \in S ⟼ (n \in Z ⟼ F (n) (z)) (k))$
36	16 18 35	seqof	$⊢ (φ \land i \in Z) \to seq N (\circ_{f} +, F) (i) = (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i))$
37	2	adantr	$⊢ (φ \land z \in S) \to N \in ℤ$
38	4	ffvelrnda	$⊢ (φ \land n \in Z) \to F (n) \in (ℂ^{S})$
39		elmapi	$⊢ F (n) \in (ℂ^{S}) \to F (n) : S ⟶ ℂ$
40	38 39	syl	$⊢ (φ \land n \in Z) \to F (n) : S ⟶ ℂ$
41	40	ffvelrnda	$⊢ ((φ \land n \in Z) \land z \in S) \to F (n) (z) \in ℂ$
42	41	an32s	$⊢ ((φ \land z \in S) \land n \in Z) \to F (n) (z) \in ℂ$
43	42	fmpttd	$⊢ (φ \land z \in S) \to (n \in Z ⟼ F (n) (z)) : Z ⟶ ℂ$
44	43	ffvelrnda	$⊢ ((φ \land z \in S) \land i \in Z) \to (n \in Z ⟼ F (n) (z)) (i) \in ℂ$
45	1 37 44	serf	$⊢ (φ \land z \in S) \to seq N (+ (n \in Z ⟼ F (n) (z))) : Z ⟶ ℂ$
46	45	ffvelrnda	$⊢ ((φ \land z \in S) \land i \in Z) \to seq N (+ (n \in Z ⟼ F (n) (z))) (i) \in ℂ$
47	46	an32s	$⊢ ((φ \land i \in Z) \land z \in S) \to seq N (+ (n \in Z ⟼ F (n) (z))) (i) \in ℂ$
48	47	fmpttd	$⊢ (φ \land i \in Z) \to (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i)) : S ⟶ ℂ$
49		cnex	$⊢ ℂ \in V$
50		elmapg	$⊢ (ℂ \in V \land S \in V) \to ((z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i)) \in (ℂ^{S}) \leftrightarrow (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i)) : S ⟶ ℂ)$
51	49 16 50	sylancr	$⊢ (φ \land i \in Z) \to ((z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i)) \in (ℂ^{S}) \leftrightarrow (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i)) : S ⟶ ℂ)$
52	48 51	mpbird	$⊢ (φ \land i \in Z) \to (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i)) \in (ℂ^{S})$
53	36 52	eqeltrd	$⊢ (φ \land i \in Z) \to seq N (\circ_{f} +, F) (i) \in (ℂ^{S})$
54	53	ralrimiva	$⊢ φ \to \forall i \in Z seq N (\circ_{f} +, F) (i) \in (ℂ^{S})$
55		ffnfv	$⊢ seq N (\circ_{f} +, F) : Z ⟶ ℂ^{S} \leftrightarrow (seq N (\circ_{f} +, F) Fn Z \land \forall i \in Z seq N (\circ_{f} +, F) (i) \in (ℂ^{S}))$
56	14 54 55	sylanbrc	$⊢ φ \to seq N (\circ_{f} +, F) : Z ⟶ ℂ^{S}$
57	56	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to seq N (\circ_{f} +, F) : Z ⟶ ℂ^{S}$
58	1	uztrn2	$⊢ (j \in Z \land i \in ℤ_{\geq j}) \to i \in Z$
59	58	adantl	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to i \in Z$
60	57 59	ffvelrnd	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to seq N (\circ_{f} +, F) (i) \in (ℂ^{S})$
61		elmapi	$⊢ seq N (\circ_{f} +, F) (i) \in (ℂ^{S}) \to seq N (\circ_{f} +, F) (i) : S ⟶ ℂ$
62	60 61	syl	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to seq N (\circ_{f} +, F) (i) : S ⟶ ℂ$
63	62	ffvelrnda	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to seq N (\circ_{f} +, F) (i) (z) \in ℂ$
64		simprl	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to j \in Z$
65	57 64	ffvelrnd	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to seq N (\circ_{f} +, F) (j) \in (ℂ^{S})$
66		elmapi	$⊢ seq N (\circ_{f} +, F) (j) \in (ℂ^{S}) \to seq N (\circ_{f} +, F) (j) : S ⟶ ℂ$
67	65 66	syl	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to seq N (\circ_{f} +, F) (j) : S ⟶ ℂ$
68	67	ffvelrnda	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to seq N (\circ_{f} +, F) (j) (z) \in ℂ$
69	63 68	subcld	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z) \in ℂ$
70	69	abscld	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| \in ℝ$
71		fzfid	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to (j + 1 \dots i) \in Fin$
72		ssun2	$⊢ (j + 1 \dots i) \subseteq (N \dots j) \cup (j + 1 \dots i)$
73	64 1	eleqtrdi	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to j \in ℤ_{\geq N}$
74		simprr	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to i \in ℤ_{\geq j}$
75		elfzuzb	$⊢ j \in (N \dots i) \leftrightarrow (j \in ℤ_{\geq N} \land i \in ℤ_{\geq j})$
76	73 74 75	sylanbrc	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to j \in (N \dots i)$
77		fzsplit	$⊢ j \in (N \dots i) \to (N \dots i) = (N \dots j) \cup (j + 1 \dots i)$
78	76 77	syl	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to (N \dots i) = (N \dots j) \cup (j + 1 \dots i)$
79	72 78	sseqtrrid	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to (j + 1 \dots i) \subseteq (N \dots i)$
80	79	sselda	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land k \in (j + 1 \dots i)) \to k \in (N \dots i)$
81	80	adantlr	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \land k \in (j + 1 \dots i)) \to k \in (N \dots i)$
82	4	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to F : Z ⟶ ℂ^{S}$
83	82 21 22	syl2an	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land k \in (N \dots i)) \to F (k) \in (ℂ^{S})$
84	83 24	syl	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land k \in (N \dots i)) \to F (k) : S ⟶ ℂ$
85	84	ffvelrnda	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land k \in (N \dots i)) \land z \in S) \to F (k) (z) \in ℂ$
86	85	an32s	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \land k \in (N \dots i)) \to F (k) (z) \in ℂ$
87	81 86	syldan	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \land k \in (j + 1 \dots i)) \to F (k) (z) \in ℂ$
88	87	abscld	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \land k \in (j + 1 \dots i)) \to \|F (k) (z)\| \in ℝ$
89	71 88	fsumrecl	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \sum_{k = j + 1}^{i} \|F (k) (z)\| \in ℝ$
90	1 2 6	serfre	$⊢ φ \to seq N (+ M) : Z ⟶ ℝ$
91	90	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to seq N (+ M) : Z ⟶ ℝ$
92	91 59	ffvelrnd	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to seq N (+ M) (i) \in ℝ$
93	91 64	ffvelrnd	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to seq N (+ M) (j) \in ℝ$
94	92 93	resubcld	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to seq N (+ M) (i) - seq N (+ M) (j) \in ℝ$
95	94	recnd	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to seq N (+ M) (i) - seq N (+ M) (j) \in ℂ$
96	95	abscld	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to \|seq N (+ M) (i) - seq N (+ M) (j)\| \in ℝ$
97	96	adantr	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \|seq N (+ M) (i) - seq N (+ M) (j)\| \in ℝ$
98	58 36	sylan2	$⊢ (φ \land (j \in Z \land i \in ℤ_{\geq j})) \to seq N (\circ_{f} +, F) (i) = (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i))$
99	98	adantlr	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to seq N (\circ_{f} +, F) (i) = (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i))$
100	99	fveq1d	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to seq N (\circ_{f} +, F) (i) (z) = (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i)) (z)$
101		fvex	$⊢ seq N (+ (n \in Z ⟼ F (n) (z))) (i) \in V$
102		eqid	$⊢ (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i)) = (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i))$
103	102	fvmpt2	$⊢ (z \in S \land seq N (+ (n \in Z ⟼ F (n) (z))) (i) \in V) \to (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i)) (z) = seq N (+ (n \in Z ⟼ F (n) (z))) (i)$
104	101 103	mpan2	$⊢ z \in S \to (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i)) (z) = seq N (+ (n \in Z ⟼ F (n) (z))) (i)$
105	100 104	sylan9eq	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to seq N (\circ_{f} +, F) (i) (z) = seq N (+ (n \in Z ⟼ F (n) (z))) (i)$
106		fveq2	$⊢ i = j \to seq N (\circ_{f} +, F) (i) = seq N (\circ_{f} +, F) (j)$
107		fveq2	$⊢ i = j \to seq N (+ (n \in Z ⟼ F (n) (z))) (i) = seq N (+ (n \in Z ⟼ F (n) (z))) (j)$
108	107	mpteq2dv	$⊢ i = j \to (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i)) = (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (j))$
109	106 108	eqeq12d	$⊢ i = j \to (seq N (\circ_{f} +, F) (i) = (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i)) \leftrightarrow seq N (\circ_{f} +, F) (j) = (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (j)))$
110	36	ralrimiva	$⊢ φ \to \forall i \in Z seq N (\circ_{f} +, F) (i) = (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i))$
111	110	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to \forall i \in Z seq N (\circ_{f} +, F) (i) = (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (i))$
112	109 111 64	rspcdva	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to seq N (\circ_{f} +, F) (j) = (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (j))$
113	112	fveq1d	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to seq N (\circ_{f} +, F) (j) (z) = (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (j)) (z)$
114		fvex	$⊢ seq N (+ (n \in Z ⟼ F (n) (z))) (j) \in V$
115		eqid	$⊢ (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (j)) = (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (j))$
116	115	fvmpt2	$⊢ (z \in S \land seq N (+ (n \in Z ⟼ F (n) (z))) (j) \in V) \to (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (j)) (z) = seq N (+ (n \in Z ⟼ F (n) (z))) (j)$
117	114 116	mpan2	$⊢ z \in S \to (z \in S ⟼ seq N (+ (n \in Z ⟼ F (n) (z))) (j)) (z) = seq N (+ (n \in Z ⟼ F (n) (z))) (j)$
118	113 117	sylan9eq	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to seq N (\circ_{f} +, F) (j) (z) = seq N (+ (n \in Z ⟼ F (n) (z))) (j)$
119	105 118	oveq12d	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z) = seq N (+ (n \in Z ⟼ F (n) (z))) (i) - seq N (+ (n \in Z ⟼ F (n) (z))) (j)$
120	21	adantl	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \land k \in (N \dots i)) \to k \in Z$
121	120 32	syl	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \land k \in (N \dots i)) \to (n \in Z ⟼ F (n) (z)) (k) = F (k) (z)$
122	59	adantr	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to i \in Z$
123	122 1	eleqtrdi	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to i \in ℤ_{\geq N}$
124	121 123 86	fsumser	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \sum_{k = N}^{i} F (k) (z) = seq N (+ (n \in Z ⟼ F (n) (z))) (i)$
125		elfzuz	$⊢ k \in (N \dots j) \to k \in ℤ_{\geq N}$
126	125 1	eleqtrrdi	$⊢ k \in (N \dots j) \to k \in Z$
127	126	adantl	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \land k \in (N \dots j)) \to k \in Z$
128	127 32	syl	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \land k \in (N \dots j)) \to (n \in Z ⟼ F (n) (z)) (k) = F (k) (z)$
129	64	adantr	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to j \in Z$
130	129 1	eleqtrdi	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to j \in ℤ_{\geq N}$
131	82 126 22	syl2an	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land k \in (N \dots j)) \to F (k) \in (ℂ^{S})$
132	131 24	syl	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land k \in (N \dots j)) \to F (k) : S ⟶ ℂ$
133	132	ffvelrnda	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land k \in (N \dots j)) \land z \in S) \to F (k) (z) \in ℂ$
134	133	an32s	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \land k \in (N \dots j)) \to F (k) (z) \in ℂ$
135	128 130 134	fsumser	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \sum_{k = N}^{j} F (k) (z) = seq N (+ (n \in Z ⟼ F (n) (z))) (j)$
136	124 135	oveq12d	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \sum_{k = N}^{i} F (k) (z) - \sum_{k = N}^{j} F (k) (z) = seq N (+ (n \in Z ⟼ F (n) (z))) (i) - seq N (+ (n \in Z ⟼ F (n) (z))) (j)$
137		fzfid	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to (N \dots j) \in Fin$
138	137 134	fsumcl	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \sum_{k = N}^{j} F (k) (z) \in ℂ$
139	71 87	fsumcl	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \sum_{k = j + 1}^{i} F (k) (z) \in ℂ$
140		eluzelre	$⊢ j \in ℤ_{\geq N} \to j \in ℝ$
141	73 140	syl	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to j \in ℝ$
142	141	ltp1d	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to j < j + 1$
143		fzdisj	$⊢ j < j + 1 \to (N \dots j) \cap (j + 1 \dots i) = \emptyset$
144	142 143	syl	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to (N \dots j) \cap (j + 1 \dots i) = \emptyset$
145	144	adantr	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to (N \dots j) \cap (j + 1 \dots i) = \emptyset$
146	78	adantr	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to (N \dots i) = (N \dots j) \cup (j + 1 \dots i)$
147		fzfid	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to (N \dots i) \in Fin$
148	145 146 147 86	fsumsplit	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \sum_{k = N}^{i} F (k) (z) = \sum_{k = N}^{j} F (k) (z) + \sum_{k = j + 1}^{i} F (k) (z)$
149	138 139 148	mvrladdd	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \sum_{k = N}^{i} F (k) (z) - \sum_{k = N}^{j} F (k) (z) = \sum_{k = j + 1}^{i} F (k) (z)$
150	119 136 149	3eqtr2d	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z) = \sum_{k = j + 1}^{i} F (k) (z)$
151	150	fveq2d	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| = \|\sum_{k = j + 1}^{i} F (k) (z)\|$
152	71 87	fsumabs	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \|\sum_{k = j + 1}^{i} F (k) (z)\| \leq \sum_{k = j + 1}^{i} \|F (k) (z)\|$
153	151 152	eqbrtrd	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| \leq \sum_{k = j + 1}^{i} \|F (k) (z)\|$
154		simpll	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to φ$
155	154 21 6	syl2an	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land k \in (N \dots i)) \to M (k) \in ℝ$
156	80 155	syldan	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land k \in (j + 1 \dots i)) \to M (k) \in ℝ$
157	156	adantlr	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \land k \in (j + 1 \dots i)) \to M (k) \in ℝ$
158	81 21	syl	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \land k \in (j + 1 \dots i)) \to k \in Z$
159	7	ad4ant14	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land (k \in Z \land z \in S)) \to \|F (k) (z)\| \leq M (k)$
160	159	anass1rs	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \land k \in Z) \to \|F (k) (z)\| \leq M (k)$
161	158 160	syldan	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \land k \in (j + 1 \dots i)) \to \|F (k) (z)\| \leq M (k)$
162	71 88 157 161	fsumle	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \sum_{k = j + 1}^{i} \|F (k) (z)\| \leq \sum_{k = j + 1}^{i} M (k)$
163		eqidd	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land k \in (N \dots i)) \to M (k) = M (k)$
164	59 1	eleqtrdi	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to i \in ℤ_{\geq N}$
165	155	recnd	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land k \in (N \dots i)) \to M (k) \in ℂ$
166	163 164 165	fsumser	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to \sum_{k = N}^{i} M (k) = seq N (+ M) (i)$
167		eqidd	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land k \in (N \dots j)) \to M (k) = M (k)$
168	154 126 6	syl2an	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land k \in (N \dots j)) \to M (k) \in ℝ$
169	168	recnd	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land k \in (N \dots j)) \to M (k) \in ℂ$
170	167 73 169	fsumser	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to \sum_{k = N}^{j} M (k) = seq N (+ M) (j)$
171	166 170	oveq12d	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to \sum_{k = N}^{i} M (k) - \sum_{k = N}^{j} M (k) = seq N (+ M) (i) - seq N (+ M) (j)$
172		fzfid	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to (N \dots j) \in Fin$
173	172 169	fsumcl	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to \sum_{k = N}^{j} M (k) \in ℂ$
174		fzfid	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to (j + 1 \dots i) \in Fin$
175	80 165	syldan	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land k \in (j + 1 \dots i)) \to M (k) \in ℂ$
176	174 175	fsumcl	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to \sum_{k = j + 1}^{i} M (k) \in ℂ$
177		fzfid	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to (N \dots i) \in Fin$
178	144 78 177 165	fsumsplit	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to \sum_{k = N}^{i} M (k) = \sum_{k = N}^{j} M (k) + \sum_{k = j + 1}^{i} M (k)$
179	173 176 178	mvrladdd	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to \sum_{k = N}^{i} M (k) - \sum_{k = N}^{j} M (k) = \sum_{k = j + 1}^{i} M (k)$
180	171 179	eqtr3d	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to seq N (+ M) (i) - seq N (+ M) (j) = \sum_{k = j + 1}^{i} M (k)$
181	180	fveq2d	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to \|seq N (+ M) (i) - seq N (+ M) (j)\| = \|\sum_{k = j + 1}^{i} M (k)\|$
182	181	adantr	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \|seq N (+ M) (i) - seq N (+ M) (j)\| = \|\sum_{k = j + 1}^{i} M (k)\|$
183	180 94	eqeltrrd	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to \sum_{k = j + 1}^{i} M (k) \in ℝ$
184	183	adantr	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \sum_{k = j + 1}^{i} M (k) \in ℝ$
185		0red	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \land k \in (j + 1 \dots i)) \to 0 \in ℝ$
186	87	absge0d	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \land k \in (j + 1 \dots i)) \to 0 \leq \|F (k) (z)\|$
187	185 88 157 186 161	letrd	$⊢ ((((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \land k \in (j + 1 \dots i)) \to 0 \leq M (k)$
188	71 157 187	fsumge0	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to 0 \leq \sum_{k = j + 1}^{i} M (k)$
189	184 188	absidd	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \|\sum_{k = j + 1}^{i} M (k)\| = \sum_{k = j + 1}^{i} M (k)$
190	182 189	eqtrd	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \|seq N (+ M) (i) - seq N (+ M) (j)\| = \sum_{k = j + 1}^{i} M (k)$
191	162 190	breqtrrd	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \sum_{k = j + 1}^{i} \|F (k) (z)\| \leq \|seq N (+ M) (i) - seq N (+ M) (j)\|$
192	70 89 97 153 191	letrd	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to \|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| \leq \|seq N (+ M) (i) - seq N (+ M) (j)\|$
193		simpllr	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to r \in ℝ^{+}$
194	193	rpred	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to r \in ℝ$
195		lelttr	$⊢ (\|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| \in ℝ \land \|seq N (+ M) (i) - seq N (+ M) (j)\| \in ℝ \land r \in ℝ) \to ((\|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| \leq \|seq N (+ M) (i) - seq N (+ M) (j)\| \land \|seq N (+ M) (i) - seq N (+ M) (j)\| < r) \to \|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| < r)$
196	70 97 194 195	syl3anc	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to ((\|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| \leq \|seq N (+ M) (i) - seq N (+ M) (j)\| \land \|seq N (+ M) (i) - seq N (+ M) (j)\| < r) \to \|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| < r)$
197	192 196	mpand	$⊢ (((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \land z \in S) \to (\|seq N (+ M) (i) - seq N (+ M) (j)\| < r \to \|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| < r)$
198	197	ralrimdva	$⊢ ((φ \land r \in ℝ^{+}) \land (j \in Z \land i \in ℤ_{\geq j})) \to (\|seq N (+ M) (i) - seq N (+ M) (j)\| < r \to \forall z \in S \|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| < r)$
199	198	anassrs	$⊢ (((φ \land r \in ℝ^{+}) \land j \in Z) \land i \in ℤ_{\geq j}) \to (\|seq N (+ M) (i) - seq N (+ M) (j)\| < r \to \forall z \in S \|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| < r)$
200	199	ralimdva	$⊢ ((φ \land r \in ℝ^{+}) \land j \in Z) \to (\forall i \in ℤ_{\geq j} \|seq N (+ M) (i) - seq N (+ M) (j)\| < r \to \forall i \in ℤ_{\geq j} \forall z \in S \|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| < r)$
201	200	reximdva	$⊢ (φ \land r \in ℝ^{+}) \to (\exists j \in Z \forall i \in ℤ_{\geq j} \|seq N (+ M) (i) - seq N (+ M) (j)\| < r \to \exists j \in Z \forall i \in ℤ_{\geq j} \forall z \in S \|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| < r)$
202	201	ralimdva	$⊢ φ \to (\forall r \in ℝ^{+} \exists j \in Z \forall i \in ℤ_{\geq j} \|seq N (+ M) (i) - seq N (+ M) (j)\| < r \to \forall r \in ℝ^{+} \exists j \in Z \forall i \in ℤ_{\geq j} \forall z \in S \|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| < r)$
203	10 202	mpd	$⊢ φ \to \forall r \in ℝ^{+} \exists j \in Z \forall i \in ℤ_{\geq j} \forall z \in S \|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| < r$
204	1 2 3 56	ulmcau	$⊢ φ \to (seq N (\circ_{f} +, F) \in dom \underset{u}{⇝} (S) \leftrightarrow \forall r \in ℝ^{+} \exists j \in Z \forall i \in ℤ_{\geq j} \forall z \in S \|seq N (\circ_{f} +, F) (i) (z) - seq N (\circ_{f} +, F) (j) (z)\| < r)$
205	203 204	mpbird	$⊢ φ \to seq N (\circ_{f} +, F) \in dom \underset{u}{⇝} (S)$

Metamath Proof Explorer

Theorem mtest

Proof