Metamath Proof Explorer


Theorem 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 = N
mtest.n φ N
mtest.s φ S V
mtest.f φ F : Z S
mtest.m φ M W
mtest.c φ k Z M k
mtest.l φ k Z z S F k z M k
mtest.d φ seq N + M dom
mtest.t φ seq N f + F u S T
Assertion mtestbdd φ x z S T z x

Proof

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