ulmcn

Description: A uniform limit of continuous functions is continuous. (Contributed by Mario Carneiro, 27-Feb-2015)

	Ref	Expression
Hypotheses	ulmcn.z	$⊢ Z = ℤ_{\geq M}$
	ulmcn.m	$⊢ φ \to M \in ℤ$
	ulmcn.f	$⊢ φ \to F : Z ⟶ S \underset{cn}{⟶} ℂ$
	ulmcn.u	$⊢ φ \to F \underset{u}{⇝} (S) G$
Assertion	ulmcn	$⊢ φ \to G : S \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		ulmcn.z	$⊢ Z = ℤ_{\geq M}$
2		ulmcn.m	$⊢ φ \to M \in ℤ$
3		ulmcn.f	$⊢ φ \to F : Z ⟶ S \underset{cn}{⟶} ℂ$
4		ulmcn.u	$⊢ φ \to F \underset{u}{⇝} (S) G$
5		ulmcl	$⊢ F \underset{u}{⇝} (S) G \to G : S ⟶ ℂ$
6	4 5	syl	$⊢ φ \to G : S ⟶ ℂ$
7	2	adantr	$⊢ (φ \land (x \in S \land y \in ℝ^{+})) \to M \in ℤ$
8		cncff	$⊢ x : S \underset{cn}{⟶} ℂ \to x : S ⟶ ℂ$
9		cnex	$⊢ ℂ \in V$
10		cncfrss	$⊢ x : S \underset{cn}{⟶} ℂ \to S \subseteq ℂ$
11		ssexg	$⊢ (S \subseteq ℂ \land ℂ \in V) \to S \in V$
12	10 9 11	sylancl	$⊢ x : S \underset{cn}{⟶} ℂ \to S \in V$
13		elmapg	$⊢ (ℂ \in V \land S \in V) \to (x \in (ℂ^{S}) \leftrightarrow x : S ⟶ ℂ)$
14	9 12 13	sylancr	$⊢ x : S \underset{cn}{⟶} ℂ \to (x \in (ℂ^{S}) \leftrightarrow x : S ⟶ ℂ)$
15	8 14	mpbird	$⊢ x : S \underset{cn}{⟶} ℂ \to x \in (ℂ^{S})$
16	15	ssriv	$⊢ S \underset{cn}{⟶} ℂ \subseteq ℂ^{S}$
17		fss	$⊢ (F : Z ⟶ S \underset{cn}{⟶} ℂ \land S \underset{cn}{⟶} ℂ \subseteq ℂ^{S}) \to F : Z ⟶ ℂ^{S}$
18	3 16 17	sylancl	$⊢ φ \to F : Z ⟶ ℂ^{S}$
19	18	adantr	$⊢ (φ \land (x \in S \land y \in ℝ^{+})) \to F : Z ⟶ ℂ^{S}$
20		eqidd	$⊢ ((φ \land (x \in S \land y \in ℝ^{+})) \land (k \in Z \land w \in S)) \to F (k) (w) = F (k) (w)$
21		eqidd	$⊢ ((φ \land (x \in S \land y \in ℝ^{+})) \land w \in S) \to G (w) = G (w)$
22	4	adantr	$⊢ (φ \land (x \in S \land y \in ℝ^{+})) \to F \underset{u}{⇝} (S) G$
23		rphalfcl	$⊢ y \in ℝ^{+} \to \frac{y}{2} \in ℝ^{+}$
24	23	ad2antll	$⊢ (φ \land (x \in S \land y \in ℝ^{+})) \to \frac{y}{2} \in ℝ^{+}$
25	24	rphalfcld	$⊢ (φ \land (x \in S \land y \in ℝ^{+})) \to \frac{\frac{y}{2}}{2} \in ℝ^{+}$
26	1 7 19 20 21 22 25	ulmi	$⊢ (φ \land (x \in S \land y \in ℝ^{+})) \to \exists j \in Z \forall k \in ℤ_{\geq j} \forall w \in S \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2}$
27	1	r19.2uz	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} \forall w \in S \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2} \to \exists k \in Z \forall w \in S \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2}$
28		simplrl	$⊢ ((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \to x \in S$
29		fveq2	$⊢ w = x \to F (k) (w) = F (k) (x)$
30		fveq2	$⊢ w = x \to G (w) = G (x)$
31	29 30	oveq12d	$⊢ w = x \to F (k) (w) - G (w) = F (k) (x) - G (x)$
32	31	fveq2d	$⊢ w = x \to \|F (k) (w) - G (w)\| = \|F (k) (x) - G (x)\|$
33	32	breq1d	$⊢ w = x \to (\|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2} \leftrightarrow \|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2})$
34	33	rspcv	$⊢ x \in S \to (\forall w \in S \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2} \to \|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2})$
35	28 34	syl	$⊢ ((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \to (\forall w \in S \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2} \to \|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2})$
36	3	adantr	$⊢ (φ \land (x \in S \land y \in ℝ^{+})) \to F : Z ⟶ S \underset{cn}{⟶} ℂ$
37	36	ffvelrnda	$⊢ ((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \to F (k) : S \underset{cn}{⟶} ℂ$
38	24	adantr	$⊢ ((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \to \frac{y}{2} \in ℝ^{+}$
39		cncfi	$⊢ (F (k) : S \underset{cn}{⟶} ℂ \land x \in S \land \frac{y}{2} \in ℝ^{+}) \to \exists z \in ℝ^{+} \forall w \in S (\|w - x\| < z \to \|F (k) (w) - F (k) (x)\| < \frac{y}{2})$
40	37 28 38 39	syl3anc	$⊢ ((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \to \exists z \in ℝ^{+} \forall w \in S (\|w - x\| < z \to \|F (k) (w) - F (k) (x)\| < \frac{y}{2})$
41	40	ad2antrr	$⊢ ((((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land \forall w \in S \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2}) \land \|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2}) \to \exists z \in ℝ^{+} \forall w \in S (\|w - x\| < z \to \|F (k) (w) - F (k) (x)\| < \frac{y}{2})$
42		r19.26	$⊢ \forall w \in S (\|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2} \land (\|w - x\| < z \to \|F (k) (w) - F (k) (x)\| < \frac{y}{2})) \leftrightarrow (\forall w \in S \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2} \land \forall w \in S (\|w - x\| < z \to \|F (k) (w) - F (k) (x)\| < \frac{y}{2}))$
43	19	ad2antrr	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to F : Z ⟶ ℂ^{S}$
44		simplr	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to k \in Z$
45	43 44	ffvelrnd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to F (k) \in (ℂ^{S})$
46		elmapi	$⊢ F (k) \in (ℂ^{S}) \to F (k) : S ⟶ ℂ$
47	45 46	syl	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to F (k) : S ⟶ ℂ$
48	28	adantr	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to x \in S$
49	47 48	ffvelrnd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to F (k) (x) \in ℂ$
50	6	ad3antrrr	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to G : S ⟶ ℂ$
51	50 48	ffvelrnd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to G (x) \in ℂ$
52	49 51	subcld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to F (k) (x) - G (x) \in ℂ$
53	52	abscld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|F (k) (x) - G (x)\| \in ℝ$
54		ffvelrn	$⊢ (F (k) : S ⟶ ℂ \land w \in S) \to F (k) (w) \in ℂ$
55	47 54	sylancom	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to F (k) (w) \in ℂ$
56		ffvelrn	$⊢ (G : S ⟶ ℂ \land w \in S) \to G (w) \in ℂ$
57	50 56	sylancom	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to G (w) \in ℂ$
58	55 57	subcld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to F (k) (w) - G (w) \in ℂ$
59	58	abscld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|F (k) (w) - G (w)\| \in ℝ$
60	38	adantr	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \frac{y}{2} \in ℝ^{+}$
61	60	rphalfcld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \frac{\frac{y}{2}}{2} \in ℝ^{+}$
62	61	rpred	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \frac{\frac{y}{2}}{2} \in ℝ$
63		lt2add	$⊢ ((\|F (k) (x) - G (x)\| \in ℝ \land \|F (k) (w) - G (w)\| \in ℝ) \land (\frac{\frac{y}{2}}{2} \in ℝ \land \frac{\frac{y}{2}}{2} \in ℝ)) \to ((\|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2} \land \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2}) \to \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| < (\frac{\frac{y}{2}}{2}) + (\frac{\frac{y}{2}}{2}))$
64	53 59 62 62 63	syl22anc	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to ((\|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2} \land \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2}) \to \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| < (\frac{\frac{y}{2}}{2}) + (\frac{\frac{y}{2}}{2}))$
65	60	rpred	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \frac{y}{2} \in ℝ$
66	65	recnd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \frac{y}{2} \in ℂ$
67	66	2halvesd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to (\frac{\frac{y}{2}}{2}) + (\frac{\frac{y}{2}}{2}) = \frac{y}{2}$
68	67	breq2d	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to (\|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| < (\frac{\frac{y}{2}}{2}) + (\frac{\frac{y}{2}}{2}) \leftrightarrow \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| < \frac{y}{2})$
69	53 59	readdcld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| \in ℝ$
70	55 49	subcld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to F (k) (w) - F (k) (x) \in ℂ$
71	70	abscld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|F (k) (w) - F (k) (x)\| \in ℝ$
72		lt2add	$⊢ ((\|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| \in ℝ \land \|F (k) (w) - F (k) (x)\| \in ℝ) \land (\frac{y}{2} \in ℝ \land \frac{y}{2} \in ℝ)) \to ((\|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| < \frac{y}{2} \land \|F (k) (w) - F (k) (x)\| < \frac{y}{2}) \to \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\| < (\frac{y}{2}) + (\frac{y}{2}))$
73	69 71 65 65 72	syl22anc	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to ((\|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| < \frac{y}{2} \land \|F (k) (w) - F (k) (x)\| < \frac{y}{2}) \to \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\| < (\frac{y}{2}) + (\frac{y}{2}))$
74		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
75	74	ad2antll	$⊢ (φ \land (x \in S \land y \in ℝ^{+})) \to y \in ℝ$
76	75	ad2antrr	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to y \in ℝ$
77	76	recnd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to y \in ℂ$
78	77	2halvesd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to (\frac{y}{2}) + (\frac{y}{2}) = y$
79	78	breq2d	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to (\|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\| < (\frac{y}{2}) + (\frac{y}{2}) \leftrightarrow \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\| < y)$
80	57 51	subcld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to G (w) - G (x) \in ℂ$
81	80	abscld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|G (w) - G (x)\| \in ℝ$
82	57 49	subcld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to G (w) - F (k) (x) \in ℂ$
83	82	abscld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|G (w) - F (k) (x)\| \in ℝ$
84	53 83	readdcld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|F (k) (x) - G (x)\| + \|G (w) - F (k) (x)\| \in ℝ$
85	69 71	readdcld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\| \in ℝ$
86	57 51 49	abs3difd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|G (w) - G (x)\| \leq \|G (w) - F (k) (x)\| + \|F (k) (x) - G (x)\|$
87	83	recnd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|G (w) - F (k) (x)\| \in ℂ$
88	53	recnd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|F (k) (x) - G (x)\| \in ℂ$
89	87 88	addcomd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|G (w) - F (k) (x)\| + \|F (k) (x) - G (x)\| = \|F (k) (x) - G (x)\| + \|G (w) - F (k) (x)\|$
90	86 89	breqtrd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|G (w) - G (x)\| \leq \|F (k) (x) - G (x)\| + \|G (w) - F (k) (x)\|$
91	59 71	readdcld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\| \in ℝ$
92	57 49 55	abs3difd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|G (w) - F (k) (x)\| \leq \|G (w) - F (k) (w)\| + \|F (k) (w) - F (k) (x)\|$
93	57 55	abssubd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|G (w) - F (k) (w)\| = \|F (k) (w) - G (w)\|$
94	93	oveq1d	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|G (w) - F (k) (w)\| + \|F (k) (w) - F (k) (x)\| = \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\|$
95	92 94	breqtrd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|G (w) - F (k) (x)\| \leq \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\|$
96	83 91 53 95	leadd2dd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|F (k) (x) - G (x)\| + \|G (w) - F (k) (x)\| \leq \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\|$
97	59	recnd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|F (k) (w) - G (w)\| \in ℂ$
98	71	recnd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|F (k) (w) - F (k) (x)\| \in ℂ$
99	88 97 98	addassd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\| = \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\|$
100	96 99	breqtrrd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|F (k) (x) - G (x)\| + \|G (w) - F (k) (x)\| \leq \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\|$
101	81 84 85 90 100	letrd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to \|G (w) - G (x)\| \leq \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\|$
102		lelttr	$⊢ (\|G (w) - G (x)\| \in ℝ \land \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\| \in ℝ \land y \in ℝ) \to ((\|G (w) - G (x)\| \leq \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\| \land \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\| < y) \to \|G (w) - G (x)\| < y)$
103	81 85 76 102	syl3anc	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to ((\|G (w) - G (x)\| \leq \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\| \land \|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\| < y) \to \|G (w) - G (x)\| < y)$
104	101 103	mpand	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to (\|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\| < y \to \|G (w) - G (x)\| < y)$
105	79 104	sylbid	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to (\|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| + \|F (k) (w) - F (k) (x)\| < (\frac{y}{2}) + (\frac{y}{2}) \to \|G (w) - G (x)\| < y)$
106	73 105	syld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to ((\|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| < \frac{y}{2} \land \|F (k) (w) - F (k) (x)\| < \frac{y}{2}) \to \|G (w) - G (x)\| < y)$
107	106	expd	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to (\|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| < \frac{y}{2} \to (\|F (k) (w) - F (k) (x)\| < \frac{y}{2} \to \|G (w) - G (x)\| < y))$
108	68 107	sylbid	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to (\|F (k) (x) - G (x)\| + \|F (k) (w) - G (w)\| < (\frac{\frac{y}{2}}{2}) + (\frac{\frac{y}{2}}{2}) \to (\|F (k) (w) - F (k) (x)\| < \frac{y}{2} \to \|G (w) - G (x)\| < y))$
109	64 108	syld	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \to ((\|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2} \land \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2}) \to (\|F (k) (w) - F (k) (x)\| < \frac{y}{2} \to \|G (w) - G (x)\| < y))$
110	109	expdimp	$⊢ ((((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land w \in S) \land \|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2}) \to (\|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2} \to (\|F (k) (w) - F (k) (x)\| < \frac{y}{2} \to \|G (w) - G (x)\| < y))$
111	110	an32s	$⊢ ((((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land \|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2}) \land w \in S) \to (\|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2} \to (\|F (k) (w) - F (k) (x)\| < \frac{y}{2} \to \|G (w) - G (x)\| < y))$
112	111	imp	$⊢ (((((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land \|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2}) \land w \in S) \land \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2}) \to (\|F (k) (w) - F (k) (x)\| < \frac{y}{2} \to \|G (w) - G (x)\| < y)$
113	112	imim2d	$⊢ (((((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land \|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2}) \land w \in S) \land \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2}) \to ((\|w - x\| < z \to \|F (k) (w) - F (k) (x)\| < \frac{y}{2}) \to (\|w - x\| < z \to \|G (w) - G (x)\| < y))$
114	113	expimpd	$⊢ ((((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land \|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2}) \land w \in S) \to ((\|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2} \land (\|w - x\| < z \to \|F (k) (w) - F (k) (x)\| < \frac{y}{2})) \to (\|w - x\| < z \to \|G (w) - G (x)\| < y))$
115	114	ralimdva	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land \|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2}) \to (\forall w \in S (\|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2} \land (\|w - x\| < z \to \|F (k) (w) - F (k) (x)\| < \frac{y}{2})) \to \forall w \in S (\|w - x\| < z \to \|G (w) - G (x)\| < y))$
116	42 115	syl5bir	$⊢ (((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land \|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2}) \to ((\forall w \in S \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2} \land \forall w \in S (\|w - x\| < z \to \|F (k) (w) - F (k) (x)\| < \frac{y}{2})) \to \forall w \in S (\|w - x\| < z \to \|G (w) - G (x)\| < y))$
117	116	expdimp	$⊢ ((((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land \|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2}) \land \forall w \in S \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2}) \to (\forall w \in S (\|w - x\| < z \to \|F (k) (w) - F (k) (x)\| < \frac{y}{2}) \to \forall w \in S (\|w - x\| < z \to \|G (w) - G (x)\| < y))$
118	117	an32s	$⊢ ((((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land \forall w \in S \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2}) \land \|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2}) \to (\forall w \in S (\|w - x\| < z \to \|F (k) (w) - F (k) (x)\| < \frac{y}{2}) \to \forall w \in S (\|w - x\| < z \to \|G (w) - G (x)\| < y))$
119	118	reximdv	$⊢ ((((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land \forall w \in S \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2}) \land \|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2}) \to (\exists z \in ℝ^{+} \forall w \in S (\|w - x\| < z \to \|F (k) (w) - F (k) (x)\| < \frac{y}{2}) \to \exists z \in ℝ^{+} \forall w \in S (\|w - x\| < z \to \|G (w) - G (x)\| < y))$
120	41 119	mpd	$⊢ ((((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \land \forall w \in S \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2}) \land \|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2}) \to \exists z \in ℝ^{+} \forall w \in S (\|w - x\| < z \to \|G (w) - G (x)\| < y)$
121	120	exp31	$⊢ ((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \to (\forall w \in S \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2} \to (\|F (k) (x) - G (x)\| < \frac{\frac{y}{2}}{2} \to \exists z \in ℝ^{+} \forall w \in S (\|w - x\| < z \to \|G (w) - G (x)\| < y)))$
122	35 121	mpdd	$⊢ ((φ \land (x \in S \land y \in ℝ^{+})) \land k \in Z) \to (\forall w \in S \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2} \to \exists z \in ℝ^{+} \forall w \in S (\|w - x\| < z \to \|G (w) - G (x)\| < y))$
123	122	rexlimdva	$⊢ (φ \land (x \in S \land y \in ℝ^{+})) \to (\exists k \in Z \forall w \in S \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2} \to \exists z \in ℝ^{+} \forall w \in S (\|w - x\| < z \to \|G (w) - G (x)\| < y))$
124	27 123	syl5	$⊢ (φ \land (x \in S \land y \in ℝ^{+})) \to (\exists j \in Z \forall k \in ℤ_{\geq j} \forall w \in S \|F (k) (w) - G (w)\| < \frac{\frac{y}{2}}{2} \to \exists z \in ℝ^{+} \forall w \in S (\|w - x\| < z \to \|G (w) - G (x)\| < y))$
125	26 124	mpd	$⊢ (φ \land (x \in S \land y \in ℝ^{+})) \to \exists z \in ℝ^{+} \forall w \in S (\|w - x\| < z \to \|G (w) - G (x)\| < y)$
126	125	ralrimivva	$⊢ φ \to \forall x \in S \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in S (\|w - x\| < z \to \|G (w) - G (x)\| < y)$
127		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
128	2 127	syl	$⊢ φ \to M \in ℤ_{\geq M}$
129	128 1	eleqtrrdi	$⊢ φ \to M \in Z$
130	3 129	ffvelrnd	$⊢ φ \to F (M) : S \underset{cn}{⟶} ℂ$
131		cncfrss	$⊢ F (M) : S \underset{cn}{⟶} ℂ \to S \subseteq ℂ$
132	130 131	syl	$⊢ φ \to S \subseteq ℂ$
133		ssid	$⊢ ℂ \subseteq ℂ$
134		elcncf2	$⊢ (S \subseteq ℂ \land ℂ \subseteq ℂ) \to (G : S \underset{cn}{⟶} ℂ \leftrightarrow (G : S ⟶ ℂ \land \forall x \in S \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in S (\|w - x\| < z \to \|G (w) - G (x)\| < y)))$
135	132 133 134	sylancl	$⊢ φ \to (G : S \underset{cn}{⟶} ℂ \leftrightarrow (G : S ⟶ ℂ \land \forall x \in S \forall y \in ℝ^{+} \exists z \in ℝ^{+} \forall w \in S (\|w - x\| < z \to \|G (w) - G (x)\| < y)))$
136	6 126 135	mpbir2and	$⊢ φ \to G : S \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem ulmcn

Proof