mtestbdd

Description: Given the hypotheses of the Weierstrass M-test, the convergent function of the sequence is uniformly bounded. (Contributed by Mario Carneiro, 9-Jul-2017)

	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 ⇝$
	mtest.t	$⊢ φ \to seq N (\circ_{f} +, F) \underset{u}{⇝} (S) T$
Assertion	mtestbdd	$⊢ φ \to \exists x \in ℝ \forall z \in S \|T (z)\| \leq x$

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		mtest.t	$⊢ φ \to seq N (\circ_{f} +, F) \underset{u}{⇝} (S) T$
10	6	recnd	$⊢ (φ \land k \in Z) \to M (k) \in ℂ$
11	1 2 10	serf	$⊢ φ \to seq N (+ M) : Z ⟶ ℂ$
12	11	ffvelrnda	$⊢ (φ \land m \in Z) \to seq N (+ M) (m) \in ℂ$
13	12	ralrimiva	$⊢ φ \to \forall m \in Z seq N (+ M) (m) \in ℂ$
14	1	climbdd	$⊢ (N \in ℤ \land seq N (+ M) \in dom ⇝ \land \forall m \in Z seq N (+ M) (m) \in ℂ) \to \exists y \in ℝ \forall m \in Z \|seq N (+ M) (m)\| \leq y$
15	2 8 13 14	syl3anc	$⊢ φ \to \exists y \in ℝ \forall m \in Z \|seq N (+ M) (m)\| \leq y$
16	2	adantr	$⊢ (φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \to N \in ℤ$
17		seqfn	$⊢ N \in ℤ \to seq N (\circ_{f} +, F) Fn ℤ_{\geq N}$
18	2 17	syl	$⊢ φ \to seq N (\circ_{f} +, F) Fn ℤ_{\geq N}$
19	1	fneq2i	$⊢ seq N (\circ_{f} +, F) Fn Z \leftrightarrow seq N (\circ_{f} +, F) Fn ℤ_{\geq N}$
20	18 19	sylibr	$⊢ φ \to seq N (\circ_{f} +, F) Fn Z$
21		ulmf2	$⊢ (seq N (\circ_{f} +, F) Fn Z \land seq N (\circ_{f} +, F) \underset{u}{⇝} (S) T) \to seq N (\circ_{f} +, F) : Z ⟶ ℂ^{S}$
22	20 9 21	syl2anc	$⊢ φ \to seq N (\circ_{f} +, F) : Z ⟶ ℂ^{S}$
23	22	adantr	$⊢ (φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \to seq N (\circ_{f} +, F) : Z ⟶ ℂ^{S}$
24		simplrl	$⊢ ((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \to y \in ℝ$
25		fveq2	$⊢ x = z \to F (j) (x) = F (j) (z)$
26	25	mpteq2dv	$⊢ x = z \to (j \in Z ⟼ F (j) (x)) = (j \in Z ⟼ F (j) (z))$
27	26	seqeq3d	$⊢ x = z \to seq N (+ (j \in Z ⟼ F (j) (x))) = seq N (+ (j \in Z ⟼ F (j) (z)))$
28	27	fveq1d	$⊢ x = z \to seq N (+ (j \in Z ⟼ F (j) (x))) (n) = seq N (+ (j \in Z ⟼ F (j) (z))) (n)$
29		eqid	$⊢ (x \in S ⟼ seq N (+ (j \in Z ⟼ F (j) (x))) (n)) = (x \in S ⟼ seq N (+ (j \in Z ⟼ F (j) (x))) (n))$
30		fvex	$⊢ seq N (+ (j \in Z ⟼ F (j) (z))) (n) \in V$
31	28 29 30	fvmpt	$⊢ z \in S \to (x \in S ⟼ seq N (+ (j \in Z ⟼ F (j) (x))) (n)) (z) = seq N (+ (j \in Z ⟼ F (j) (z))) (n)$
32	31	adantl	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to (x \in S ⟼ seq N (+ (j \in Z ⟼ F (j) (x))) (n)) (z) = seq N (+ (j \in Z ⟼ F (j) (z))) (n)$
33	4	ad3antrrr	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to F : Z ⟶ ℂ^{S}$
34	33	feqmptd	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to F = (j \in Z ⟼ F (j))$
35	33	ffvelrnda	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land j \in Z) \to F (j) \in (ℂ^{S})$
36		elmapi	$⊢ F (j) \in (ℂ^{S}) \to F (j) : S ⟶ ℂ$
37	35 36	syl	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land j \in Z) \to F (j) : S ⟶ ℂ$
38	37	feqmptd	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land j \in Z) \to F (j) = (x \in S ⟼ F (j) (x))$
39	38	mpteq2dva	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to (j \in Z ⟼ F (j)) = (j \in Z ⟼ (x \in S ⟼ F (j) (x)))$
40	34 39	eqtrd	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to F = (j \in Z ⟼ (x \in S ⟼ F (j) (x)))$
41	40	seqeq3d	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to seq N (\circ_{f} +, F) = seq N (\circ_{f} +, (j \in Z ⟼ (x \in S ⟼ F (j) (x))))$
42	41	fveq1d	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to seq N (\circ_{f} +, F) (n) = seq N (\circ_{f} +, (j \in Z ⟼ (x \in S ⟼ F (j) (x)))) (n)$
43	3	ad3antrrr	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to S \in V$
44		simplr	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to n \in Z$
45	44 1	eleqtrdi	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to n \in ℤ_{\geq N}$
46		elfzuz	$⊢ k \in (N \dots n) \to k \in ℤ_{\geq N}$
47	46 1	eleqtrrdi	$⊢ k \in (N \dots n) \to k \in Z$
48	47	ssriv	$⊢ (N \dots n) \subseteq Z$
49	48	a1i	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to (N \dots n) \subseteq Z$
50	37	ffvelrnda	$⊢ (((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land j \in Z) \land x \in S) \to F (j) (x) \in ℂ$
51	50	anasss	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land (j \in Z \land x \in S)) \to F (j) (x) \in ℂ$
52	43 45 49 51	seqof2	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to seq N (\circ_{f} +, (j \in Z ⟼ (x \in S ⟼ F (j) (x)))) (n) = (x \in S ⟼ seq N (+ (j \in Z ⟼ F (j) (x))) (n))$
53	42 52	eqtrd	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to seq N (\circ_{f} +, F) (n) = (x \in S ⟼ seq N (+ (j \in Z ⟼ F (j) (x))) (n))$
54	53	fveq1d	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to seq N (\circ_{f} +, F) (n) (z) = (x \in S ⟼ seq N (+ (j \in Z ⟼ F (j) (x))) (n)) (z)$
55	47	adantl	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land k \in (N \dots n)) \to k \in Z$
56		fveq2	$⊢ j = k \to F (j) = F (k)$
57	56	fveq1d	$⊢ j = k \to F (j) (z) = F (k) (z)$
58		eqid	$⊢ (j \in Z ⟼ F (j) (z)) = (j \in Z ⟼ F (j) (z))$
59		fvex	$⊢ F (k) (z) \in V$
60	57 58 59	fvmpt	$⊢ k \in Z \to (j \in Z ⟼ F (j) (z)) (k) = F (k) (z)$
61	55 60	syl	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land k \in (N \dots n)) \to (j \in Z ⟼ F (j) (z)) (k) = F (k) (z)$
62		simplr	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land j \in Z) \to z \in S$
63	37 62	ffvelrnd	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land j \in Z) \to F (j) (z) \in ℂ$
64	63	fmpttd	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to (j \in Z ⟼ F (j) (z)) : Z ⟶ ℂ$
65	64	ffvelrnda	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land k \in Z) \to (j \in Z ⟼ F (j) (z)) (k) \in ℂ$
66	47 65	sylan2	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land k \in (N \dots n)) \to (j \in Z ⟼ F (j) (z)) (k) \in ℂ$
67	61 66	eqeltrrd	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land k \in (N \dots n)) \to F (k) (z) \in ℂ$
68	61 45 67	fsumser	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \sum_{k = N}^{n} F (k) (z) = seq N (+ (j \in Z ⟼ F (j) (z))) (n)$
69	32 54 68	3eqtr4d	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to seq N (\circ_{f} +, F) (n) (z) = \sum_{k = N}^{n} F (k) (z)$
70	69	fveq2d	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \|seq N (\circ_{f} +, F) (n) (z)\| = \|\sum_{k = N}^{n} F (k) (z)\|$
71		fzfid	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to (N \dots n) \in Fin$
72	71 67	fsumcl	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \sum_{k = N}^{n} F (k) (z) \in ℂ$
73	72	abscld	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \|\sum_{k = N}^{n} F (k) (z)\| \in ℝ$
74	67	abscld	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land k \in (N \dots n)) \to \|F (k) (z)\| \in ℝ$
75	71 74	fsumrecl	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \sum_{k = N}^{n} \|F (k) (z)\| \in ℝ$
76	24	adantr	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to y \in ℝ$
77	71 67	fsumabs	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \|\sum_{k = N}^{n} F (k) (z)\| \leq \sum_{k = N}^{n} \|F (k) (z)\|$
78		simp-4l	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land k \in (N \dots n)) \to φ$
79	78 55 6	syl2anc	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land k \in (N \dots n)) \to M (k) \in ℝ$
80	71 79	fsumrecl	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \sum_{k = N}^{n} M (k) \in ℝ$
81		simplr	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land k \in (N \dots n)) \to z \in S$
82	78 55 81 7	syl12anc	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land k \in (N \dots n)) \to \|F (k) (z)\| \leq M (k)$
83	71 74 79 82	fsumle	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \sum_{k = N}^{n} \|F (k) (z)\| \leq \sum_{k = N}^{n} M (k)$
84	80	recnd	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \sum_{k = N}^{n} M (k) \in ℂ$
85	84	abscld	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \|\sum_{k = N}^{n} M (k)\| \in ℝ$
86	80	leabsd	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \sum_{k = N}^{n} M (k) \leq \|\sum_{k = N}^{n} M (k)\|$
87		eqidd	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land k \in (N \dots n)) \to M (k) = M (k)$
88	78 55 10	syl2anc	$⊢ ((((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \land k \in (N \dots n)) \to M (k) \in ℂ$
89	87 45 88	fsumser	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \sum_{k = N}^{n} M (k) = seq N (+ M) (n)$
90	89	fveq2d	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \|\sum_{k = N}^{n} M (k)\| = \|seq N (+ M) (n)\|$
91		simprr	$⊢ (φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \to \forall m \in Z \|seq N (+ M) (m)\| \leq y$
92		fveq2	$⊢ m = n \to seq N (+ M) (m) = seq N (+ M) (n)$
93	92	fveq2d	$⊢ m = n \to \|seq N (+ M) (m)\| = \|seq N (+ M) (n)\|$
94	93	breq1d	$⊢ m = n \to (\|seq N (+ M) (m)\| \leq y \leftrightarrow \|seq N (+ M) (n)\| \leq y)$
95	94	rspccva	$⊢ (\forall m \in Z \|seq N (+ M) (m)\| \leq y \land n \in Z) \to \|seq N (+ M) (n)\| \leq y$
96	91 95	sylan	$⊢ ((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \to \|seq N (+ M) (n)\| \leq y$
97	96	adantr	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \|seq N (+ M) (n)\| \leq y$
98	90 97	eqbrtrd	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \|\sum_{k = N}^{n} M (k)\| \leq y$
99	80 85 76 86 98	letrd	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \sum_{k = N}^{n} M (k) \leq y$
100	75 80 76 83 99	letrd	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \sum_{k = N}^{n} \|F (k) (z)\| \leq y$
101	73 75 76 77 100	letrd	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \|\sum_{k = N}^{n} F (k) (z)\| \leq y$
102	70 101	eqbrtrd	$⊢ (((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \land z \in S) \to \|seq N (\circ_{f} +, F) (n) (z)\| \leq y$
103	102	ralrimiva	$⊢ ((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \to \forall z \in S \|seq N (\circ_{f} +, F) (n) (z)\| \leq y$
104		brralrspcev	$⊢ (y \in ℝ \land \forall z \in S \|seq N (\circ_{f} +, F) (n) (z)\| \leq y) \to \exists x \in ℝ \forall z \in S \|seq N (\circ_{f} +, F) (n) (z)\| \leq x$
105	24 103 104	syl2anc	$⊢ ((φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \land n \in Z) \to \exists x \in ℝ \forall z \in S \|seq N (\circ_{f} +, F) (n) (z)\| \leq x$
106	9	adantr	$⊢ (φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \to seq N (\circ_{f} +, F) \underset{u}{⇝} (S) T$
107	1 16 23 105 106	ulmbdd	$⊢ (φ \land (y \in ℝ \land \forall m \in Z \|seq N (+ M) (m)\| \leq y)) \to \exists x \in ℝ \forall z \in S \|T (z)\| \leq x$
108	15 107	rexlimddv	$⊢ φ \to \exists x \in ℝ \forall z \in S \|T (z)\| \leq x$

Metamath Proof Explorer

Theorem mtestbdd

Proof