ulmcau

Description: A sequence of functions converges uniformly iff it is uniformly Cauchy, which is to say that for every 0 < x there is a j such that for all j <_ k the functions F ( k ) and F ( j ) are uniformly within x of each other on S . This is the four-quantifier version, see ulmcau2 for the more conventional five-quantifier version. (Contributed by Mario Carneiro, 1-Mar-2015)

	Ref	Expression
Hypotheses	ulmcau.z	$⊢ Z = ℤ_{\geq M}$
	ulmcau.m	$⊢ φ \to M \in ℤ$
	ulmcau.s	$⊢ φ \to S \in V$
	ulmcau.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
Assertion	ulmcau	$⊢ φ \to (F \in dom \underset{u}{⇝} (S) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$

Proof

Step	Hyp	Ref	Expression
1		ulmcau.z	$⊢ Z = ℤ_{\geq M}$
2		ulmcau.m	$⊢ φ \to M \in ℤ$
3		ulmcau.s	$⊢ φ \to S \in V$
4		ulmcau.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
5		eldmg	$⊢ F \in dom \underset{u}{⇝} (S) \to (F \in dom \underset{u}{⇝} (S) \leftrightarrow \exists g F \underset{u}{⇝} (S) g)$
6	5	ibi	$⊢ F \in dom \underset{u}{⇝} (S) \to \exists g F \underset{u}{⇝} (S) g$
7	2	ad2antrr	$⊢ ((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \to M \in ℤ$
8	4	ad2antrr	$⊢ ((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \to F : Z ⟶ ℂ^{S}$
9		eqidd	$⊢ (((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land (k \in Z \land z \in S)) \to F (k) (z) = F (k) (z)$
10		eqidd	$⊢ (((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land z \in S) \to g (z) = g (z)$
11		simplr	$⊢ ((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \to F \underset{u}{⇝} (S) g$
12		rphalfcl	$⊢ x \in ℝ^{+} \to \frac{x}{2} \in ℝ^{+}$
13	12	adantl	$⊢ ((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \to \frac{x}{2} \in ℝ^{+}$
14	1 7 8 9 10 11 13	ulmi	$⊢ ((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - g (z)\| < \frac{x}{2}$
15		simpr	$⊢ (((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \to j \in Z$
16	15 1	eleqtrdi	$⊢ (((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \to j \in ℤ_{\geq M}$
17		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
18		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
19		fveq2	$⊢ k = j \to F (k) = F (j)$
20	19	fveq1d	$⊢ k = j \to F (k) (z) = F (j) (z)$
21	20	fvoveq1d	$⊢ k = j \to \|F (k) (z) - g (z)\| = \|F (j) (z) - g (z)\|$
22	21	breq1d	$⊢ k = j \to (\|F (k) (z) - g (z)\| < \frac{x}{2} \leftrightarrow \|F (j) (z) - g (z)\| < \frac{x}{2})$
23	22	ralbidv	$⊢ k = j \to (\forall z \in S \|F (k) (z) - g (z)\| < \frac{x}{2} \leftrightarrow \forall z \in S \|F (j) (z) - g (z)\| < \frac{x}{2})$
24	23	rspcv	$⊢ j \in ℤ_{\geq j} \to (\forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - g (z)\| < \frac{x}{2} \to \forall z \in S \|F (j) (z) - g (z)\| < \frac{x}{2})$
25	16 17 18 24	4syl	$⊢ (((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - g (z)\| < \frac{x}{2} \to \forall z \in S \|F (j) (z) - g (z)\| < \frac{x}{2})$
26		r19.26	$⊢ \forall z \in S (\|F (j) (z) - g (z)\| < \frac{x}{2} \land \|F (k) (z) - g (z)\| < \frac{x}{2}) \leftrightarrow (\forall z \in S \|F (j) (z) - g (z)\| < \frac{x}{2} \land \forall z \in S \|F (k) (z) - g (z)\| < \frac{x}{2})$
27	8	ffvelrnda	$⊢ (((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \to F (j) \in (ℂ^{S})$
28	27	adantr	$⊢ ((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to F (j) \in (ℂ^{S})$
29		elmapi	$⊢ F (j) \in (ℂ^{S}) \to F (j) : S ⟶ ℂ$
30	28 29	syl	$⊢ ((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to F (j) : S ⟶ ℂ$
31	30	ffvelrnda	$⊢ (((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land z \in S) \to F (j) (z) \in ℂ$
32		ulmcl	$⊢ F \underset{u}{⇝} (S) g \to g : S ⟶ ℂ$
33	32	ad4antlr	$⊢ ((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to g : S ⟶ ℂ$
34	33	ffvelrnda	$⊢ (((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land z \in S) \to g (z) \in ℂ$
35	31 34	abssubd	$⊢ (((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land z \in S) \to \|F (j) (z) - g (z)\| = \|g (z) - F (j) (z)\|$
36	35	breq1d	$⊢ (((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land z \in S) \to (\|F (j) (z) - g (z)\| < \frac{x}{2} \leftrightarrow \|g (z) - F (j) (z)\| < \frac{x}{2})$
37	36	biimpd	$⊢ (((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land z \in S) \to (\|F (j) (z) - g (z)\| < \frac{x}{2} \to \|g (z) - F (j) (z)\| < \frac{x}{2})$
38	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
39		ffvelrn	$⊢ (F : Z ⟶ ℂ^{S} \land k \in Z) \to F (k) \in (ℂ^{S})$
40	8 38 39	syl2an	$⊢ (((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to F (k) \in (ℂ^{S})$
41	40	anassrs	$⊢ ((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) \in (ℂ^{S})$
42		elmapi	$⊢ F (k) \in (ℂ^{S}) \to F (k) : S ⟶ ℂ$
43	41 42	syl	$⊢ ((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) : S ⟶ ℂ$
44	43	ffvelrnda	$⊢ (((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land z \in S) \to F (k) (z) \in ℂ$
45		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
46	45	ad4antlr	$⊢ (((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land z \in S) \to x \in ℝ$
47		abs3lem	$⊢ ((F (k) (z) \in ℂ \land F (j) (z) \in ℂ) \land (g (z) \in ℂ \land x \in ℝ)) \to ((\|F (k) (z) - g (z)\| < \frac{x}{2} \land \|g (z) - F (j) (z)\| < \frac{x}{2}) \to \|F (k) (z) - F (j) (z)\| < x)$
48	44 31 34 46 47	syl22anc	$⊢ (((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land z \in S) \to ((\|F (k) (z) - g (z)\| < \frac{x}{2} \land \|g (z) - F (j) (z)\| < \frac{x}{2}) \to \|F (k) (z) - F (j) (z)\| < x)$
49	37 48	sylan2d	$⊢ (((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land z \in S) \to ((\|F (k) (z) - g (z)\| < \frac{x}{2} \land \|F (j) (z) - g (z)\| < \frac{x}{2}) \to \|F (k) (z) - F (j) (z)\| < x)$
50	49	ancomsd	$⊢ (((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land z \in S) \to ((\|F (j) (z) - g (z)\| < \frac{x}{2} \land \|F (k) (z) - g (z)\| < \frac{x}{2}) \to \|F (k) (z) - F (j) (z)\| < x)$
51	50	ralimdva	$⊢ ((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to (\forall z \in S (\|F (j) (z) - g (z)\| < \frac{x}{2} \land \|F (k) (z) - g (z)\| < \frac{x}{2}) \to \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
52	26 51	syl5bir	$⊢ ((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to ((\forall z \in S \|F (j) (z) - g (z)\| < \frac{x}{2} \land \forall z \in S \|F (k) (z) - g (z)\| < \frac{x}{2}) \to \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
53	52	expdimp	$⊢ (((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land \forall z \in S \|F (j) (z) - g (z)\| < \frac{x}{2}) \to (\forall z \in S \|F (k) (z) - g (z)\| < \frac{x}{2} \to \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
54	53	an32s	$⊢ (((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land \forall z \in S \|F (j) (z) - g (z)\| < \frac{x}{2}) \land k \in ℤ_{\geq j}) \to (\forall z \in S \|F (k) (z) - g (z)\| < \frac{x}{2} \to \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
55	54	ralimdva	$⊢ ((((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \land \forall z \in S \|F (j) (z) - g (z)\| < \frac{x}{2}) \to (\forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - g (z)\| < \frac{x}{2} \to \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
56	55	ex	$⊢ (((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \to (\forall z \in S \|F (j) (z) - g (z)\| < \frac{x}{2} \to (\forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - g (z)\| < \frac{x}{2} \to \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x))$
57	56	com23	$⊢ (((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - g (z)\| < \frac{x}{2} \to (\forall z \in S \|F (j) (z) - g (z)\| < \frac{x}{2} \to \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x))$
58	25 57	mpdd	$⊢ (((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - g (z)\| < \frac{x}{2} \to \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
59	58	reximdva	$⊢ ((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \to (\exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - g (z)\| < \frac{x}{2} \to \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
60	14 59	mpd	$⊢ ((φ \land F \underset{u}{⇝} (S) g) \land x \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x$
61	60	ralrimiva	$⊢ (φ \land F \underset{u}{⇝} (S) g) \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x$
62	61	ex	$⊢ φ \to (F \underset{u}{⇝} (S) g \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
63	62	exlimdv	$⊢ φ \to (\exists g F \underset{u}{⇝} (S) g \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
64	6 63	syl5	$⊢ φ \to (F \in dom \underset{u}{⇝} (S) \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
65		ulmrel	$⊢ Rel \underset{u}{⇝} (S)$
66	1 2 3 4	ulmcaulem	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$
67	66	biimpa	$⊢ (φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x$
68		rphalfcl	$⊢ r \in ℝ^{+} \to \frac{r}{2} \in ℝ^{+}$
69		breq2	$⊢ x = \frac{r}{2} \to (\|F (k) (z) - F (m) (z)\| < x \leftrightarrow \|F (k) (z) - F (m) (z)\| < \frac{r}{2})$
70	69	ralbidv	$⊢ x = \frac{r}{2} \to (\forall z \in S \|F (k) (z) - F (m) (z)\| < x \leftrightarrow \forall z \in S \|F (k) (z) - F (m) (z)\| < \frac{r}{2})$
71	70	2ralbidv	$⊢ x = \frac{r}{2} \to (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x \leftrightarrow \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < \frac{r}{2})$
72	71	rexbidv	$⊢ x = \frac{r}{2} \to (\exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < \frac{r}{2})$
73		ralcom	$⊢ \forall w \in S \forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \leftrightarrow \forall m \in ℤ_{\geq q} \forall w \in S \|F (q) (w) - F (m) (w)\| < \frac{r}{2}$
74		fveq2	$⊢ q = k \to ℤ_{\geq q} = ℤ_{\geq k}$
75		fveq2	$⊢ w = z \to F (q) (w) = F (q) (z)$
76		fveq2	$⊢ w = z \to F (m) (w) = F (m) (z)$
77	75 76	oveq12d	$⊢ w = z \to F (q) (w) - F (m) (w) = F (q) (z) - F (m) (z)$
78	77	fveq2d	$⊢ w = z \to \|F (q) (w) - F (m) (w)\| = \|F (q) (z) - F (m) (z)\|$
79	78	breq1d	$⊢ w = z \to (\|F (q) (w) - F (m) (w)\| < \frac{r}{2} \leftrightarrow \|F (q) (z) - F (m) (z)\| < \frac{r}{2})$
80	79	cbvralvw	$⊢ \forall w \in S \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \leftrightarrow \forall z \in S \|F (q) (z) - F (m) (z)\| < \frac{r}{2}$
81		fveq2	$⊢ q = k \to F (q) = F (k)$
82	81	fveq1d	$⊢ q = k \to F (q) (z) = F (k) (z)$
83	82	fvoveq1d	$⊢ q = k \to \|F (q) (z) - F (m) (z)\| = \|F (k) (z) - F (m) (z)\|$
84	83	breq1d	$⊢ q = k \to (\|F (q) (z) - F (m) (z)\| < \frac{r}{2} \leftrightarrow \|F (k) (z) - F (m) (z)\| < \frac{r}{2})$
85	84	ralbidv	$⊢ q = k \to (\forall z \in S \|F (q) (z) - F (m) (z)\| < \frac{r}{2} \leftrightarrow \forall z \in S \|F (k) (z) - F (m) (z)\| < \frac{r}{2})$
86	80 85	syl5bb	$⊢ q = k \to (\forall w \in S \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \leftrightarrow \forall z \in S \|F (k) (z) - F (m) (z)\| < \frac{r}{2})$
87	74 86	raleqbidv	$⊢ q = k \to (\forall m \in ℤ_{\geq q} \forall w \in S \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \leftrightarrow \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < \frac{r}{2})$
88	73 87	syl5bb	$⊢ q = k \to (\forall w \in S \forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \leftrightarrow \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < \frac{r}{2})$
89	88	cbvralvw	$⊢ \forall q \in ℤ_{\geq p} \forall w \in S \forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \leftrightarrow \forall k \in ℤ_{\geq p} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < \frac{r}{2}$
90		fveq2	$⊢ p = j \to ℤ_{\geq p} = ℤ_{\geq j}$
91	90	raleqdv	$⊢ p = j \to (\forall k \in ℤ_{\geq p} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < \frac{r}{2} \leftrightarrow \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < \frac{r}{2})$
92	89 91	syl5bb	$⊢ p = j \to (\forall q \in ℤ_{\geq p} \forall w \in S \forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \leftrightarrow \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < \frac{r}{2})$
93	92	cbvrexvw	$⊢ \exists p \in Z \forall q \in ℤ_{\geq p} \forall w \in S \forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < \frac{r}{2}$
94	72 93	syl6bbr	$⊢ x = \frac{r}{2} \to (\exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x \leftrightarrow \exists p \in Z \forall q \in ℤ_{\geq p} \forall w \in S \forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2})$
95	94	rspccva	$⊢ (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x \land \frac{r}{2} \in ℝ^{+}) \to \exists p \in Z \forall q \in ℤ_{\geq p} \forall w \in S \forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2}$
96	67 68 95	syl2an	$⊢ ((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \to \exists p \in Z \forall q \in ℤ_{\geq p} \forall w \in S \forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2}$
97	1	uztrn2	$⊢ (p \in Z \land q \in ℤ_{\geq p}) \to q \in Z$
98		eqid	$⊢ ℤ_{\geq q} = ℤ_{\geq q}$
99		eluzelz	$⊢ q \in ℤ_{\geq M} \to q \in ℤ$
100	99 1	eleq2s	$⊢ q \in Z \to q \in ℤ$
101	100	ad2antlr	$⊢ ((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \to q \in ℤ$
102	68	adantl	$⊢ ((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \to \frac{r}{2} \in ℝ^{+}$
103	102	ad2antrr	$⊢ ((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \to \frac{r}{2} \in ℝ^{+}$
104		simplr	$⊢ ((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \to q \in Z$
105	1	uztrn2	$⊢ (q \in Z \land m \in ℤ_{\geq q}) \to m \in Z$
106	104 105	sylan	$⊢ (((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \land m \in ℤ_{\geq q}) \to m \in Z$
107		fveq2	$⊢ n = m \to F (n) = F (m)$
108	107	fveq1d	$⊢ n = m \to F (n) (w) = F (m) (w)$
109		eqid	$⊢ (n \in Z ⟼ F (n) (w)) = (n \in Z ⟼ F (n) (w))$
110		fvex	$⊢ F (m) (w) \in V$
111	108 109 110	fvmpt	$⊢ m \in Z \to (n \in Z ⟼ F (n) (w)) (m) = F (m) (w)$
112	106 111	syl	$⊢ (((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \land m \in ℤ_{\geq q}) \to (n \in Z ⟼ F (n) (w)) (m) = F (m) (w)$
113	4	adantr	$⊢ (φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \to F : Z ⟶ ℂ^{S}$
114	113	ffvelrnda	$⊢ ((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land n \in Z) \to F (n) \in (ℂ^{S})$
115		elmapi	$⊢ F (n) \in (ℂ^{S}) \to F (n) : S ⟶ ℂ$
116	114 115	syl	$⊢ ((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land n \in Z) \to F (n) : S ⟶ ℂ$
117	116	ffvelrnda	$⊢ (((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land n \in Z) \land y \in S) \to F (n) (y) \in ℂ$
118	117	an32s	$⊢ (((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land y \in S) \land n \in Z) \to F (n) (y) \in ℂ$
119	118	fmpttd	$⊢ ((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land y \in S) \to (n \in Z ⟼ F (n) (y)) : Z ⟶ ℂ$
120	119	ffvelrnda	$⊢ (((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land y \in S) \land q \in Z) \to (n \in Z ⟼ F (n) (y)) (q) \in ℂ$
121		fveq2	$⊢ z = y \to F (k) (z) = F (k) (y)$
122		fveq2	$⊢ z = y \to F (j) (z) = F (j) (y)$
123	121 122	oveq12d	$⊢ z = y \to F (k) (z) - F (j) (z) = F (k) (y) - F (j) (y)$
124	123	fveq2d	$⊢ z = y \to \|F (k) (z) - F (j) (z)\| = \|F (k) (y) - F (j) (y)\|$
125	124	breq1d	$⊢ z = y \to (\|F (k) (z) - F (j) (z)\| < x \leftrightarrow \|F (k) (y) - F (j) (y)\| < x)$
126	125	rspcv	$⊢ y \in S \to (\forall z \in S \|F (k) (z) - F (j) (z)\| < x \to \|F (k) (y) - F (j) (y)\| < x)$
127	126	ralimdv	$⊢ y \in S \to (\forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x \to \forall k \in ℤ_{\geq j} \|F (k) (y) - F (j) (y)\| < x)$
128	127	reximdv	$⊢ y \in S \to (\exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) (y) - F (j) (y)\| < x)$
129	128	ralimdv	$⊢ y \in S \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) (y) - F (j) (y)\| < x)$
130	129	impcom	$⊢ (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x \land y \in S) \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) (y) - F (j) (y)\| < x$
131	130	adantll	$⊢ ((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land y \in S) \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) (y) - F (j) (y)\| < x$
132		fveq2	$⊢ q = k \to (n \in Z ⟼ F (n) (y)) (q) = (n \in Z ⟼ F (n) (y)) (k)$
133	132	fvoveq1d	$⊢ q = k \to \|(n \in Z ⟼ F (n) (y)) (q) - (n \in Z ⟼ F (n) (y)) (p)\| = \|(n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (p)\|$
134	133	breq1d	$⊢ q = k \to (\|(n \in Z ⟼ F (n) (y)) (q) - (n \in Z ⟼ F (n) (y)) (p)\| < r \leftrightarrow \|(n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (p)\| < r)$
135	134	cbvralvw	$⊢ \forall q \in ℤ_{\geq p} \|(n \in Z ⟼ F (n) (y)) (q) - (n \in Z ⟼ F (n) (y)) (p)\| < r \leftrightarrow \forall k \in ℤ_{\geq p} \|(n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (p)\| < r$
136		fveq2	$⊢ p = j \to (n \in Z ⟼ F (n) (y)) (p) = (n \in Z ⟼ F (n) (y)) (j)$
137	136	oveq2d	$⊢ p = j \to (n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (p) = (n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (j)$
138	137	fveq2d	$⊢ p = j \to \|(n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (p)\| = \|(n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (j)\|$
139	138	breq1d	$⊢ p = j \to (\|(n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (p)\| < r \leftrightarrow \|(n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (j)\| < r)$
140	90 139	raleqbidv	$⊢ p = j \to (\forall k \in ℤ_{\geq p} \|(n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (p)\| < r \leftrightarrow \forall k \in ℤ_{\geq j} \|(n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (j)\| < r)$
141	135 140	syl5bb	$⊢ p = j \to (\forall q \in ℤ_{\geq p} \|(n \in Z ⟼ F (n) (y)) (q) - (n \in Z ⟼ F (n) (y)) (p)\| < r \leftrightarrow \forall k \in ℤ_{\geq j} \|(n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (j)\| < r)$
142	141	cbvrexvw	$⊢ \exists p \in Z \forall q \in ℤ_{\geq p} \|(n \in Z ⟼ F (n) (y)) (q) - (n \in Z ⟼ F (n) (y)) (p)\| < r \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} \|(n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (j)\| < r$
143		fveq2	$⊢ n = k \to F (n) = F (k)$
144	143	fveq1d	$⊢ n = k \to F (n) (y) = F (k) (y)$
145		eqid	$⊢ (n \in Z ⟼ F (n) (y)) = (n \in Z ⟼ F (n) (y))$
146		fvex	$⊢ F (k) (y) \in V$
147	144 145 146	fvmpt	$⊢ k \in Z \to (n \in Z ⟼ F (n) (y)) (k) = F (k) (y)$
148	38 147	syl	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to (n \in Z ⟼ F (n) (y)) (k) = F (k) (y)$
149		fveq2	$⊢ n = j \to F (n) = F (j)$
150	149	fveq1d	$⊢ n = j \to F (n) (y) = F (j) (y)$
151		fvex	$⊢ F (j) (y) \in V$
152	150 145 151	fvmpt	$⊢ j \in Z \to (n \in Z ⟼ F (n) (y)) (j) = F (j) (y)$
153	152	adantr	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to (n \in Z ⟼ F (n) (y)) (j) = F (j) (y)$
154	148 153	oveq12d	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to (n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (j) = F (k) (y) - F (j) (y)$
155	154	fveq2d	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to \|(n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (j)\| = \|F (k) (y) - F (j) (y)\|$
156	155	breq1d	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to (\|(n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (j)\| < r \leftrightarrow \|F (k) (y) - F (j) (y)\| < r)$
157	156	ralbidva	$⊢ j \in Z \to (\forall k \in ℤ_{\geq j} \|(n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (j)\| < r \leftrightarrow \forall k \in ℤ_{\geq j} \|F (k) (y) - F (j) (y)\| < r)$
158	157	rexbiia	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} \|(n \in Z ⟼ F (n) (y)) (k) - (n \in Z ⟼ F (n) (y)) (j)\| < r \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) (y) - F (j) (y)\| < r$
159	142 158	bitri	$⊢ \exists p \in Z \forall q \in ℤ_{\geq p} \|(n \in Z ⟼ F (n) (y)) (q) - (n \in Z ⟼ F (n) (y)) (p)\| < r \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) (y) - F (j) (y)\| < r$
160		breq2	$⊢ r = x \to (\|F (k) (y) - F (j) (y)\| < r \leftrightarrow \|F (k) (y) - F (j) (y)\| < x)$
161	160	ralbidv	$⊢ r = x \to (\forall k \in ℤ_{\geq j} \|F (k) (y) - F (j) (y)\| < r \leftrightarrow \forall k \in ℤ_{\geq j} \|F (k) (y) - F (j) (y)\| < x)$
162	161	rexbidv	$⊢ r = x \to (\exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) (y) - F (j) (y)\| < r \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) (y) - F (j) (y)\| < x)$
163	159 162	syl5bb	$⊢ r = x \to (\exists p \in Z \forall q \in ℤ_{\geq p} \|(n \in Z ⟼ F (n) (y)) (q) - (n \in Z ⟼ F (n) (y)) (p)\| < r \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) (y) - F (j) (y)\| < x)$
164	163	cbvralvw	$⊢ \forall r \in ℝ^{+} \exists p \in Z \forall q \in ℤ_{\geq p} \|(n \in Z ⟼ F (n) (y)) (q) - (n \in Z ⟼ F (n) (y)) (p)\| < r \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) (y) - F (j) (y)\| < x$
165	131 164	sylibr	$⊢ ((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land y \in S) \to \forall r \in ℝ^{+} \exists p \in Z \forall q \in ℤ_{\geq p} \|(n \in Z ⟼ F (n) (y)) (q) - (n \in Z ⟼ F (n) (y)) (p)\| < r$
166	1	fvexi	$⊢ Z \in V$
167	166	mptex	$⊢ (n \in Z ⟼ F (n) (y)) \in V$
168	167	a1i	$⊢ ((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land y \in S) \to (n \in Z ⟼ F (n) (y)) \in V$
169	1 120 165 168	caucvg	$⊢ ((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land y \in S) \to (n \in Z ⟼ F (n) (y)) \in dom ⇝$
170	169	ralrimiva	$⊢ (φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \to \forall y \in S (n \in Z ⟼ F (n) (y)) \in dom ⇝$
171	170	ad2antrr	$⊢ (((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \to \forall y \in S (n \in Z ⟼ F (n) (y)) \in dom ⇝$
172		fveq2	$⊢ y = w \to F (n) (y) = F (n) (w)$
173	172	mpteq2dv	$⊢ y = w \to (n \in Z ⟼ F (n) (y)) = (n \in Z ⟼ F (n) (w))$
174	173	eleq1d	$⊢ y = w \to ((n \in Z ⟼ F (n) (y)) \in dom ⇝ \leftrightarrow (n \in Z ⟼ F (n) (w)) \in dom ⇝)$
175	174	rspccva	$⊢ (\forall y \in S (n \in Z ⟼ F (n) (y)) \in dom ⇝ \land w \in S) \to (n \in Z ⟼ F (n) (w)) \in dom ⇝$
176	171 175	sylan	$⊢ ((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \to (n \in Z ⟼ F (n) (w)) \in dom ⇝$
177		climdm	$⊢ (n \in Z ⟼ F (n) (w)) \in dom ⇝ \leftrightarrow (n \in Z ⟼ F (n) (w)) ⇝ ⇝ ((n \in Z ⟼ F (n) (w)))$
178	176 177	sylib	$⊢ ((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \to (n \in Z ⟼ F (n) (w)) ⇝ ⇝ ((n \in Z ⟼ F (n) (w)))$
179	98 101 103 112 178	climi2	$⊢ ((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \to \exists v \in ℤ_{\geq q} \forall m \in ℤ_{\geq v} \|F (m) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < \frac{r}{2}$
180	98	r19.29uz	$⊢ (\forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \land \exists v \in ℤ_{\geq q} \forall m \in ℤ_{\geq v} \|F (m) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < \frac{r}{2}) \to \exists v \in ℤ_{\geq q} \forall m \in ℤ_{\geq v} (\|F (q) (w) - F (m) (w)\| < \frac{r}{2} \land \|F (m) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < \frac{r}{2})$
181	98	r19.2uz	$⊢ \exists v \in ℤ_{\geq q} \forall m \in ℤ_{\geq v} (\|F (q) (w) - F (m) (w)\| < \frac{r}{2} \land \|F (m) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < \frac{r}{2}) \to \exists m \in ℤ_{\geq q} (\|F (q) (w) - F (m) (w)\| < \frac{r}{2} \land \|F (m) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < \frac{r}{2})$
182	180 181	syl	$⊢ (\forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \land \exists v \in ℤ_{\geq q} \forall m \in ℤ_{\geq v} \|F (m) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < \frac{r}{2}) \to \exists m \in ℤ_{\geq q} (\|F (q) (w) - F (m) (w)\| < \frac{r}{2} \land \|F (m) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < \frac{r}{2})$
183	4	ad2antrr	$⊢ ((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \to F : Z ⟶ ℂ^{S}$
184	183	ffvelrnda	$⊢ (((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \to F (q) \in (ℂ^{S})$
185		elmapi	$⊢ F (q) \in (ℂ^{S}) \to F (q) : S ⟶ ℂ$
186	184 185	syl	$⊢ (((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \to F (q) : S ⟶ ℂ$
187	186	ffvelrnda	$⊢ ((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \to F (q) (w) \in ℂ$
188	187	adantr	$⊢ (((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \land m \in ℤ_{\geq q}) \to F (q) (w) \in ℂ$
189		climcl	$⊢ (n \in Z ⟼ F (n) (w)) ⇝ ⇝ ((n \in Z ⟼ F (n) (w))) \to ⇝ ((n \in Z ⟼ F (n) (w))) \in ℂ$
190	178 189	syl	$⊢ ((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \to ⇝ ((n \in Z ⟼ F (n) (w))) \in ℂ$
191	190	adantr	$⊢ (((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \land m \in ℤ_{\geq q}) \to ⇝ ((n \in Z ⟼ F (n) (w))) \in ℂ$
192	4	ad5antr	$⊢ (((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \land m \in ℤ_{\geq q}) \to F : Z ⟶ ℂ^{S}$
193	192 106	ffvelrnd	$⊢ (((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \land m \in ℤ_{\geq q}) \to F (m) \in (ℂ^{S})$
194		elmapi	$⊢ F (m) \in (ℂ^{S}) \to F (m) : S ⟶ ℂ$
195	193 194	syl	$⊢ (((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \land m \in ℤ_{\geq q}) \to F (m) : S ⟶ ℂ$
196		simplr	$⊢ (((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \land m \in ℤ_{\geq q}) \to w \in S$
197	195 196	ffvelrnd	$⊢ (((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \land m \in ℤ_{\geq q}) \to F (m) (w) \in ℂ$
198		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
199	198	ad4antlr	$⊢ (((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \land m \in ℤ_{\geq q}) \to r \in ℝ$
200		abs3lem	$⊢ ((F (q) (w) \in ℂ \land ⇝ ((n \in Z ⟼ F (n) (w))) \in ℂ) \land (F (m) (w) \in ℂ \land r \in ℝ)) \to ((\|F (q) (w) - F (m) (w)\| < \frac{r}{2} \land \|F (m) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < \frac{r}{2}) \to \|F (q) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < r)$
201	188 191 197 199 200	syl22anc	$⊢ (((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \land m \in ℤ_{\geq q}) \to ((\|F (q) (w) - F (m) (w)\| < \frac{r}{2} \land \|F (m) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < \frac{r}{2}) \to \|F (q) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < r)$
202	201	rexlimdva	$⊢ ((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \to (\exists m \in ℤ_{\geq q} (\|F (q) (w) - F (m) (w)\| < \frac{r}{2} \land \|F (m) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < \frac{r}{2}) \to \|F (q) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < r)$
203	182 202	syl5	$⊢ ((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \to ((\forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \land \exists v \in ℤ_{\geq q} \forall m \in ℤ_{\geq v} \|F (m) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < \frac{r}{2}) \to \|F (q) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < r)$
204	179 203	mpan2d	$⊢ ((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \land w \in S) \to (\forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \to \|F (q) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < r)$
205	204	ralimdva	$⊢ (((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land q \in Z) \to (\forall w \in S \forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \to \forall w \in S \|F (q) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < r)$
206	97 205	sylan2	$⊢ (((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land (p \in Z \land q \in ℤ_{\geq p})) \to (\forall w \in S \forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \to \forall w \in S \|F (q) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < r)$
207	206	anassrs	$⊢ ((((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land p \in Z) \land q \in ℤ_{\geq p}) \to (\forall w \in S \forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \to \forall w \in S \|F (q) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < r)$
208	207	ralimdva	$⊢ (((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \land p \in Z) \to (\forall q \in ℤ_{\geq p} \forall w \in S \forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \to \forall q \in ℤ_{\geq p} \forall w \in S \|F (q) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < r)$
209	208	reximdva	$⊢ ((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \to (\exists p \in Z \forall q \in ℤ_{\geq p} \forall w \in S \forall m \in ℤ_{\geq q} \|F (q) (w) - F (m) (w)\| < \frac{r}{2} \to \exists p \in Z \forall q \in ℤ_{\geq p} \forall w \in S \|F (q) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < r)$
210	96 209	mpd	$⊢ ((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land r \in ℝ^{+}) \to \exists p \in Z \forall q \in ℤ_{\geq p} \forall w \in S \|F (q) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < r$
211	210	ralrimiva	$⊢ (φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \to \forall r \in ℝ^{+} \exists p \in Z \forall q \in ℤ_{\geq p} \forall w \in S \|F (q) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < r$
212	2	adantr	$⊢ (φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \to M \in ℤ$
213		eqidd	$⊢ ((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land (q \in Z \land w \in S)) \to F (q) (w) = F (q) (w)$
214	173	fveq2d	$⊢ y = w \to ⇝ ((n \in Z ⟼ F (n) (y))) = ⇝ ((n \in Z ⟼ F (n) (w)))$
215		eqid	$⊢ (y \in S ⟼ ⇝ ((n \in Z ⟼ F (n) (y)))) = (y \in S ⟼ ⇝ ((n \in Z ⟼ F (n) (y))))$
216		fvex	$⊢ ⇝ ((n \in Z ⟼ F (n) (w))) \in V$
217	214 215 216	fvmpt	$⊢ w \in S \to (y \in S ⟼ ⇝ ((n \in Z ⟼ F (n) (y)))) (w) = ⇝ ((n \in Z ⟼ F (n) (w)))$
218	217	adantl	$⊢ ((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land w \in S) \to (y \in S ⟼ ⇝ ((n \in Z ⟼ F (n) (y)))) (w) = ⇝ ((n \in Z ⟼ F (n) (w)))$
219		climdm	$⊢ (n \in Z ⟼ F (n) (y)) \in dom ⇝ \leftrightarrow (n \in Z ⟼ F (n) (y)) ⇝ ⇝ ((n \in Z ⟼ F (n) (y)))$
220	169 219	sylib	$⊢ ((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land y \in S) \to (n \in Z ⟼ F (n) (y)) ⇝ ⇝ ((n \in Z ⟼ F (n) (y)))$
221		climcl	$⊢ (n \in Z ⟼ F (n) (y)) ⇝ ⇝ ((n \in Z ⟼ F (n) (y))) \to ⇝ ((n \in Z ⟼ F (n) (y))) \in ℂ$
222	220 221	syl	$⊢ ((φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \land y \in S) \to ⇝ ((n \in Z ⟼ F (n) (y))) \in ℂ$
223	222	fmpttd	$⊢ (φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \to (y \in S ⟼ ⇝ ((n \in Z ⟼ F (n) (y)))) : S ⟶ ℂ$
224	3	adantr	$⊢ (φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \to S \in V$
225	1 212 113 213 218 223 224	ulm2	$⊢ (φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \to (F \underset{u}{⇝} (S) (y \in S ⟼ ⇝ ((n \in Z ⟼ F (n) (y)))) \leftrightarrow \forall r \in ℝ^{+} \exists p \in Z \forall q \in ℤ_{\geq p} \forall w \in S \|F (q) (w) - ⇝ ((n \in Z ⟼ F (n) (w)))\| < r)$
226	211 225	mpbird	$⊢ (φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \to F \underset{u}{⇝} (S) (y \in S ⟼ ⇝ ((n \in Z ⟼ F (n) (y))))$
227		releldm	$⊢ (Rel \underset{u}{⇝} (S) \land F \underset{u}{⇝} (S) (y \in S ⟼ ⇝ ((n \in Z ⟼ F (n) (y))))) \to F \in dom \underset{u}{⇝} (S)$
228	65 226 227	sylancr	$⊢ (φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x) \to F \in dom \underset{u}{⇝} (S)$
229	228	ex	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x \to F \in dom \underset{u}{⇝} (S))$
230	64 229	impbid	$⊢ φ \to (F \in dom \underset{u}{⇝} (S) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$

Metamath Proof Explorer

Theorem ulmcau

Proof