Metamath Proof Explorer


Theorem ulmres

Description: A sequence of functions converges iff the tail of the sequence converges (for any finite cutoff). (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypotheses ulmres.z Z = M
ulmres.w W = N
ulmres.m φ N Z
ulmres.f φ F : Z S
Assertion ulmres φ F u S G F W u S G

Proof

Step Hyp Ref Expression
1 ulmres.z Z = M
2 ulmres.w W = N
3 ulmres.m φ N Z
4 ulmres.f φ F : Z S
5 ulmscl F u S G S V
6 ulmcl F u S G G : S
7 5 6 jca F u S G S V G : S
8 7 a1i φ F u S G S V G : S
9 ulmscl F W u S G S V
10 ulmcl F W u S G G : S
11 9 10 jca F W u S G S V G : S
12 11 a1i φ F W u S G S V G : S
13 3 1 eleqtrdi φ N M
14 13 adantr φ S V G : S N M
15 eluzel2 N M M
16 14 15 syl φ S V G : S M
17 1 rexuz3 M j Z k j z S F k z G z < r j k j z S F k z G z < r
18 16 17 syl φ S V G : S j Z k j z S F k z G z < r j k j z S F k z G z < r
19 eluzelz N M N
20 14 19 syl φ S V G : S N
21 2 rexuz3 N j W k j z S F k z G z < r j k j z S F k z G z < r
22 20 21 syl φ S V G : S j W k j z S F k z G z < r j k j z S F k z G z < r
23 18 22 bitr4d φ S V G : S j Z k j z S F k z G z < r j W k j z S F k z G z < r
24 23 ralbidv φ S V G : S r + j Z k j z S F k z G z < r r + j W k j z S F k z G z < r
25 4 adantr φ S V G : S F : Z S
26 eqidd φ S V G : S k Z z S F k z = F k z
27 eqidd φ S V G : S z S G z = G z
28 simprr φ S V G : S G : S
29 simprl φ S V G : S S V
30 1 16 25 26 27 28 29 ulm2 φ S V G : S F u S G r + j Z k j z S F k z G z < r
31 uzss N M N M
32 14 31 syl φ S V G : S N M
33 32 2 1 3sstr4g φ S V G : S W Z
34 25 33 fssresd φ S V G : S F W : W S
35 fvres k W F W k = F k
36 35 ad2antrl φ S V G : S k W z S F W k = F k
37 36 fveq1d φ S V G : S k W z S F W k z = F k z
38 2 20 34 37 27 28 29 ulm2 φ S V G : S F W u S G r + j W k j z S F k z G z < r
39 24 30 38 3bitr4d φ S V G : S F u S G F W u S G
40 39 ex φ S V G : S F u S G F W u S G
41 8 12 40 pm5.21ndd φ F u S G F W u S G