ulmdvlem3

	Ref	Expression
Hypotheses	ulmdv.z	$⊢ Z = ℤ_{\geq M}$
	ulmdv.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
	ulmdv.m	$⊢ φ \to M \in ℤ$
	ulmdv.f	$⊢ φ \to F : Z ⟶ ℂ^{X}$
	ulmdv.g	$⊢ φ \to G : X ⟶ ℂ$
	ulmdv.l	$⊢ (φ \land z \in X) \to (k \in Z ⟼ F (k) (z)) ⇝ G (z)$
	ulmdv.u	$⊢ φ \to (k \in Z ⟼ S D F (k)) \underset{u}{⇝} (X) H$
Assertion	ulmdvlem3	$⊢ (φ \land z \in X) \to z G_{S}^{'} H (z)$

Proof

Step	Hyp	Ref	Expression
1		ulmdv.z	$⊢ Z = ℤ_{\geq M}$
2		ulmdv.s	$⊢ φ \to S \in \{ℝ, ℂ\}$
3		ulmdv.m	$⊢ φ \to M \in ℤ$
4		ulmdv.f	$⊢ φ \to F : Z ⟶ ℂ^{X}$
5		ulmdv.g	$⊢ φ \to G : X ⟶ ℂ$
6		ulmdv.l	$⊢ (φ \land z \in X) \to (k \in Z ⟼ F (k) (z)) ⇝ G (z)$
7		ulmdv.u	$⊢ φ \to (k \in Z ⟼ S D F (k)) \underset{u}{⇝} (X) H$
8		biidd	$⊢ k = M \to (X \subseteq int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X) \leftrightarrow X \subseteq int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X))$
9	1 2 3 4 5 6 7	ulmdvlem2	$⊢ (φ \land k \in Z) \to dom {F (k)}_{S}^{'} = X$
10		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
11	2 10	syl	$⊢ φ \to S \subseteq ℂ$
12	11	adantr	$⊢ (φ \land k \in Z) \to S \subseteq ℂ$
13	4	ffvelcdmda	$⊢ (φ \land k \in Z) \to F (k) \in (ℂ^{X})$
14		elmapi	$⊢ F (k) \in (ℂ^{X}) \to F (k) : X ⟶ ℂ$
15	13 14	syl	$⊢ (φ \land k \in Z) \to F (k) : X ⟶ ℂ$
16		dvbsss	$⊢ dom {F (k)}_{S}^{'} \subseteq S$
17	9 16	eqsstrrdi	$⊢ (φ \land k \in Z) \to X \subseteq S$
18		eqid	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S = TopOpen (ℂ_{fld}) ↾_{𝑡} S$
19		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
20	12 15 17 18 19	dvbssntr	$⊢ (φ \land k \in Z) \to dom {F (k)}_{S}^{'} \subseteq int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X)$
21	9 20	eqsstrrd	$⊢ (φ \land k \in Z) \to X \subseteq int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X)$
22	21	ralrimiva	$⊢ φ \to \forall k \in Z X \subseteq int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X)$
23		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
24	3 23	syl	$⊢ φ \to M \in ℤ_{\geq M}$
25	24 1	eleqtrrdi	$⊢ φ \to M \in Z$
26	8 22 25	rspcdva	$⊢ φ \to X \subseteq int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X)$
27	26	sselda	$⊢ (φ \land z \in X) \to z \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X)$
28		ulmcl	$⊢ (k \in Z ⟼ S D F (k)) \underset{u}{⇝} (X) H \to H : X ⟶ ℂ$
29	7 28	syl	$⊢ φ \to H : X ⟶ ℂ$
30	29	ffvelcdmda	$⊢ (φ \land z \in X) \to H (z) \in ℂ$
31		breq2	$⊢ s = \frac{\frac{r}{2}}{2} \to (\|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < s \leftrightarrow \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2})$
32	31	2ralbidv	$⊢ s = \frac{\frac{r}{2}}{2} \to (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < s \leftrightarrow \forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2})$
33	32	rexralbidv	$⊢ s = \frac{\frac{r}{2}}{2} \to (\exists j \in Z \forall n \in ℤ_{\geq j} \forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < s \leftrightarrow \exists j \in Z \forall n \in ℤ_{\geq j} \forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2})$
34		ulmrel	$⊢ Rel \underset{u}{⇝} (X)$
35		releldm	$⊢ (Rel \underset{u}{⇝} (X) \land (k \in Z ⟼ S D F (k)) \underset{u}{⇝} (X) H) \to (k \in Z ⟼ S D F (k)) \in dom \underset{u}{⇝} (X)$
36	34 7 35	sylancr	$⊢ φ \to (k \in Z ⟼ S D F (k)) \in dom \underset{u}{⇝} (X)$
37		ulmscl	$⊢ (k \in Z ⟼ S D F (k)) \underset{u}{⇝} (X) H \to X \in V$
38	7 37	syl	$⊢ φ \to X \in V$
39		ovex	$⊢ S D F (k) \in V$
40	39	rgenw	$⊢ \forall k \in Z S D F (k) \in V$
41		eqid	$⊢ (k \in Z ⟼ S D F (k)) = (k \in Z ⟼ S D F (k))$
42	41	fnmpt	$⊢ \forall k \in Z S D F (k) \in V \to (k \in Z ⟼ S D F (k)) Fn Z$
43	40 42	mp1i	$⊢ φ \to (k \in Z ⟼ S D F (k)) Fn Z$
44		ulmf2	$⊢ ((k \in Z ⟼ S D F (k)) Fn Z \land (k \in Z ⟼ S D F (k)) \underset{u}{⇝} (X) H) \to (k \in Z ⟼ S D F (k)) : Z ⟶ ℂ^{X}$
45	43 7 44	syl2anc	$⊢ φ \to (k \in Z ⟼ S D F (k)) : Z ⟶ ℂ^{X}$
46	1 3 38 45	ulmcau2	$⊢ φ \to ((k \in Z ⟼ S D F (k)) \in dom \underset{u}{⇝} (X) \leftrightarrow \forall s \in ℝ^{+} \exists j \in Z \forall n \in ℤ_{\geq j} \forall m \in ℤ_{\geq n} \forall x \in X \|(k \in Z ⟼ S D F (k)) (n) (x) - (k \in Z ⟼ S D F (k)) (m) (x)\| < s)$
47	36 46	mpbid	$⊢ φ \to \forall s \in ℝ^{+} \exists j \in Z \forall n \in ℤ_{\geq j} \forall m \in ℤ_{\geq n} \forall x \in X \|(k \in Z ⟼ S D F (k)) (n) (x) - (k \in Z ⟼ S D F (k)) (m) (x)\| < s$
48	1	uztrn2	$⊢ (j \in Z \land n \in ℤ_{\geq j}) \to n \in Z$
49	48	ad2ant2lr	$⊢ ((φ \land j \in Z) \land (n \in ℤ_{\geq j} \land m \in ℤ_{\geq n})) \to n \in Z$
50		fveq2	$⊢ k = n \to F (k) = F (n)$
51	50	oveq2d	$⊢ k = n \to S D F (k) = S D F (n)$
52		ovex	$⊢ S D F (n) \in V$
53	51 41 52	fvmpt	$⊢ n \in Z \to (k \in Z ⟼ S D F (k)) (n) = S D F (n)$
54	49 53	syl	$⊢ ((φ \land j \in Z) \land (n \in ℤ_{\geq j} \land m \in ℤ_{\geq n})) \to (k \in Z ⟼ S D F (k)) (n) = S D F (n)$
55	54	fveq1d	$⊢ ((φ \land j \in Z) \land (n \in ℤ_{\geq j} \land m \in ℤ_{\geq n})) \to (k \in Z ⟼ S D F (k)) (n) (x) = {F (n)}_{S}^{'} (x)$
56		simprr	$⊢ ((φ \land j \in Z) \land (n \in ℤ_{\geq j} \land m \in ℤ_{\geq n})) \to m \in ℤ_{\geq n}$
57	1	uztrn2	$⊢ (n \in Z \land m \in ℤ_{\geq n}) \to m \in Z$
58	49 56 57	syl2anc	$⊢ ((φ \land j \in Z) \land (n \in ℤ_{\geq j} \land m \in ℤ_{\geq n})) \to m \in Z$
59		fveq2	$⊢ k = m \to F (k) = F (m)$
60	59	oveq2d	$⊢ k = m \to S D F (k) = S D F (m)$
61		ovex	$⊢ S D F (m) \in V$
62	60 41 61	fvmpt	$⊢ m \in Z \to (k \in Z ⟼ S D F (k)) (m) = S D F (m)$
63	58 62	syl	$⊢ ((φ \land j \in Z) \land (n \in ℤ_{\geq j} \land m \in ℤ_{\geq n})) \to (k \in Z ⟼ S D F (k)) (m) = S D F (m)$
64	63	fveq1d	$⊢ ((φ \land j \in Z) \land (n \in ℤ_{\geq j} \land m \in ℤ_{\geq n})) \to (k \in Z ⟼ S D F (k)) (m) (x) = {F (m)}_{S}^{'} (x)$
65	55 64	oveq12d	$⊢ ((φ \land j \in Z) \land (n \in ℤ_{\geq j} \land m \in ℤ_{\geq n})) \to (k \in Z ⟼ S D F (k)) (n) (x) - (k \in Z ⟼ S D F (k)) (m) (x) = {F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)$
66	65	fveq2d	$⊢ ((φ \land j \in Z) \land (n \in ℤ_{\geq j} \land m \in ℤ_{\geq n})) \to \|(k \in Z ⟼ S D F (k)) (n) (x) - (k \in Z ⟼ S D F (k)) (m) (x)\| = \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\|$
67	66	breq1d	$⊢ ((φ \land j \in Z) \land (n \in ℤ_{\geq j} \land m \in ℤ_{\geq n})) \to (\|(k \in Z ⟼ S D F (k)) (n) (x) - (k \in Z ⟼ S D F (k)) (m) (x)\| < s \leftrightarrow \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < s)$
68	67	ralbidv	$⊢ ((φ \land j \in Z) \land (n \in ℤ_{\geq j} \land m \in ℤ_{\geq n})) \to (\forall x \in X \|(k \in Z ⟼ S D F (k)) (n) (x) - (k \in Z ⟼ S D F (k)) (m) (x)\| < s \leftrightarrow \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < s)$
69	68	2ralbidva	$⊢ (φ \land j \in Z) \to (\forall n \in ℤ_{\geq j} \forall m \in ℤ_{\geq n} \forall x \in X \|(k \in Z ⟼ S D F (k)) (n) (x) - (k \in Z ⟼ S D F (k)) (m) (x)\| < s \leftrightarrow \forall n \in ℤ_{\geq j} \forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < s)$
70	69	rexbidva	$⊢ φ \to (\exists j \in Z \forall n \in ℤ_{\geq j} \forall m \in ℤ_{\geq n} \forall x \in X \|(k \in Z ⟼ S D F (k)) (n) (x) - (k \in Z ⟼ S D F (k)) (m) (x)\| < s \leftrightarrow \exists j \in Z \forall n \in ℤ_{\geq j} \forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < s)$
71	70	ralbidv	$⊢ φ \to (\forall s \in ℝ^{+} \exists j \in Z \forall n \in ℤ_{\geq j} \forall m \in ℤ_{\geq n} \forall x \in X \|(k \in Z ⟼ S D F (k)) (n) (x) - (k \in Z ⟼ S D F (k)) (m) (x)\| < s \leftrightarrow \forall s \in ℝ^{+} \exists j \in Z \forall n \in ℤ_{\geq j} \forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < s)$
72	47 71	mpbid	$⊢ φ \to \forall s \in ℝ^{+} \exists j \in Z \forall n \in ℤ_{\geq j} \forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < s$
73	72	ad2antrr	$⊢ ((φ \land z \in X) \land r \in ℝ^{+}) \to \forall s \in ℝ^{+} \exists j \in Z \forall n \in ℤ_{\geq j} \forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < s$
74		rphalfcl	$⊢ r \in ℝ^{+} \to \frac{r}{2} \in ℝ^{+}$
75	74	adantl	$⊢ ((φ \land z \in X) \land r \in ℝ^{+}) \to \frac{r}{2} \in ℝ^{+}$
76		rphalfcl	$⊢ \frac{r}{2} \in ℝ^{+} \to \frac{\frac{r}{2}}{2} \in ℝ^{+}$
77	75 76	syl	$⊢ ((φ \land z \in X) \land r \in ℝ^{+}) \to \frac{\frac{r}{2}}{2} \in ℝ^{+}$
78	33 73 77	rspcdva	$⊢ ((φ \land z \in X) \land r \in ℝ^{+}) \to \exists j \in Z \forall n \in ℤ_{\geq j} \forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2}$
79	3	ad2antrr	$⊢ ((φ \land z \in X) \land r \in ℝ^{+}) \to M \in ℤ$
80	51	fveq1d	$⊢ k = n \to {F (k)}_{S}^{'} (z) = {F (n)}_{S}^{'} (z)$
81		eqid	$⊢ (k \in Z ⟼ {F (k)}_{S}^{'} (z)) = (k \in Z ⟼ {F (k)}_{S}^{'} (z))$
82		fvex	$⊢ {F (n)}_{S}^{'} (z) \in V$
83	80 81 82	fvmpt	$⊢ n \in Z \to (k \in Z ⟼ {F (k)}_{S}^{'} (z)) (n) = {F (n)}_{S}^{'} (z)$
84	83	adantl	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to (k \in Z ⟼ {F (k)}_{S}^{'} (z)) (n) = {F (n)}_{S}^{'} (z)$
85	45	ad2antrr	$⊢ ((φ \land z \in X) \land r \in ℝ^{+}) \to (k \in Z ⟼ S D F (k)) : Z ⟶ ℂ^{X}$
86		simplr	$⊢ ((φ \land z \in X) \land r \in ℝ^{+}) \to z \in X$
87	1	fvexi	$⊢ Z \in V$
88	87	mptex	$⊢ (k \in Z ⟼ {F (k)}_{S}^{'} (z)) \in V$
89	88	a1i	$⊢ ((φ \land z \in X) \land r \in ℝ^{+}) \to (k \in Z ⟼ {F (k)}_{S}^{'} (z)) \in V$
90	53	adantl	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to (k \in Z ⟼ S D F (k)) (n) = S D F (n)$
91	90	fveq1d	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to (k \in Z ⟼ S D F (k)) (n) (z) = {F (n)}_{S}^{'} (z)$
92	91 84	eqtr4d	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to (k \in Z ⟼ S D F (k)) (n) (z) = (k \in Z ⟼ {F (k)}_{S}^{'} (z)) (n)$
93	7	ad2antrr	$⊢ ((φ \land z \in X) \land r \in ℝ^{+}) \to (k \in Z ⟼ S D F (k)) \underset{u}{⇝} (X) H$
94	1 79 85 86 89 92 93	ulmclm	$⊢ ((φ \land z \in X) \land r \in ℝ^{+}) \to (k \in Z ⟼ {F (k)}_{S}^{'} (z)) ⇝ H (z)$
95	1 79 75 84 94	climi2	$⊢ ((φ \land z \in X) \land r \in ℝ^{+}) \to \exists j \in Z \forall n \in ℤ_{\geq j} \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}$
96	1	rexanuz2	$⊢ \exists j \in Z \forall n \in ℤ_{\geq j} (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \leftrightarrow (\exists j \in Z \forall n \in ℤ_{\geq j} \forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \exists j \in Z \forall n \in ℤ_{\geq j} \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2})$
97	1	r19.2uz	$⊢ \exists j \in Z \forall n \in ℤ_{\geq j} (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \to \exists n \in Z (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2})$
98	96 97	sylbir	$⊢ (\exists j \in Z \forall n \in ℤ_{\geq j} \forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \exists j \in Z \forall n \in ℤ_{\geq j} \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \to \exists n \in Z (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2})$
99		fveq2	$⊢ y = v \to F (n) (y) = F (n) (v)$
100	99	oveq1d	$⊢ y = v \to F (n) (y) - F (n) (z) = F (n) (v) - F (n) (z)$
101		oveq1	$⊢ y = v \to y - z = v - z$
102	100 101	oveq12d	$⊢ y = v \to \frac{F (n) (y) - F (n) (z)}{y - z} = \frac{F (n) (v) - F (n) (z)}{v - z}$
103		eqid	$⊢ (y \in (X ∖ \{z\}) ⟼ \frac{F (n) (y) - F (n) (z)}{y - z}) = (y \in (X ∖ \{z\}) ⟼ \frac{F (n) (y) - F (n) (z)}{y - z})$
104		ovex	$⊢ \frac{F (n) (v) - F (n) (z)}{v - z} \in V$
105	102 103 104	fvmpt	$⊢ v \in (X ∖ \{z\}) \to (y \in (X ∖ \{z\}) ⟼ \frac{F (n) (y) - F (n) (z)}{y - z}) (v) = \frac{F (n) (v) - F (n) (z)}{v - z}$
106	105	fvoveq1d	$⊢ v \in (X ∖ \{z\}) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{F (n) (y) - F (n) (z)}{y - z}) (v) - {F (n)}_{S}^{'} (z)\| = \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\|$
107		id	$⊢ s = \frac{\frac{r}{2}}{2} \to s = \frac{\frac{r}{2}}{2}$
108	106 107	breqan12rd	$⊢ (s = \frac{\frac{r}{2}}{2} \land v \in (X ∖ \{z\})) \to (\|(y \in (X ∖ \{z\}) ⟼ \frac{F (n) (y) - F (n) (z)}{y - z}) (v) - {F (n)}_{S}^{'} (z)\| < s \leftrightarrow \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2})$
109	108	imbi2d	$⊢ (s = \frac{\frac{r}{2}}{2} \land v \in (X ∖ \{z\})) \to (((v \neq z \land \|v - z\| < w) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{F (n) (y) - F (n) (z)}{y - z}) (v) - {F (n)}_{S}^{'} (z)\| < s) \leftrightarrow ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}))$
110	109	ralbidva	$⊢ s = \frac{\frac{r}{2}}{2} \to (\forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{F (n) (y) - F (n) (z)}{y - z}) (v) - {F (n)}_{S}^{'} (z)\| < s) \leftrightarrow \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}))$
111	110	rexbidv	$⊢ s = \frac{\frac{r}{2}}{2} \to (\exists w \in ℝ^{+} \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{F (n) (y) - F (n) (z)}{y - z}) (v) - {F (n)}_{S}^{'} (z)\| < s) \leftrightarrow \exists w \in ℝ^{+} \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}))$
112		simpllr	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to z \in X$
113	85	ffvelcdmda	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to (k \in Z ⟼ S D F (k)) (n) \in (ℂ^{X})$
114	90 113	eqeltrrd	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to S D F (n) \in (ℂ^{X})$
115		elmapi	$⊢ S D F (n) \in (ℂ^{X}) \to {F (n)}_{S}^{'} : X ⟶ ℂ$
116		fdm	$⊢ {F (n)}_{S}^{'} : X ⟶ ℂ \to dom {F (n)}_{S}^{'} = X$
117	114 115 116	3syl	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to dom {F (n)}_{S}^{'} = X$
118	112 117	eleqtrrd	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to z \in dom {F (n)}_{S}^{'}$
119	2	ad3antrrr	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to S \in \{ℝ, ℂ\}$
120		dvfg	$⊢ S \in \{ℝ, ℂ\} \to {F (n)}_{S}^{'} : dom {F (n)}_{S}^{'} ⟶ ℂ$
121		ffun	$⊢ {F (n)}_{S}^{'} : dom {F (n)}_{S}^{'} ⟶ ℂ \to Fun {F (n)}_{S}^{'}$
122		funfvbrb	$⊢ Fun {F (n)}_{S}^{'} \to (z \in dom {F (n)}_{S}^{'} \leftrightarrow z {F (n)}_{S}^{'} {F (n)}_{S}^{'} (z))$
123	119 120 121 122	4syl	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to (z \in dom {F (n)}_{S}^{'} \leftrightarrow z {F (n)}_{S}^{'} {F (n)}_{S}^{'} (z))$
124	118 123	mpbid	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to z {F (n)}_{S}^{'} {F (n)}_{S}^{'} (z)$
125	119 10	syl	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to S \subseteq ℂ$
126	4	ad2antrr	$⊢ ((φ \land z \in X) \land r \in ℝ^{+}) \to F : Z ⟶ ℂ^{X}$
127	126	ffvelcdmda	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to F (n) \in (ℂ^{X})$
128		elmapi	$⊢ F (n) \in (ℂ^{X}) \to F (n) : X ⟶ ℂ$
129	127 128	syl	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to F (n) : X ⟶ ℂ$
130		biidd	$⊢ k = M \to (X \subseteq S \leftrightarrow X \subseteq S)$
131	17	ralrimiva	$⊢ φ \to \forall k \in Z X \subseteq S$
132	130 131 25	rspcdva	$⊢ φ \to X \subseteq S$
133	132	ad3antrrr	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to X \subseteq S$
134	18 19 103 125 129 133	eldv	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to (z {F (n)}_{S}^{'} {F (n)}_{S}^{'} (z) \leftrightarrow (z \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X) \land {F (n)}_{S}^{'} (z) \in ((y \in (X ∖ \{z\}) ⟼ \frac{F (n) (y) - F (n) (z)}{y - z}) {lim}_{ℂ} z)))$
135	124 134	mpbid	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to (z \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X) \land {F (n)}_{S}^{'} (z) \in ((y \in (X ∖ \{z\}) ⟼ \frac{F (n) (y) - F (n) (z)}{y - z}) {lim}_{ℂ} z))$
136	135	simprd	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to {F (n)}_{S}^{'} (z) \in ((y \in (X ∖ \{z\}) ⟼ \frac{F (n) (y) - F (n) (z)}{y - z}) {lim}_{ℂ} z)$
137	132	adantr	$⊢ (φ \land z \in X) \to X \subseteq S$
138	11	adantr	$⊢ (φ \land z \in X) \to S \subseteq ℂ$
139	137 138	sstrd	$⊢ (φ \land z \in X) \to X \subseteq ℂ$
140	139	ad2antrr	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to X \subseteq ℂ$
141	129 140 112	dvlem	$⊢ ((((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \land y \in (X ∖ \{z\})) \to \frac{F (n) (y) - F (n) (z)}{y - z} \in ℂ$
142	141	fmpttd	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to (y \in (X ∖ \{z\}) ⟼ \frac{F (n) (y) - F (n) (z)}{y - z}) : X ∖ \{z\} ⟶ ℂ$
143	140	ssdifssd	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to X ∖ \{z\} \subseteq ℂ$
144	140 112	sseldd	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to z \in ℂ$
145	142 143 144	ellimc3	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to ({F (n)}_{S}^{'} (z) \in ((y \in (X ∖ \{z\}) ⟼ \frac{F (n) (y) - F (n) (z)}{y - z}) {lim}_{ℂ} z) \leftrightarrow ({F (n)}_{S}^{'} (z) \in ℂ \land \forall s \in ℝ^{+} \exists w \in ℝ^{+} \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{F (n) (y) - F (n) (z)}{y - z}) (v) - {F (n)}_{S}^{'} (z)\| < s)))$
146	136 145	mpbid	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to ({F (n)}_{S}^{'} (z) \in ℂ \land \forall s \in ℝ^{+} \exists w \in ℝ^{+} \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{F (n) (y) - F (n) (z)}{y - z}) (v) - {F (n)}_{S}^{'} (z)\| < s))$
147	146	simprd	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to \forall s \in ℝ^{+} \exists w \in ℝ^{+} \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{F (n) (y) - F (n) (z)}{y - z}) (v) - {F (n)}_{S}^{'} (z)\| < s)$
148	77	adantr	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to \frac{\frac{r}{2}}{2} \in ℝ^{+}$
149	111 147 148	rspcdva	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land n \in Z) \to \exists w \in ℝ^{+} \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2})$
150	149	adantrr	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \to \exists w \in ℝ^{+} \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2})$
151		anass	$⊢ (((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land (u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X))) \land w \in ℝ^{+}) \leftrightarrow ((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land ((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}))$
152		df-3an	$⊢ (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))) \leftrightarrow ((n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2})) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u))))$
153		anass	$⊢ ((φ \land z \in X) \land r \in ℝ^{+}) \leftrightarrow (φ \land (z \in X \land r \in ℝ^{+}))$
154	6	ralrimiva	$⊢ φ \to \forall z \in X (k \in Z ⟼ F (k) (z)) ⇝ G (z)$
155		fveq2	$⊢ z = s \to F (k) (z) = F (k) (s)$
156	155	mpteq2dv	$⊢ z = s \to (k \in Z ⟼ F (k) (z)) = (k \in Z ⟼ F (k) (s))$
157		fveq2	$⊢ z = s \to G (z) = G (s)$
158	156 157	breq12d	$⊢ z = s \to ((k \in Z ⟼ F (k) (z)) ⇝ G (z) \leftrightarrow (k \in Z ⟼ F (k) (s)) ⇝ G (s))$
159	158	rspccva	$⊢ (\forall z \in X (k \in Z ⟼ F (k) (z)) ⇝ G (z) \land s \in X) \to (k \in Z ⟼ F (k) (s)) ⇝ G (s)$
160	154 159	sylan	$⊢ (φ \land s \in X) \to (k \in Z ⟼ F (k) (s)) ⇝ G (s)$
161		simprll	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to z \in X$
162		simprlr	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to r \in ℝ^{+}$
163		simprr3	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))$
164		simplll	$⊢ (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u))) \to u \in ℝ^{+}$
165	163 164	syl	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to u \in ℝ^{+}$
166		simplr	$⊢ (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u))) \to w \in ℝ^{+}$
167	163 166	syl	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to w \in ℝ^{+}$
168		simpllr	$⊢ (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u))) \to (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)$
169	163 168	syl	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)$
170	169	simpld	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to u < w$
171	169	simprd	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X$
172		simpr3	$⊢ (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u))) \to (v \neq z \land \|v - z\| < u)$
173	163 172	syl	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to (v \neq z \land \|v - z\| < u)$
174	173	simprd	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to \|v - z\| < u$
175		simprr1	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to n \in Z$
176		simprr2	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2})$
177	176	simpld	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to \forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2}$
178	176	simprd	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}$
179		simpr1	$⊢ (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u))) \to v \in (X ∖ \{z\})$
180	163 179	syl	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to v \in (X ∖ \{z\})$
181	180	eldifad	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to v \in X$
182	173	simpld	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to v \neq z$
183		simpr2	$⊢ (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u))) \to ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2})$
184	163 183	syl	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2})$
185	182 184	mpand	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to (\|v - z\| < w \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2})$
186	1 2 3 4 5 160 7 161 162 165 167 170 171 174 175 177 178 181 182 185	ulmdvlem1	$⊢ (φ \land ((z \in X \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))))) \to \|(\frac{G (v) - G (z)}{v - z}) - H (z)\| < r$
187	186	anassrs	$⊢ ((φ \land (z \in X \land r \in ℝ^{+})) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u))))) \to \|(\frac{G (v) - G (z)}{v - z}) - H (z)\| < r$
188	153 187	sylanb	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u))))) \to \|(\frac{G (v) - G (z)}{v - z}) - H (z)\| < r$
189	152 188	sylan2br	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land ((n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2})) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u))))) \to \|(\frac{G (v) - G (z)}{v - z}) - H (z)\| < r$
190	189	anassrs	$⊢ ((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land (((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u)))) \to \|(\frac{G (v) - G (z)}{v - z}) - H (z)\| < r$
191	190	anassrs	$⊢ (((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land ((u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)) \land w \in ℝ^{+})) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u))) \to \|(\frac{G (v) - G (z)}{v - z}) - H (z)\| < r$
192	151 191	sylanb	$⊢ ((((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land (u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X))) \land w \in ℝ^{+}) \land (v \in (X ∖ \{z\}) \land ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \land (v \neq z \land \|v - z\| < u))) \to \|(\frac{G (v) - G (z)}{v - z}) - H (z)\| < r$
193	192	3exp2	$⊢ (((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land (u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X))) \land w \in ℝ^{+}) \to (v \in (X ∖ \{z\}) \to (((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \to ((v \neq z \land \|v - z\| < u) \to \|(\frac{G (v) - G (z)}{v - z}) - H (z)\| < r)))$
194	193	imp	$⊢ ((((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land (u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X))) \land w \in ℝ^{+}) \land v \in (X ∖ \{z\})) \to (((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \to ((v \neq z \land \|v - z\| < u) \to \|(\frac{G (v) - G (z)}{v - z}) - H (z)\| < r))$
195		fveq2	$⊢ y = v \to G (y) = G (v)$
196	195	oveq1d	$⊢ y = v \to G (y) - G (z) = G (v) - G (z)$
197	196 101	oveq12d	$⊢ y = v \to \frac{G (y) - G (z)}{y - z} = \frac{G (v) - G (z)}{v - z}$
198		eqid	$⊢ (y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) = (y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z})$
199		ovex	$⊢ \frac{G (v) - G (z)}{v - z} \in V$
200	197 198 199	fvmpt	$⊢ v \in (X ∖ \{z\}) \to (y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) (v) = \frac{G (v) - G (z)}{v - z}$
201	200	fvoveq1d	$⊢ v \in (X ∖ \{z\}) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) (v) - H (z)\| = \|(\frac{G (v) - G (z)}{v - z}) - H (z)\|$
202	201	breq1d	$⊢ v \in (X ∖ \{z\}) \to (\|(y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) (v) - H (z)\| < r \leftrightarrow \|(\frac{G (v) - G (z)}{v - z}) - H (z)\| < r)$
203	202	imbi2d	$⊢ v \in (X ∖ \{z\}) \to (((v \neq z \land \|v - z\| < u) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) (v) - H (z)\| < r) \leftrightarrow ((v \neq z \land \|v - z\| < u) \to \|(\frac{G (v) - G (z)}{v - z}) - H (z)\| < r))$
204	203	adantl	$⊢ ((((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land (u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X))) \land w \in ℝ^{+}) \land v \in (X ∖ \{z\})) \to (((v \neq z \land \|v - z\| < u) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) (v) - H (z)\| < r) \leftrightarrow ((v \neq z \land \|v - z\| < u) \to \|(\frac{G (v) - G (z)}{v - z}) - H (z)\| < r))$
205	194 204	sylibrd	$⊢ ((((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land (u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X))) \land w \in ℝ^{+}) \land v \in (X ∖ \{z\})) \to (((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \to ((v \neq z \land \|v - z\| < u) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) (v) - H (z)\| < r))$
206	205	ralimdva	$⊢ (((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land (u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X))) \land w \in ℝ^{+}) \to (\forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}) \to \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < u) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) (v) - H (z)\| < r))$
207	206	impr	$⊢ (((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land (u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X))) \land (w \in ℝ^{+} \land \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}))) \to \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < u) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) (v) - H (z)\| < r)$
208	207	an32s	$⊢ (((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land (w \in ℝ^{+} \land \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}))) \land (u \in ℝ^{+} \land (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X))) \to \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < u) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) (v) - H (z)\| < r)$
209		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
210		xmetres2	$⊢ (abs \circ - \in ∞Met (ℂ) \land S \subseteq ℂ) \to {(abs \circ -) ↾}_{(S \times S)} \in ∞Met (S)$
211	209 138 210	sylancr	$⊢ (φ \land z \in X) \to {(abs \circ -) ↾}_{(S \times S)} \in ∞Met (S)$
212	211	ad3antrrr	$⊢ ((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land (w \in ℝ^{+} \land \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}))) \to {(abs \circ -) ↾}_{(S \times S)} \in ∞Met (S)$
213	19	cnfldtop	$⊢ TopOpen (ℂ_{fld}) \in Top$
214		resttop	$⊢ (TopOpen (ℂ_{fld}) \in Top \land S \in \{ℝ, ℂ\}) \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Top$
215	213 2 214	sylancr	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Top$
216	19	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
217		resttopon	$⊢ (TopOpen (ℂ_{fld}) \in TopOn (ℂ) \land S \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S)$
218	216 11 217	sylancr	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S)$
219		toponuni	$⊢ TopOpen (ℂ_{fld}) ↾_{𝑡} S \in TopOn (S) \to S = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
220	218 219	syl	$⊢ φ \to S = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
221	132 220	sseqtrd	$⊢ φ \to X \subseteq ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
222		eqid	$⊢ ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S) = ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
223	222	ntrss2	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Top \land X \subseteq ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)) \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X) \subseteq X$
224	215 221 223	syl2anc	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X) \subseteq X$
225	224 26	eqssd	$⊢ φ \to int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X) = X$
226	222	isopn3	$⊢ (TopOpen (ℂ_{fld}) ↾_{𝑡} S \in Top \land X \subseteq ⋃ (TopOpen (ℂ_{fld}) ↾_{𝑡} S)) \to (X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S) \leftrightarrow int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X) = X)$
227	215 221 226	syl2anc	$⊢ φ \to (X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S) \leftrightarrow int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X) = X)$
228	225 227	mpbird	$⊢ φ \to X \in (TopOpen (ℂ_{fld}) ↾_{𝑡} S)$
229		eqid	$⊢ {(abs \circ -) ↾}_{(S \times S)} = {(abs \circ -) ↾}_{(S \times S)}$
230	19	cnfldtopn	$⊢ TopOpen (ℂ_{fld}) = MetOpen (abs \circ -)$
231		eqid	$⊢ MetOpen ({(abs \circ -) ↾}_{(S \times S)}) = MetOpen ({(abs \circ -) ↾}_{(S \times S)})$
232	229 230 231	metrest	$⊢ (abs \circ - \in ∞Met (ℂ) \land S \subseteq ℂ) \to TopOpen (ℂ_{fld}) ↾_{𝑡} S = MetOpen ({(abs \circ -) ↾}_{(S \times S)})$
233	209 11 232	sylancr	$⊢ φ \to TopOpen (ℂ_{fld}) ↾_{𝑡} S = MetOpen ({(abs \circ -) ↾}_{(S \times S)})$
234	228 233	eleqtrd	$⊢ φ \to X \in MetOpen ({(abs \circ -) ↾}_{(S \times S)})$
235	234	adantr	$⊢ (φ \land z \in X) \to X \in MetOpen ({(abs \circ -) ↾}_{(S \times S)})$
236	235	ad3antrrr	$⊢ ((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land (w \in ℝ^{+} \land \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}))) \to X \in MetOpen ({(abs \circ -) ↾}_{(S \times S)})$
237	86	ad2antrr	$⊢ ((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land (w \in ℝ^{+} \land \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}))) \to z \in X$
238		simprl	$⊢ ((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land (w \in ℝ^{+} \land \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}))) \to w \in ℝ^{+}$
239	231	mopni3	$⊢ (({(abs \circ -) ↾}_{(S \times S)} \in ∞Met (S) \land X \in MetOpen ({(abs \circ -) ↾}_{(S \times S)}) \land z \in X) \land w \in ℝ^{+}) \to \exists u \in ℝ^{+} (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)$
240	212 236 237 238 239	syl31anc	$⊢ ((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land (w \in ℝ^{+} \land \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}))) \to \exists u \in ℝ^{+} (u < w \land z ball ({(abs \circ -) ↾}_{(S \times S)}) u \subseteq X)$
241	208 240	reximddv	$⊢ ((((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \land (w \in ℝ^{+} \land \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < w) \to \|(\frac{F (n) (v) - F (n) (z)}{v - z}) - {F (n)}_{S}^{'} (z)\| < \frac{\frac{r}{2}}{2}))) \to \exists u \in ℝ^{+} \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < u) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) (v) - H (z)\| < r)$
242	150 241	rexlimddv	$⊢ (((φ \land z \in X) \land r \in ℝ^{+}) \land (n \in Z \land (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}))) \to \exists u \in ℝ^{+} \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < u) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) (v) - H (z)\| < r)$
243	242	rexlimdvaa	$⊢ ((φ \land z \in X) \land r \in ℝ^{+}) \to (\exists n \in Z (\forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \to \exists u \in ℝ^{+} \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < u) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) (v) - H (z)\| < r))$
244	98 243	syl5	$⊢ ((φ \land z \in X) \land r \in ℝ^{+}) \to ((\exists j \in Z \forall n \in ℤ_{\geq j} \forall m \in ℤ_{\geq n} \forall x \in X \|{F (n)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{r}{2}}{2} \land \exists j \in Z \forall n \in ℤ_{\geq j} \|{F (n)}_{S}^{'} (z) - H (z)\| < \frac{r}{2}) \to \exists u \in ℝ^{+} \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < u) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) (v) - H (z)\| < r))$
245	78 95 244	mp2and	$⊢ ((φ \land z \in X) \land r \in ℝ^{+}) \to \exists u \in ℝ^{+} \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < u) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) (v) - H (z)\| < r)$
246	245	ralrimiva	$⊢ (φ \land z \in X) \to \forall r \in ℝ^{+} \exists u \in ℝ^{+} \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < u) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) (v) - H (z)\| < r)$
247	5	adantr	$⊢ (φ \land z \in X) \to G : X ⟶ ℂ$
248		simpr	$⊢ (φ \land z \in X) \to z \in X$
249	247 139 248	dvlem	$⊢ ((φ \land z \in X) \land y \in (X ∖ \{z\})) \to \frac{G (y) - G (z)}{y - z} \in ℂ$
250	249	fmpttd	$⊢ (φ \land z \in X) \to (y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) : X ∖ \{z\} ⟶ ℂ$
251	139	ssdifssd	$⊢ (φ \land z \in X) \to X ∖ \{z\} \subseteq ℂ$
252	139 248	sseldd	$⊢ (φ \land z \in X) \to z \in ℂ$
253	250 251 252	ellimc3	$⊢ (φ \land z \in X) \to (H (z) \in ((y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) {lim}_{ℂ} z) \leftrightarrow (H (z) \in ℂ \land \forall r \in ℝ^{+} \exists u \in ℝ^{+} \forall v \in (X ∖ \{z\}) ((v \neq z \land \|v - z\| < u) \to \|(y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) (v) - H (z)\| < r)))$
254	30 246 253	mpbir2and	$⊢ (φ \land z \in X) \to H (z) \in ((y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) {lim}_{ℂ} z)$
255	18 19 198 138 247 137	eldv	$⊢ (φ \land z \in X) \to (z G_{S}^{'} H (z) \leftrightarrow (z \in int (TopOpen (ℂ_{fld}) ↾_{𝑡} S) (X) \land H (z) \in ((y \in (X ∖ \{z\}) ⟼ \frac{G (y) - G (z)}{y - z}) {lim}_{ℂ} z)))$
256	27 254 255	mpbir2and	$⊢ (φ \land z \in X) \to z G_{S}^{'} H (z)$

Metamath Proof Explorer

Theorem ulmdvlem3

Proof