ulmdvlem1

	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$
	ulmdvlem1.c	$⊢ (φ \land ψ) \to C \in X$
	ulmdvlem1.r	$⊢ (φ \land ψ) \to R \in ℝ^{+}$
	ulmdvlem1.u	$⊢ (φ \land ψ) \to U \in ℝ^{+}$
	ulmdvlem1.v	$⊢ (φ \land ψ) \to W \in ℝ^{+}$
	ulmdvlem1.l	$⊢ (φ \land ψ) \to U < W$
	ulmdvlem1.b	$⊢ (φ \land ψ) \to C ball ({(abs \circ -) ↾}_{(S \times S)}) U \subseteq X$
	ulmdvlem1.a	$⊢ (φ \land ψ) \to \|Y - C\| < U$
	ulmdvlem1.n	$⊢ (φ \land ψ) \to N \in Z$
	ulmdvlem1.1	$⊢ (φ \land ψ) \to \forall m \in ℤ_{\geq N} \forall x \in X \|{F (N)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{R}{2}}{2}$
	ulmdvlem1.2	$⊢ (φ \land ψ) \to \|{F (N)}_{S}^{'} (C) - H (C)\| < \frac{R}{2}$
	ulmdvlem1.y	$⊢ (φ \land ψ) \to Y \in X$
	ulmdvlem1.3	$⊢ (φ \land ψ) \to Y \neq C$
	ulmdvlem1.4	$⊢ (φ \land ψ) \to (\|Y - C\| < W \to \|(\frac{F (N) (Y) - F (N) (C)}{Y - C}) - {F (N)}_{S}^{'} (C)\| < \frac{\frac{R}{2}}{2})$
Assertion	ulmdvlem1	$⊢ (φ \land ψ) \to \|(\frac{G (Y) - G (C)}{Y - C}) - H (C)\| < R$

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		ulmdvlem1.c	$⊢ (φ \land ψ) \to C \in X$
9		ulmdvlem1.r	$⊢ (φ \land ψ) \to R \in ℝ^{+}$
10		ulmdvlem1.u	$⊢ (φ \land ψ) \to U \in ℝ^{+}$
11		ulmdvlem1.v	$⊢ (φ \land ψ) \to W \in ℝ^{+}$
12		ulmdvlem1.l	$⊢ (φ \land ψ) \to U < W$
13		ulmdvlem1.b	$⊢ (φ \land ψ) \to C ball ({(abs \circ -) ↾}_{(S \times S)}) U \subseteq X$
14		ulmdvlem1.a	$⊢ (φ \land ψ) \to \|Y - C\| < U$
15		ulmdvlem1.n	$⊢ (φ \land ψ) \to N \in Z$
16		ulmdvlem1.1	$⊢ (φ \land ψ) \to \forall m \in ℤ_{\geq N} \forall x \in X \|{F (N)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{R}{2}}{2}$
17		ulmdvlem1.2	$⊢ (φ \land ψ) \to \|{F (N)}_{S}^{'} (C) - H (C)\| < \frac{R}{2}$
18		ulmdvlem1.y	$⊢ (φ \land ψ) \to Y \in X$
19		ulmdvlem1.3	$⊢ (φ \land ψ) \to Y \neq C$
20		ulmdvlem1.4	$⊢ (φ \land ψ) \to (\|Y - C\| < W \to \|(\frac{F (N) (Y) - F (N) (C)}{Y - C}) - {F (N)}_{S}^{'} (C)\| < \frac{\frac{R}{2}}{2})$
21	5	adantr	$⊢ (φ \land ψ) \to G : X ⟶ ℂ$
22	21 18	ffvelrnd	$⊢ (φ \land ψ) \to G (Y) \in ℂ$
23	21 8	ffvelrnd	$⊢ (φ \land ψ) \to G (C) \in ℂ$
24	22 23	subcld	$⊢ (φ \land ψ) \to G (Y) - G (C) \in ℂ$
25		fveq2	$⊢ k = N \to F (k) = F (N)$
26	25	oveq2d	$⊢ k = N \to S D F (k) = S D F (N)$
27		eqid	$⊢ (k \in Z ⟼ S D F (k)) = (k \in Z ⟼ S D F (k))$
28		ovex	$⊢ S D F (N) \in V$
29	26 27 28	fvmpt	$⊢ N \in Z \to (k \in Z ⟼ S D F (k)) (N) = S D F (N)$
30	15 29	syl	$⊢ (φ \land ψ) \to (k \in Z ⟼ S D F (k)) (N) = S D F (N)$
31		ovex	$⊢ S D F (k) \in V$
32	31	rgenw	$⊢ \forall k \in Z S D F (k) \in V$
33	27	fnmpt	$⊢ \forall k \in Z S D F (k) \in V \to (k \in Z ⟼ S D F (k)) Fn Z$
34	32 33	mp1i	$⊢ φ \to (k \in Z ⟼ S D F (k)) Fn Z$
35		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}$
36	34 7 35	syl2anc	$⊢ φ \to (k \in Z ⟼ S D F (k)) : Z ⟶ ℂ^{X}$
37	36	adantr	$⊢ (φ \land ψ) \to (k \in Z ⟼ S D F (k)) : Z ⟶ ℂ^{X}$
38	37 15	ffvelrnd	$⊢ (φ \land ψ) \to (k \in Z ⟼ S D F (k)) (N) \in (ℂ^{X})$
39	30 38	eqeltrrd	$⊢ (φ \land ψ) \to S D F (N) \in (ℂ^{X})$
40		elmapi	$⊢ S D F (N) \in (ℂ^{X}) \to {F (N)}_{S}^{'} : X ⟶ ℂ$
41	39 40	syl	$⊢ (φ \land ψ) \to {F (N)}_{S}^{'} : X ⟶ ℂ$
42	41	fdmd	$⊢ (φ \land ψ) \to dom {F (N)}_{S}^{'} = X$
43		dvbsss	$⊢ dom {F (N)}_{S}^{'} \subseteq S$
44	42 43	eqsstrrdi	$⊢ (φ \land ψ) \to X \subseteq S$
45		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
46	2 45	syl	$⊢ φ \to S \subseteq ℂ$
47	46	adantr	$⊢ (φ \land ψ) \to S \subseteq ℂ$
48	44 47	sstrd	$⊢ (φ \land ψ) \to X \subseteq ℂ$
49	48 18	sseldd	$⊢ (φ \land ψ) \to Y \in ℂ$
50	48 8	sseldd	$⊢ (φ \land ψ) \to C \in ℂ$
51	49 50	subcld	$⊢ (φ \land ψ) \to Y - C \in ℂ$
52	49 50 19	subne0d	$⊢ (φ \land ψ) \to Y - C \neq 0$
53	24 51 52	divcld	$⊢ (φ \land ψ) \to \frac{G (Y) - G (C)}{Y - C} \in ℂ$
54		ulmcl	$⊢ (k \in Z ⟼ S D F (k)) \underset{u}{⇝} (X) H \to H : X ⟶ ℂ$
55	7 54	syl	$⊢ φ \to H : X ⟶ ℂ$
56	55	adantr	$⊢ (φ \land ψ) \to H : X ⟶ ℂ$
57	56 8	ffvelrnd	$⊢ (φ \land ψ) \to H (C) \in ℂ$
58	41 8	ffvelrnd	$⊢ (φ \land ψ) \to {F (N)}_{S}^{'} (C) \in ℂ$
59	9	rpred	$⊢ (φ \land ψ) \to R \in ℝ$
60	53 58	subcld	$⊢ (φ \land ψ) \to (\frac{G (Y) - G (C)}{Y - C}) - {F (N)}_{S}^{'} (C) \in ℂ$
61	60	abscld	$⊢ (φ \land ψ) \to \|(\frac{G (Y) - G (C)}{Y - C}) - {F (N)}_{S}^{'} (C)\| \in ℝ$
62	4	adantr	$⊢ (φ \land ψ) \to F : Z ⟶ ℂ^{X}$
63	62 15	ffvelrnd	$⊢ (φ \land ψ) \to F (N) \in (ℂ^{X})$
64		elmapi	$⊢ F (N) \in (ℂ^{X}) \to F (N) : X ⟶ ℂ$
65	63 64	syl	$⊢ (φ \land ψ) \to F (N) : X ⟶ ℂ$
66	65 18	ffvelrnd	$⊢ (φ \land ψ) \to F (N) (Y) \in ℂ$
67	65 8	ffvelrnd	$⊢ (φ \land ψ) \to F (N) (C) \in ℂ$
68	66 67	subcld	$⊢ (φ \land ψ) \to F (N) (Y) - F (N) (C) \in ℂ$
69	68 51 52	divcld	$⊢ (φ \land ψ) \to \frac{F (N) (Y) - F (N) (C)}{Y - C} \in ℂ$
70	53 69	subcld	$⊢ (φ \land ψ) \to (\frac{G (Y) - G (C)}{Y - C}) - (\frac{F (N) (Y) - F (N) (C)}{Y - C}) \in ℂ$
71	70	abscld	$⊢ (φ \land ψ) \to \|(\frac{G (Y) - G (C)}{Y - C}) - (\frac{F (N) (Y) - F (N) (C)}{Y - C})\| \in ℝ$
72	69 58	subcld	$⊢ (φ \land ψ) \to (\frac{F (N) (Y) - F (N) (C)}{Y - C}) - {F (N)}_{S}^{'} (C) \in ℂ$
73	72	abscld	$⊢ (φ \land ψ) \to \|(\frac{F (N) (Y) - F (N) (C)}{Y - C}) - {F (N)}_{S}^{'} (C)\| \in ℝ$
74	71 73	readdcld	$⊢ (φ \land ψ) \to \|(\frac{G (Y) - G (C)}{Y - C}) - (\frac{F (N) (Y) - F (N) (C)}{Y - C})\| + \|(\frac{F (N) (Y) - F (N) (C)}{Y - C}) - {F (N)}_{S}^{'} (C)\| \in ℝ$
75	59	rehalfcld	$⊢ (φ \land ψ) \to \frac{R}{2} \in ℝ$
76	53 58 69	abs3difd	$⊢ (φ \land ψ) \to \|(\frac{G (Y) - G (C)}{Y - C}) - {F (N)}_{S}^{'} (C)\| \leq \|(\frac{G (Y) - G (C)}{Y - C}) - (\frac{F (N) (Y) - F (N) (C)}{Y - C})\| + \|(\frac{F (N) (Y) - F (N) (C)}{Y - C}) - {F (N)}_{S}^{'} (C)\|$
77	75	rehalfcld	$⊢ (φ \land ψ) \to \frac{\frac{R}{2}}{2} \in ℝ$
78	22 66 23 67	sub4d	$⊢ (φ \land ψ) \to G (Y) - F (N) (Y) - (G (C) - F (N) (C)) = G (Y) - G (C) - (F (N) (Y) - F (N) (C))$
79	78	oveq1d	$⊢ (φ \land ψ) \to \frac{G (Y) - F (N) (Y) - (G (C) - F (N) (C))}{Y - C} = \frac{G (Y) - G (C) - (F (N) (Y) - F (N) (C))}{Y - C}$
80	24 68 51 52	divsubdird	$⊢ (φ \land ψ) \to \frac{G (Y) - G (C) - (F (N) (Y) - F (N) (C))}{Y - C} = (\frac{G (Y) - G (C)}{Y - C}) - (\frac{F (N) (Y) - F (N) (C)}{Y - C})$
81	79 80	eqtrd	$⊢ (φ \land ψ) \to \frac{G (Y) - F (N) (Y) - (G (C) - F (N) (C))}{Y - C} = (\frac{G (Y) - G (C)}{Y - C}) - (\frac{F (N) (Y) - F (N) (C)}{Y - C})$
82	81	fveq2d	$⊢ (φ \land ψ) \to \|\frac{G (Y) - F (N) (Y) - (G (C) - F (N) (C))}{Y - C}\| = \|(\frac{G (Y) - G (C)}{Y - C}) - (\frac{F (N) (Y) - F (N) (C)}{Y - C})\|$
83	22 66	subcld	$⊢ (φ \land ψ) \to G (Y) - F (N) (Y) \in ℂ$
84	23 67	subcld	$⊢ (φ \land ψ) \to G (C) - F (N) (C) \in ℂ$
85	83 84	subcld	$⊢ (φ \land ψ) \to G (Y) - F (N) (Y) - (G (C) - F (N) (C)) \in ℂ$
86	85 51 52	absdivd	$⊢ (φ \land ψ) \to \|\frac{G (Y) - F (N) (Y) - (G (C) - F (N) (C))}{Y - C}\| = \frac{\|G (Y) - F (N) (Y) - (G (C) - F (N) (C))\|}{\|Y - C\|}$
87	82 86	eqtr3d	$⊢ (φ \land ψ) \to \|(\frac{G (Y) - G (C)}{Y - C}) - (\frac{F (N) (Y) - F (N) (C)}{Y - C})\| = \frac{\|G (Y) - F (N) (Y) - (G (C) - F (N) (C))\|}{\|Y - C\|}$
88		eqid	$⊢ ℤ_{\geq N} = ℤ_{\geq N}$
89	15 1	eleqtrdi	$⊢ (φ \land ψ) \to N \in ℤ_{\geq M}$
90		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
91	89 90	syl	$⊢ (φ \land ψ) \to N \in ℤ$
92	3	adantr	$⊢ (φ \land ψ) \to M \in ℤ$
93		fveq2	$⊢ z = Y \to F (k) (z) = F (k) (Y)$
94	93	mpteq2dv	$⊢ z = Y \to (k \in Z ⟼ F (k) (z)) = (k \in Z ⟼ F (k) (Y))$
95		fveq2	$⊢ z = Y \to G (z) = G (Y)$
96	94 95	breq12d	$⊢ z = Y \to ((k \in Z ⟼ F (k) (z)) ⇝ G (z) \leftrightarrow (k \in Z ⟼ F (k) (Y)) ⇝ G (Y))$
97	6	ralrimiva	$⊢ φ \to \forall z \in X (k \in Z ⟼ F (k) (z)) ⇝ G (z)$
98	97	adantr	$⊢ (φ \land ψ) \to \forall z \in X (k \in Z ⟼ F (k) (z)) ⇝ G (z)$
99	96 98 18	rspcdva	$⊢ (φ \land ψ) \to (k \in Z ⟼ F (k) (Y)) ⇝ G (Y)$
100	1	fvexi	$⊢ Z \in V$
101	100	mptex	$⊢ (k \in Z ⟼ F (k) (Y) - F (N) (Y)) \in V$
102	101	a1i	$⊢ (φ \land ψ) \to (k \in Z ⟼ F (k) (Y) - F (N) (Y)) \in V$
103		fveq2	$⊢ k = n \to F (k) = F (n)$
104	103	fveq1d	$⊢ k = n \to F (k) (Y) = F (n) (Y)$
105		eqid	$⊢ (k \in Z ⟼ F (k) (Y)) = (k \in Z ⟼ F (k) (Y))$
106		fvex	$⊢ F (n) (Y) \in V$
107	104 105 106	fvmpt	$⊢ n \in Z \to (k \in Z ⟼ F (k) (Y)) (n) = F (n) (Y)$
108	107	adantl	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ F (k) (Y)) (n) = F (n) (Y)$
109	62	ffvelrnda	$⊢ ((φ \land ψ) \land n \in Z) \to F (n) \in (ℂ^{X})$
110		elmapi	$⊢ F (n) \in (ℂ^{X}) \to F (n) : X ⟶ ℂ$
111	109 110	syl	$⊢ ((φ \land ψ) \land n \in Z) \to F (n) : X ⟶ ℂ$
112	18	adantr	$⊢ ((φ \land ψ) \land n \in Z) \to Y \in X$
113	111 112	ffvelrnd	$⊢ ((φ \land ψ) \land n \in Z) \to F (n) (Y) \in ℂ$
114	108 113	eqeltrd	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ F (k) (Y)) (n) \in ℂ$
115	104	oveq1d	$⊢ k = n \to F (k) (Y) - F (N) (Y) = F (n) (Y) - F (N) (Y)$
116		eqid	$⊢ (k \in Z ⟼ F (k) (Y) - F (N) (Y)) = (k \in Z ⟼ F (k) (Y) - F (N) (Y))$
117		ovex	$⊢ F (n) (Y) - F (N) (Y) \in V$
118	115 116 117	fvmpt	$⊢ n \in Z \to (k \in Z ⟼ F (k) (Y) - F (N) (Y)) (n) = F (n) (Y) - F (N) (Y)$
119	118	adantl	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ F (k) (Y) - F (N) (Y)) (n) = F (n) (Y) - F (N) (Y)$
120	108	oveq1d	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ F (k) (Y)) (n) - F (N) (Y) = F (n) (Y) - F (N) (Y)$
121	119 120	eqtr4d	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ F (k) (Y) - F (N) (Y)) (n) = (k \in Z ⟼ F (k) (Y)) (n) - F (N) (Y)$
122	1 92 99 66 102 114 121	climsubc1	$⊢ (φ \land ψ) \to (k \in Z ⟼ F (k) (Y) - F (N) (Y)) ⇝ (G (Y) - F (N) (Y))$
123	100	mptex	$⊢ (k \in Z ⟼ F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))) \in V$
124	123	a1i	$⊢ (φ \land ψ) \to (k \in Z ⟼ F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))) \in V$
125		fveq2	$⊢ z = C \to F (k) (z) = F (k) (C)$
126	125	mpteq2dv	$⊢ z = C \to (k \in Z ⟼ F (k) (z)) = (k \in Z ⟼ F (k) (C))$
127		fveq2	$⊢ z = C \to G (z) = G (C)$
128	126 127	breq12d	$⊢ z = C \to ((k \in Z ⟼ F (k) (z)) ⇝ G (z) \leftrightarrow (k \in Z ⟼ F (k) (C)) ⇝ G (C))$
129	128 98 8	rspcdva	$⊢ (φ \land ψ) \to (k \in Z ⟼ F (k) (C)) ⇝ G (C)$
130	100	mptex	$⊢ (k \in Z ⟼ F (k) (C) - F (N) (C)) \in V$
131	130	a1i	$⊢ (φ \land ψ) \to (k \in Z ⟼ F (k) (C) - F (N) (C)) \in V$
132	103	fveq1d	$⊢ k = n \to F (k) (C) = F (n) (C)$
133		eqid	$⊢ (k \in Z ⟼ F (k) (C)) = (k \in Z ⟼ F (k) (C))$
134		fvex	$⊢ F (n) (C) \in V$
135	132 133 134	fvmpt	$⊢ n \in Z \to (k \in Z ⟼ F (k) (C)) (n) = F (n) (C)$
136	135	adantl	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ F (k) (C)) (n) = F (n) (C)$
137	8	adantr	$⊢ ((φ \land ψ) \land n \in Z) \to C \in X$
138	111 137	ffvelrnd	$⊢ ((φ \land ψ) \land n \in Z) \to F (n) (C) \in ℂ$
139	136 138	eqeltrd	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ F (k) (C)) (n) \in ℂ$
140	132	oveq1d	$⊢ k = n \to F (k) (C) - F (N) (C) = F (n) (C) - F (N) (C)$
141		eqid	$⊢ (k \in Z ⟼ F (k) (C) - F (N) (C)) = (k \in Z ⟼ F (k) (C) - F (N) (C))$
142		ovex	$⊢ F (n) (C) - F (N) (C) \in V$
143	140 141 142	fvmpt	$⊢ n \in Z \to (k \in Z ⟼ F (k) (C) - F (N) (C)) (n) = F (n) (C) - F (N) (C)$
144	143	adantl	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ F (k) (C) - F (N) (C)) (n) = F (n) (C) - F (N) (C)$
145	136	oveq1d	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ F (k) (C)) (n) - F (N) (C) = F (n) (C) - F (N) (C)$
146	144 145	eqtr4d	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ F (k) (C) - F (N) (C)) (n) = (k \in Z ⟼ F (k) (C)) (n) - F (N) (C)$
147	1 92 129 67 131 139 146	climsubc1	$⊢ (φ \land ψ) \to (k \in Z ⟼ F (k) (C) - F (N) (C)) ⇝ (G (C) - F (N) (C))$
148	66	adantr	$⊢ ((φ \land ψ) \land n \in Z) \to F (N) (Y) \in ℂ$
149	113 148	subcld	$⊢ ((φ \land ψ) \land n \in Z) \to F (n) (Y) - F (N) (Y) \in ℂ$
150	119 149	eqeltrd	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ F (k) (Y) - F (N) (Y)) (n) \in ℂ$
151	67	adantr	$⊢ ((φ \land ψ) \land n \in Z) \to F (N) (C) \in ℂ$
152	138 151	subcld	$⊢ ((φ \land ψ) \land n \in Z) \to F (n) (C) - F (N) (C) \in ℂ$
153	144 152	eqeltrd	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ F (k) (C) - F (N) (C)) (n) \in ℂ$
154	115 140	oveq12d	$⊢ k = n \to F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C)) = F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C))$
155		eqid	$⊢ (k \in Z ⟼ F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))) = (k \in Z ⟼ F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C)))$
156		ovex	$⊢ F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C)) \in V$
157	154 155 156	fvmpt	$⊢ n \in Z \to (k \in Z ⟼ F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))) (n) = F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C))$
158	157	adantl	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))) (n) = F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C))$
159	119 144	oveq12d	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ F (k) (Y) - F (N) (Y)) (n) - (k \in Z ⟼ F (k) (C) - F (N) (C)) (n) = F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C))$
160	158 159	eqtr4d	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))) (n) = (k \in Z ⟼ F (k) (Y) - F (N) (Y)) (n) - (k \in Z ⟼ F (k) (C) - F (N) (C)) (n)$
161	1 92 122 124 147 150 153 160	climsub	$⊢ (φ \land ψ) \to (k \in Z ⟼ F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))) ⇝ (G (Y) - F (N) (Y) - (G (C) - F (N) (C)))$
162	100	mptex	$⊢ (k \in Z ⟼ \|F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))\|) \in V$
163	162	a1i	$⊢ (φ \land ψ) \to (k \in Z ⟼ \|F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))\|) \in V$
164	149 152	subcld	$⊢ ((φ \land ψ) \land n \in Z) \to F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C)) \in ℂ$
165	158 164	eqeltrd	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))) (n) \in ℂ$
166	154	fveq2d	$⊢ k = n \to \|F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))\| = \|F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C))\|$
167		eqid	$⊢ (k \in Z ⟼ \|F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))\|) = (k \in Z ⟼ \|F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))\|)$
168		fvex	$⊢ \|F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C))\| \in V$
169	166 167 168	fvmpt	$⊢ n \in Z \to (k \in Z ⟼ \|F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))\|) (n) = \|F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C))\|$
170	169	adantl	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ \|F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))\|) (n) = \|F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C))\|$
171	158	fveq2d	$⊢ ((φ \land ψ) \land n \in Z) \to \|(k \in Z ⟼ F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))) (n)\| = \|F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C))\|$
172	170 171	eqtr4d	$⊢ ((φ \land ψ) \land n \in Z) \to (k \in Z ⟼ \|F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))\|) (n) = \|(k \in Z ⟼ F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))) (n)\|$
173	1 161 163 92 165 172	climabs	$⊢ (φ \land ψ) \to (k \in Z ⟼ \|F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))\|) ⇝ \|G (Y) - F (N) (Y) - (G (C) - F (N) (C))\|$
174	51	abscld	$⊢ (φ \land ψ) \to \|Y - C\| \in ℝ$
175	77 174	remulcld	$⊢ (φ \land ψ) \to (\frac{\frac{R}{2}}{2}) \|Y - C\| \in ℝ$
176	175	recnd	$⊢ (φ \land ψ) \to (\frac{\frac{R}{2}}{2}) \|Y - C\| \in ℂ$
177	1	eqimss2i	$⊢ ℤ_{\geq M} \subseteq Z$
178	177 100	climconst2	$⊢ ((\frac{\frac{R}{2}}{2}) \|Y - C\| \in ℂ \land M \in ℤ) \to (Z \times \{(\frac{\frac{R}{2}}{2}) \|Y - C\|\}) ⇝ (\frac{\frac{R}{2}}{2}) \|Y - C\|$
179	176 92 178	syl2anc	$⊢ (φ \land ψ) \to (Z \times \{(\frac{\frac{R}{2}}{2}) \|Y - C\|\}) ⇝ (\frac{\frac{R}{2}}{2}) \|Y - C\|$
180	1	uztrn2	$⊢ (N \in Z \land n \in ℤ_{\geq N}) \to n \in Z$
181	15 180	sylan	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to n \in Z$
182	181 169	syl	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to (k \in Z ⟼ \|F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))\|) (n) = \|F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C))\|$
183	164	abscld	$⊢ ((φ \land ψ) \land n \in Z) \to \|F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C))\| \in ℝ$
184	181 183	syldan	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to \|F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C))\| \in ℝ$
185	182 184	eqeltrd	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to (k \in Z ⟼ \|F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))\|) (n) \in ℝ$
186		ovex	$⊢ (\frac{\frac{R}{2}}{2}) \|Y - C\| \in V$
187	186	fvconst2	$⊢ n \in Z \to (Z \times \{(\frac{\frac{R}{2}}{2}) \|Y - C\|\}) (n) = (\frac{\frac{R}{2}}{2}) \|Y - C\|$
188	181 187	syl	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to (Z \times \{(\frac{\frac{R}{2}}{2}) \|Y - C\|\}) (n) = (\frac{\frac{R}{2}}{2}) \|Y - C\|$
189	175	adantr	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to (\frac{\frac{R}{2}}{2}) \|Y - C\| \in ℝ$
190	188 189	eqeltrd	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to (Z \times \{(\frac{\frac{R}{2}}{2}) \|Y - C\|\}) (n) \in ℝ$
191	181 111	syldan	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to F (n) : X ⟶ ℂ$
192	191	ffnd	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to F (n) Fn X$
193	65	adantr	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to F (N) : X ⟶ ℂ$
194	193	ffnd	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to F (N) Fn X$
195		ulmscl	$⊢ (k \in Z ⟼ S D F (k)) \underset{u}{⇝} (X) H \to X \in V$
196	7 195	syl	$⊢ φ \to X \in V$
197	196	ad2antrr	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to X \in V$
198	18	adantr	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to Y \in X$
199		fnfvof	$⊢ ((F (n) Fn X \land F (N) Fn X) \land (X \in V \land Y \in X)) \to (F (n) -_{f} F (N)) (Y) = F (n) (Y) - F (N) (Y)$
200	192 194 197 198 199	syl22anc	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to (F (n) -_{f} F (N)) (Y) = F (n) (Y) - F (N) (Y)$
201	8	adantr	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to C \in X$
202		fnfvof	$⊢ ((F (n) Fn X \land F (N) Fn X) \land (X \in V \land C \in X)) \to (F (n) -_{f} F (N)) (C) = F (n) (C) - F (N) (C)$
203	192 194 197 201 202	syl22anc	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to (F (n) -_{f} F (N)) (C) = F (n) (C) - F (N) (C)$
204	200 203	oveq12d	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to (F (n) -_{f} F (N)) (Y) - (F (n) -_{f} F (N)) (C) = F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C))$
205	204	fveq2d	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to \|(F (n) -_{f} F (N)) (Y) - (F (n) -_{f} F (N)) (C)\| = \|F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C))\|$
206	44 18	sseldd	$⊢ (φ \land ψ) \to Y \in S$
207	44 8	sseldd	$⊢ (φ \land ψ) \to C \in S$
208	206 207	ovresd	$⊢ (φ \land ψ) \to Y ({(abs \circ -) ↾}_{(S \times S)}) C = Y (abs \circ -) C$
209		eqid	$⊢ abs \circ - = abs \circ -$
210	209	cnmetdval	$⊢ (Y \in ℂ \land C \in ℂ) \to Y (abs \circ -) C = \|Y - C\|$
211	49 50 210	syl2anc	$⊢ (φ \land ψ) \to Y (abs \circ -) C = \|Y - C\|$
212	208 211	eqtrd	$⊢ (φ \land ψ) \to Y ({(abs \circ -) ↾}_{(S \times S)}) C = \|Y - C\|$
213	212 14	eqbrtrd	$⊢ (φ \land ψ) \to Y ({(abs \circ -) ↾}_{(S \times S)}) C < U$
214		cnxmet	$⊢ abs \circ - \in ∞Met (ℂ)$
215		xmetres2	$⊢ (abs \circ - \in ∞Met (ℂ) \land S \subseteq ℂ) \to {(abs \circ -) ↾}_{(S \times S)} \in ∞Met (S)$
216	214 47 215	sylancr	$⊢ (φ \land ψ) \to {(abs \circ -) ↾}_{(S \times S)} \in ∞Met (S)$
217	10	rpxrd	$⊢ (φ \land ψ) \to U \in ℝ^{*}$
218		elbl3	$⊢ (({(abs \circ -) ↾}_{(S \times S)} \in ∞Met (S) \land U \in ℝ^{*}) \land (C \in S \land Y \in S)) \to (Y \in (C ball ({(abs \circ -) ↾}_{(S \times S)}) U) \leftrightarrow Y ({(abs \circ -) ↾}_{(S \times S)}) C < U)$
219	216 217 207 206 218	syl22anc	$⊢ (φ \land ψ) \to (Y \in (C ball ({(abs \circ -) ↾}_{(S \times S)}) U) \leftrightarrow Y ({(abs \circ -) ↾}_{(S \times S)}) C < U)$
220	213 219	mpbird	$⊢ (φ \land ψ) \to Y \in (C ball ({(abs \circ -) ↾}_{(S \times S)}) U)$
221	220	adantr	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to Y \in (C ball ({(abs \circ -) ↾}_{(S \times S)}) U)$
222		blcntr	$⊢ ({(abs \circ -) ↾}_{(S \times S)} \in ∞Met (S) \land C \in S \land U \in ℝ^{+}) \to C \in (C ball ({(abs \circ -) ↾}_{(S \times S)}) U)$
223	216 207 10 222	syl3anc	$⊢ (φ \land ψ) \to C \in (C ball ({(abs \circ -) ↾}_{(S \times S)}) U)$
224	223	adantr	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to C \in (C ball ({(abs \circ -) ↾}_{(S \times S)}) U)$
225	221 224	jca	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to (Y \in (C ball ({(abs \circ -) ↾}_{(S \times S)}) U) \land C \in (C ball ({(abs \circ -) ↾}_{(S \times S)}) U))$
226	2	ad2antrr	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to S \in \{ℝ, ℂ\}$
227		eqid	$⊢ {(abs \circ -) ↾}_{(S \times S)} = {(abs \circ -) ↾}_{(S \times S)}$
228	44	adantr	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to X \subseteq S$
229		fvexd	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to F (n) (y) \in V$
230		fvexd	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to F (N) (y) \in V$
231	191	feqmptd	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to F (n) = (y \in X ⟼ F (n) (y))$
232	193	feqmptd	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to F (N) = (y \in X ⟼ F (N) (y))$
233	197 229 230 231 232	offval2	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to F (n) -_{f} F (N) = (y \in X ⟼ F (n) (y) - F (N) (y))$
234	191	ffvelrnda	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to F (n) (y) \in ℂ$
235	193	ffvelrnda	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to F (N) (y) \in ℂ$
236	234 235	subcld	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to F (n) (y) - F (N) (y) \in ℂ$
237	233 236	fmpt3d	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to (F (n) -_{f} F (N)) : X ⟶ ℂ$
238	207	adantr	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to C \in S$
239	217	adantr	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to U \in ℝ^{*}$
240		eqid	$⊢ C ball ({(abs \circ -) ↾}_{(S \times S)}) U = C ball ({(abs \circ -) ↾}_{(S \times S)}) U$
241	13	adantr	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to C ball ({(abs \circ -) ↾}_{(S \times S)}) U \subseteq X$
242	233	oveq2d	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to S D (F (n) -_{f} F (N)) = \frac{d (y \in X⟼ F (n) (y) - F (N) (y))}{d_{S} y}$
243		fvexd	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to {F (n)}_{S}^{'} (y) \in V$
244	231	oveq2d	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to S D F (n) = \frac{d (y \in X⟼ F (n) (y))}{d_{S} y}$
245	103	oveq2d	$⊢ k = n \to S D F (k) = S D F (n)$
246		ovex	$⊢ S D F (n) \in V$
247	245 27 246	fvmpt	$⊢ n \in Z \to (k \in Z ⟼ S D F (k)) (n) = S D F (n)$
248	181 247	syl	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to (k \in Z ⟼ S D F (k)) (n) = S D F (n)$
249	36	ad2antrr	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to (k \in Z ⟼ S D F (k)) : Z ⟶ ℂ^{X}$
250	249 181	ffvelrnd	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to (k \in Z ⟼ S D F (k)) (n) \in (ℂ^{X})$
251	248 250	eqeltrrd	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to S D F (n) \in (ℂ^{X})$
252		elmapi	$⊢ S D F (n) \in (ℂ^{X}) \to {F (n)}_{S}^{'} : X ⟶ ℂ$
253	251 252	syl	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to {F (n)}_{S}^{'} : X ⟶ ℂ$
254	253	feqmptd	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to S D F (n) = (y \in X ⟼ {F (n)}_{S}^{'} (y))$
255	244 254	eqtr3d	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to \frac{d (y \in X⟼ F (n) (y))}{d_{S} y} = (y \in X ⟼ {F (n)}_{S}^{'} (y))$
256		fvexd	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to {F (N)}_{S}^{'} (y) \in V$
257	232	oveq2d	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to S D F (N) = \frac{d (y \in X⟼ F (N) (y))}{d_{S} y}$
258	41	adantr	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to {F (N)}_{S}^{'} : X ⟶ ℂ$
259	258	feqmptd	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to S D F (N) = (y \in X ⟼ {F (N)}_{S}^{'} (y))$
260	257 259	eqtr3d	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to \frac{d (y \in X⟼ F (N) (y))}{d_{S} y} = (y \in X ⟼ {F (N)}_{S}^{'} (y))$
261	226 234 243 255 235 256 260	dvmptsub	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to \frac{d (y \in X⟼ F (n) (y) - F (N) (y))}{d_{S} y} = (y \in X ⟼ {F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y))$
262	242 261	eqtrd	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to S D (F (n) -_{f} F (N)) = (y \in X ⟼ {F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y))$
263	262	dmeqd	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to dom {(F (n) -_{f} F (N))}_{S}^{'} = dom (y \in X ⟼ {F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y))$
264		ovex	$⊢ {F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y) \in V$
265		eqid	$⊢ (y \in X ⟼ {F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y)) = (y \in X ⟼ {F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y))$
266	264 265	dmmpti	$⊢ dom (y \in X ⟼ {F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y)) = X$
267	263 266	eqtrdi	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to dom {(F (n) -_{f} F (N))}_{S}^{'} = X$
268	241 267	sseqtrrd	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to C ball ({(abs \circ -) ↾}_{(S \times S)}) U \subseteq dom {(F (n) -_{f} F (N))}_{S}^{'}$
269	77	adantr	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to \frac{\frac{R}{2}}{2} \in ℝ$
270	241	sselda	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in (C ball ({(abs \circ -) ↾}_{(S \times S)}) U)) \to y \in X$
271	262	fveq1d	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to {(F (n) -_{f} F (N))}_{S}^{'} (y) = (y \in X ⟼ {F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y)) (y)$
272	265	fvmpt2	$⊢ (y \in X \land {F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y) \in V) \to (y \in X ⟼ {F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y)) (y) = {F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y)$
273	264 272	mpan2	$⊢ y \in X \to (y \in X ⟼ {F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y)) (y) = {F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y)$
274	271 273	sylan9eq	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to {(F (n) -_{f} F (N))}_{S}^{'} (y) = {F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y)$
275	274	fveq2d	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to \|{(F (n) -_{f} F (N))}_{S}^{'} (y)\| = \|{F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y)\|$
276	264	a1i	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to {F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y) \in V$
277	226 236 276 261	dvmptcl	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to {F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y) \in ℂ$
278	277	abscld	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to \|{F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y)\| \in ℝ$
279	77	ad2antrr	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to \frac{\frac{R}{2}}{2} \in ℝ$
280	253	ffvelrnda	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to {F (n)}_{S}^{'} (y) \in ℂ$
281	258	ffvelrnda	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to {F (N)}_{S}^{'} (y) \in ℂ$
282	280 281	abssubd	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to \|{F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y)\| = \|{F (N)}_{S}^{'} (y) - {F (n)}_{S}^{'} (y)\|$
283		fveq2	$⊢ m = n \to F (m) = F (n)$
284	283	oveq2d	$⊢ m = n \to S D F (m) = S D F (n)$
285	284	fveq1d	$⊢ m = n \to {F (m)}_{S}^{'} (x) = {F (n)}_{S}^{'} (x)$
286	285	oveq2d	$⊢ m = n \to {F (N)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x) = {F (N)}_{S}^{'} (x) - {F (n)}_{S}^{'} (x)$
287	286	fveq2d	$⊢ m = n \to \|{F (N)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| = \|{F (N)}_{S}^{'} (x) - {F (n)}_{S}^{'} (x)\|$
288	287	breq1d	$⊢ m = n \to (\|{F (N)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{R}{2}}{2} \leftrightarrow \|{F (N)}_{S}^{'} (x) - {F (n)}_{S}^{'} (x)\| < \frac{\frac{R}{2}}{2})$
289	288	ralbidv	$⊢ m = n \to (\forall x \in X \|{F (N)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{R}{2}}{2} \leftrightarrow \forall x \in X \|{F (N)}_{S}^{'} (x) - {F (n)}_{S}^{'} (x)\| < \frac{\frac{R}{2}}{2})$
290	289	rspccva	$⊢ (\forall m \in ℤ_{\geq N} \forall x \in X \|{F (N)}_{S}^{'} (x) - {F (m)}_{S}^{'} (x)\| < \frac{\frac{R}{2}}{2} \land n \in ℤ_{\geq N}) \to \forall x \in X \|{F (N)}_{S}^{'} (x) - {F (n)}_{S}^{'} (x)\| < \frac{\frac{R}{2}}{2}$
291	16 290	sylan	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to \forall x \in X \|{F (N)}_{S}^{'} (x) - {F (n)}_{S}^{'} (x)\| < \frac{\frac{R}{2}}{2}$
292		fveq2	$⊢ x = y \to {F (N)}_{S}^{'} (x) = {F (N)}_{S}^{'} (y)$
293		fveq2	$⊢ x = y \to {F (n)}_{S}^{'} (x) = {F (n)}_{S}^{'} (y)$
294	292 293	oveq12d	$⊢ x = y \to {F (N)}_{S}^{'} (x) - {F (n)}_{S}^{'} (x) = {F (N)}_{S}^{'} (y) - {F (n)}_{S}^{'} (y)$
295	294	fveq2d	$⊢ x = y \to \|{F (N)}_{S}^{'} (x) - {F (n)}_{S}^{'} (x)\| = \|{F (N)}_{S}^{'} (y) - {F (n)}_{S}^{'} (y)\|$
296	295	breq1d	$⊢ x = y \to (\|{F (N)}_{S}^{'} (x) - {F (n)}_{S}^{'} (x)\| < \frac{\frac{R}{2}}{2} \leftrightarrow \|{F (N)}_{S}^{'} (y) - {F (n)}_{S}^{'} (y)\| < \frac{\frac{R}{2}}{2})$
297	296	rspccva	$⊢ (\forall x \in X \|{F (N)}_{S}^{'} (x) - {F (n)}_{S}^{'} (x)\| < \frac{\frac{R}{2}}{2} \land y \in X) \to \|{F (N)}_{S}^{'} (y) - {F (n)}_{S}^{'} (y)\| < \frac{\frac{R}{2}}{2}$
298	291 297	sylan	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to \|{F (N)}_{S}^{'} (y) - {F (n)}_{S}^{'} (y)\| < \frac{\frac{R}{2}}{2}$
299	282 298	eqbrtrd	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to \|{F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y)\| < \frac{\frac{R}{2}}{2}$
300	278 279 299	ltled	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to \|{F (n)}_{S}^{'} (y) - {F (N)}_{S}^{'} (y)\| \leq \frac{\frac{R}{2}}{2}$
301	275 300	eqbrtrd	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in X) \to \|{(F (n) -_{f} F (N))}_{S}^{'} (y)\| \leq \frac{\frac{R}{2}}{2}$
302	270 301	syldan	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land y \in (C ball ({(abs \circ -) ↾}_{(S \times S)}) U)) \to \|{(F (n) -_{f} F (N))}_{S}^{'} (y)\| \leq \frac{\frac{R}{2}}{2}$
303	226 227 228 237 238 239 240 268 269 302	dvlip2	$⊢ (((φ \land ψ) \land n \in ℤ_{\geq N}) \land (Y \in (C ball ({(abs \circ -) ↾}_{(S \times S)}) U) \land C \in (C ball ({(abs \circ -) ↾}_{(S \times S)}) U))) \to \|(F (n) -_{f} F (N)) (Y) - (F (n) -_{f} F (N)) (C)\| \leq (\frac{\frac{R}{2}}{2}) \|Y - C\|$
304	225 303	mpdan	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to \|(F (n) -_{f} F (N)) (Y) - (F (n) -_{f} F (N)) (C)\| \leq (\frac{\frac{R}{2}}{2}) \|Y - C\|$
305	205 304	eqbrtrrd	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to \|F (n) (Y) - F (N) (Y) - (F (n) (C) - F (N) (C))\| \leq (\frac{\frac{R}{2}}{2}) \|Y - C\|$
306	305 182 188	3brtr4d	$⊢ ((φ \land ψ) \land n \in ℤ_{\geq N}) \to (k \in Z ⟼ \|F (k) (Y) - F (N) (Y) - (F (k) (C) - F (N) (C))\|) (n) \leq (Z \times \{(\frac{\frac{R}{2}}{2}) \|Y - C\|\}) (n)$
307	88 91 173 179 185 190 306	climle	$⊢ (φ \land ψ) \to \|G (Y) - F (N) (Y) - (G (C) - F (N) (C))\| \leq (\frac{\frac{R}{2}}{2}) \|Y - C\|$
308	85	abscld	$⊢ (φ \land ψ) \to \|G (Y) - F (N) (Y) - (G (C) - F (N) (C))\| \in ℝ$
309	51 52	absrpcld	$⊢ (φ \land ψ) \to \|Y - C\| \in ℝ^{+}$
310	308 77 309	ledivmul2d	$⊢ (φ \land ψ) \to (\frac{\|G (Y) - F (N) (Y) - (G (C) - F (N) (C))\|}{\|Y - C\|} \leq \frac{\frac{R}{2}}{2} \leftrightarrow \|G (Y) - F (N) (Y) - (G (C) - F (N) (C))\| \leq (\frac{\frac{R}{2}}{2}) \|Y - C\|)$
311	307 310	mpbird	$⊢ (φ \land ψ) \to \frac{\|G (Y) - F (N) (Y) - (G (C) - F (N) (C))\|}{\|Y - C\|} \leq \frac{\frac{R}{2}}{2}$
312	87 311	eqbrtrd	$⊢ (φ \land ψ) \to \|(\frac{G (Y) - G (C)}{Y - C}) - (\frac{F (N) (Y) - F (N) (C)}{Y - C})\| \leq \frac{\frac{R}{2}}{2}$
313	10	rpred	$⊢ (φ \land ψ) \to U \in ℝ$
314	11	rpred	$⊢ (φ \land ψ) \to W \in ℝ$
315	174 313 314 14 12	lttrd	$⊢ (φ \land ψ) \to \|Y - C\| < W$
316	315 20	mpd	$⊢ (φ \land ψ) \to \|(\frac{F (N) (Y) - F (N) (C)}{Y - C}) - {F (N)}_{S}^{'} (C)\| < \frac{\frac{R}{2}}{2}$
317	71 73 77 77 312 316	leltaddd	$⊢ (φ \land ψ) \to \|(\frac{G (Y) - G (C)}{Y - C}) - (\frac{F (N) (Y) - F (N) (C)}{Y - C})\| + \|(\frac{F (N) (Y) - F (N) (C)}{Y - C}) - {F (N)}_{S}^{'} (C)\| < (\frac{\frac{R}{2}}{2}) + (\frac{\frac{R}{2}}{2})$
318	75	recnd	$⊢ (φ \land ψ) \to \frac{R}{2} \in ℂ$
319	318	2halvesd	$⊢ (φ \land ψ) \to (\frac{\frac{R}{2}}{2}) + (\frac{\frac{R}{2}}{2}) = \frac{R}{2}$
320	317 319	breqtrd	$⊢ (φ \land ψ) \to \|(\frac{G (Y) - G (C)}{Y - C}) - (\frac{F (N) (Y) - F (N) (C)}{Y - C})\| + \|(\frac{F (N) (Y) - F (N) (C)}{Y - C}) - {F (N)}_{S}^{'} (C)\| < \frac{R}{2}$
321	61 74 75 76 320	lelttrd	$⊢ (φ \land ψ) \to \|(\frac{G (Y) - G (C)}{Y - C}) - {F (N)}_{S}^{'} (C)\| < \frac{R}{2}$
322	53 57 58 59 321 17	abs3lemd	$⊢ (φ \land ψ) \to \|(\frac{G (Y) - G (C)}{Y - C}) - H (C)\| < R$

Metamath Proof Explorer

Theorem ulmdvlem1

Proof