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 = ℤ_{\geq M}$
	ulmres.w	$⊢ W = ℤ_{\geq N}$
	ulmres.m	$⊢ φ \to N \in Z$
	ulmres.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
Assertion	ulmres	$⊢ φ \to (F \underset{u}{⇝} (S) G \leftrightarrow ({F ↾}_{W}) \underset{u}{⇝} (S) G)$

Proof

Step	Hyp	Ref	Expression
1		ulmres.z	$⊢ Z = ℤ_{\geq M}$
2		ulmres.w	$⊢ W = ℤ_{\geq N}$
3		ulmres.m	$⊢ φ \to N \in Z$
4		ulmres.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
5		ulmscl	$⊢ F \underset{u}{⇝} (S) G \to S \in V$
6		ulmcl	$⊢ F \underset{u}{⇝} (S) G \to G : S ⟶ ℂ$
7	5 6	jca	$⊢ F \underset{u}{⇝} (S) G \to (S \in V \land G : S ⟶ ℂ)$
8	7	a1i	$⊢ φ \to (F \underset{u}{⇝} (S) G \to (S \in V \land G : S ⟶ ℂ))$
9		ulmscl	$⊢ ({F ↾}_{W}) \underset{u}{⇝} (S) G \to S \in V$
10		ulmcl	$⊢ ({F ↾}_{W}) \underset{u}{⇝} (S) G \to G : S ⟶ ℂ$
11	9 10	jca	$⊢ ({F ↾}_{W}) \underset{u}{⇝} (S) G \to (S \in V \land G : S ⟶ ℂ)$
12	11	a1i	$⊢ φ \to (({F ↾}_{W}) \underset{u}{⇝} (S) G \to (S \in V \land G : S ⟶ ℂ))$
13	3 1	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq M}$
14	13	adantr	$⊢ (φ \land (S \in V \land G : S ⟶ ℂ)) \to N \in ℤ_{\geq M}$
15		eluzel2	$⊢ N \in ℤ_{\geq M} \to M \in ℤ$
16	14 15	syl	$⊢ (φ \land (S \in V \land G : S ⟶ ℂ)) \to M \in ℤ$
17	1	rexuz3	$⊢ M \in ℤ \to (\exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < r \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < r)$
18	16 17	syl	$⊢ (φ \land (S \in V \land G : S ⟶ ℂ)) \to (\exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < r \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < r)$
19		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
20	14 19	syl	$⊢ (φ \land (S \in V \land G : S ⟶ ℂ)) \to N \in ℤ$
21	2	rexuz3	$⊢ N \in ℤ \to (\exists j \in W \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < r \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < r)$
22	20 21	syl	$⊢ (φ \land (S \in V \land G : S ⟶ ℂ)) \to (\exists j \in W \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < r \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < r)$
23	18 22	bitr4d	$⊢ (φ \land (S \in V \land G : S ⟶ ℂ)) \to (\exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < r \leftrightarrow \exists j \in W \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < r)$
24	23	ralbidv	$⊢ (φ \land (S \in V \land G : S ⟶ ℂ)) \to (\forall r \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < r \leftrightarrow \forall r \in ℝ^{+} \exists j \in W \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < r)$
25	4	adantr	$⊢ (φ \land (S \in V \land G : S ⟶ ℂ)) \to F : Z ⟶ ℂ^{S}$
26		eqidd	$⊢ ((φ \land (S \in V \land G : S ⟶ ℂ)) \land (k \in Z \land z \in S)) \to F (k) (z) = F (k) (z)$
27		eqidd	$⊢ ((φ \land (S \in V \land G : S ⟶ ℂ)) \land z \in S) \to G (z) = G (z)$
28		simprr	$⊢ (φ \land (S \in V \land G : S ⟶ ℂ)) \to G : S ⟶ ℂ$
29		simprl	$⊢ (φ \land (S \in V \land G : S ⟶ ℂ)) \to S \in V$
30	1 16 25 26 27 28 29	ulm2	$⊢ (φ \land (S \in V \land G : S ⟶ ℂ)) \to (F \underset{u}{⇝} (S) G \leftrightarrow \forall r \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < r)$
31		uzss	$⊢ N \in ℤ_{\geq M} \to ℤ_{\geq N} \subseteq ℤ_{\geq M}$
32	14 31	syl	$⊢ (φ \land (S \in V \land G : S ⟶ ℂ)) \to ℤ_{\geq N} \subseteq ℤ_{\geq M}$
33	32 2 1	3sstr4g	$⊢ (φ \land (S \in V \land G : S ⟶ ℂ)) \to W \subseteq Z$
34	25 33	fssresd	$⊢ (φ \land (S \in V \land G : S ⟶ ℂ)) \to ({F ↾}_{W}) : W ⟶ ℂ^{S}$
35		fvres	$⊢ k \in W \to ({F ↾}_{W}) (k) = F (k)$
36	35	ad2antrl	$⊢ ((φ \land (S \in V \land G : S ⟶ ℂ)) \land (k \in W \land z \in S)) \to ({F ↾}_{W}) (k) = F (k)$
37	36	fveq1d	$⊢ ((φ \land (S \in V \land G : S ⟶ ℂ)) \land (k \in W \land z \in S)) \to ({F ↾}_{W}) (k) (z) = F (k) (z)$
38	2 20 34 37 27 28 29	ulm2	$⊢ (φ \land (S \in V \land G : S ⟶ ℂ)) \to (({F ↾}_{W}) \underset{u}{⇝} (S) G \leftrightarrow \forall r \in ℝ^{+} \exists j \in W \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - G (z)\| < r)$
39	24 30 38	3bitr4d	$⊢ (φ \land (S \in V \land G : S ⟶ ℂ)) \to (F \underset{u}{⇝} (S) G \leftrightarrow ({F ↾}_{W}) \underset{u}{⇝} (S) G)$
40	39	ex	$⊢ φ \to ((S \in V \land G : S ⟶ ℂ) \to (F \underset{u}{⇝} (S) G \leftrightarrow ({F ↾}_{W}) \underset{u}{⇝} (S) G))$
41	8 12 40	pm5.21ndd	$⊢ φ \to (F \underset{u}{⇝} (S) G \leftrightarrow ({F ↾}_{W}) \underset{u}{⇝} (S) G)$

Metamath Proof Explorer

Theorem ulmres

Proof