cncfperiod

Description: A periodic continuous function stays continuous if the domain is shifted a period. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	cncfperiod.a	$⊢ φ \to A \subseteq ℂ$
	cncfperiod.t	$⊢ φ \to T \in ℝ$
	cncfperiod.b	$⊢ B = \{x \in ℂ \| \exists y \in A x = y + T\}$
	cncfperiod.f	$⊢ φ \to F : dom F ⟶ ℂ$
	cncfperiod.cssdmf	$⊢ φ \to B \subseteq dom F$
	cncfperiod.fper	$⊢ (φ \land x \in A) \to F (x + T) = F (x)$
	cncfperiod.fcn	$⊢ φ \to ({F ↾}_{A}) : A \underset{cn}{⟶} ℂ$
Assertion	cncfperiod	$⊢ φ \to ({F ↾}_{B}) : B \underset{cn}{⟶} ℂ$

Proof

Step	Hyp	Ref	Expression
1		cncfperiod.a	$⊢ φ \to A \subseteq ℂ$
2		cncfperiod.t	$⊢ φ \to T \in ℝ$
3		cncfperiod.b	$⊢ B = \{x \in ℂ \| \exists y \in A x = y + T\}$
4		cncfperiod.f	$⊢ φ \to F : dom F ⟶ ℂ$
5		cncfperiod.cssdmf	$⊢ φ \to B \subseteq dom F$
6		cncfperiod.fper	$⊢ (φ \land x \in A) \to F (x + T) = F (x)$
7		cncfperiod.fcn	$⊢ φ \to ({F ↾}_{A}) : A \underset{cn}{⟶} ℂ$
8	4 5	fssresd	$⊢ φ \to ({F ↾}_{B}) : B ⟶ ℂ$
9		fvoveq1	$⊢ a = x - T \to \|a - b\| = \|x - T - b\|$
10	9	breq1d	$⊢ a = x - T \to (\|a - b\| < z \leftrightarrow \|x - T - b\| < z)$
11	10	imbrov2fvoveq	$⊢ a = x - T \to ((\|a - b\| < z \to \|({F ↾}_{A}) (a) - ({F ↾}_{A}) (b)\| < w) \leftrightarrow (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w))$
12	11	rexralbidv	$⊢ a = x - T \to (\exists z \in ℝ^{+} \forall b \in A (\|a - b\| < z \to \|({F ↾}_{A}) (a) - ({F ↾}_{A}) (b)\| < w) \leftrightarrow \exists z \in ℝ^{+} \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w))$
13	12	ralbidv	$⊢ a = x - T \to (\forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall b \in A (\|a - b\| < z \to \|({F ↾}_{A}) (a) - ({F ↾}_{A}) (b)\| < w) \leftrightarrow \forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w))$
14	7	adantr	$⊢ (φ \land x \in B) \to ({F ↾}_{A}) : A \underset{cn}{⟶} ℂ$
15	1	adantr	$⊢ (φ \land x \in B) \to A \subseteq ℂ$
16		ssidd	$⊢ (φ \land x \in B) \to ℂ \subseteq ℂ$
17		elcncf	$⊢ (A \subseteq ℂ \land ℂ \subseteq ℂ) \to (({F ↾}_{A}) : A \underset{cn}{⟶} ℂ \leftrightarrow (({F ↾}_{A}) : A ⟶ ℂ \land \forall a \in A \forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall b \in A (\|a - b\| < z \to \|({F ↾}_{A}) (a) - ({F ↾}_{A}) (b)\| < w)))$
18	15 16 17	syl2anc	$⊢ (φ \land x \in B) \to (({F ↾}_{A}) : A \underset{cn}{⟶} ℂ \leftrightarrow (({F ↾}_{A}) : A ⟶ ℂ \land \forall a \in A \forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall b \in A (\|a - b\| < z \to \|({F ↾}_{A}) (a) - ({F ↾}_{A}) (b)\| < w)))$
19	14 18	mpbid	$⊢ (φ \land x \in B) \to (({F ↾}_{A}) : A ⟶ ℂ \land \forall a \in A \forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall b \in A (\|a - b\| < z \to \|({F ↾}_{A}) (a) - ({F ↾}_{A}) (b)\| < w))$
20	19	simprd	$⊢ (φ \land x \in B) \to \forall a \in A \forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall b \in A (\|a - b\| < z \to \|({F ↾}_{A}) (a) - ({F ↾}_{A}) (b)\| < w)$
21		simpr	$⊢ (φ \land x \in B) \to x \in B$
22	21 3	eleqtrdi	$⊢ (φ \land x \in B) \to x \in \{x \in ℂ \| \exists y \in A x = y + T\}$
23		rabid	$⊢ x \in \{x \in ℂ \| \exists y \in A x = y + T\} \leftrightarrow (x \in ℂ \land \exists y \in A x = y + T)$
24	22 23	sylib	$⊢ (φ \land x \in B) \to (x \in ℂ \land \exists y \in A x = y + T)$
25	24	simprd	$⊢ (φ \land x \in B) \to \exists y \in A x = y + T$
26		oveq1	$⊢ x = y + T \to x - T = y + T - T$
27	26	3ad2ant3	$⊢ ((φ \land x \in B) \land y \in A \land x = y + T) \to x - T = y + T - T$
28	1	sselda	$⊢ (φ \land y \in A) \to y \in ℂ$
29	2	recnd	$⊢ φ \to T \in ℂ$
30	29	adantr	$⊢ (φ \land y \in A) \to T \in ℂ$
31	28 30	pncand	$⊢ (φ \land y \in A) \to y + T - T = y$
32	31	adantlr	$⊢ ((φ \land x \in B) \land y \in A) \to y + T - T = y$
33	32	3adant3	$⊢ ((φ \land x \in B) \land y \in A \land x = y + T) \to y + T - T = y$
34	27 33	eqtrd	$⊢ ((φ \land x \in B) \land y \in A \land x = y + T) \to x - T = y$
35		simp2	$⊢ ((φ \land x \in B) \land y \in A \land x = y + T) \to y \in A$
36	34 35	eqeltrd	$⊢ ((φ \land x \in B) \land y \in A \land x = y + T) \to x - T \in A$
37	36	rexlimdv3a	$⊢ (φ \land x \in B) \to (\exists y \in A x = y + T \to x - T \in A)$
38	25 37	mpd	$⊢ (φ \land x \in B) \to x - T \in A$
39	13 20 38	rspcdva	$⊢ (φ \land x \in B) \to \forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)$
40	39	adantrr	$⊢ (φ \land (x \in B \land w \in ℝ^{+})) \to \forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)$
41		simprr	$⊢ (φ \land (x \in B \land w \in ℝ^{+})) \to w \in ℝ^{+}$
42		rspa	$⊢ (\forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w) \land w \in ℝ^{+}) \to \exists z \in ℝ^{+} \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)$
43	40 41 42	syl2anc	$⊢ (φ \land (x \in B \land w \in ℝ^{+})) \to \exists z \in ℝ^{+} \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)$
44		simpl1l	$⊢ (((φ \land (x \in B \land w \in ℝ^{+})) \land z \in ℝ^{+} \land \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)) \land v \in B) \to φ$
45	44	adantr	$⊢ ((((φ \land (x \in B \land w \in ℝ^{+})) \land z \in ℝ^{+} \land \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)) \land v \in B) \land \|x - v\| < z) \to φ$
46		simp1rl	$⊢ ((φ \land (x \in B \land w \in ℝ^{+})) \land z \in ℝ^{+} \land \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)) \to x \in B$
47	46	adantr	$⊢ (((φ \land (x \in B \land w \in ℝ^{+})) \land z \in ℝ^{+} \land \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)) \land v \in B) \to x \in B$
48	47	adantr	$⊢ ((((φ \land (x \in B \land w \in ℝ^{+})) \land z \in ℝ^{+} \land \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)) \land v \in B) \land \|x - v\| < z) \to x \in B$
49		simplr	$⊢ ((((φ \land (x \in B \land w \in ℝ^{+})) \land z \in ℝ^{+} \land \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)) \land v \in B) \land \|x - v\| < z) \to v \in B$
50		fvres	$⊢ x \in B \to ({F ↾}_{B}) (x) = F (x)$
51	50	adantl	$⊢ (φ \land x \in B) \to ({F ↾}_{B}) (x) = F (x)$
52	3	ssrab3	$⊢ B \subseteq ℂ$
53	52	sseli	$⊢ x \in B \to x \in ℂ$
54	53	adantl	$⊢ (φ \land x \in B) \to x \in ℂ$
55	29	adantr	$⊢ (φ \land x \in B) \to T \in ℂ$
56	54 55	npcand	$⊢ (φ \land x \in B) \to x - T + T = x$
57	56	eqcomd	$⊢ (φ \land x \in B) \to x = x - T + T$
58	57	fveq2d	$⊢ (φ \land x \in B) \to F (x) = F (x - T + T)$
59		simpl	$⊢ (φ \land x \in B) \to φ$
60	59 38	jca	$⊢ (φ \land x \in B) \to (φ \land x - T \in A)$
61		eleq1	$⊢ y = x - T \to (y \in A \leftrightarrow x - T \in A)$
62	61	anbi2d	$⊢ y = x - T \to ((φ \land y \in A) \leftrightarrow (φ \land x - T \in A))$
63		fvoveq1	$⊢ y = x - T \to F (y + T) = F (x - T + T)$
64		fveq2	$⊢ y = x - T \to F (y) = F (x - T)$
65	63 64	eqeq12d	$⊢ y = x - T \to (F (y + T) = F (y) \leftrightarrow F (x - T + T) = F (x - T))$
66	62 65	imbi12d	$⊢ y = x - T \to (((φ \land y \in A) \to F (y + T) = F (y)) \leftrightarrow ((φ \land x - T \in A) \to F (x - T + T) = F (x - T)))$
67		eleq1	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
68	67	anbi2d	$⊢ x = y \to ((φ \land x \in A) \leftrightarrow (φ \land y \in A))$
69		fvoveq1	$⊢ x = y \to F (x + T) = F (y + T)$
70		fveq2	$⊢ x = y \to F (x) = F (y)$
71	69 70	eqeq12d	$⊢ x = y \to (F (x + T) = F (x) \leftrightarrow F (y + T) = F (y))$
72	68 71	imbi12d	$⊢ x = y \to (((φ \land x \in A) \to F (x + T) = F (x)) \leftrightarrow ((φ \land y \in A) \to F (y + T) = F (y)))$
73	72 6	chvarvv	$⊢ (φ \land y \in A) \to F (y + T) = F (y)$
74	66 73	vtoclg	$⊢ x - T \in A \to ((φ \land x - T \in A) \to F (x - T + T) = F (x - T))$
75	38 60 74	sylc	$⊢ (φ \land x \in B) \to F (x - T + T) = F (x - T)$
76	38	fvresd	$⊢ (φ \land x \in B) \to ({F ↾}_{A}) (x - T) = F (x - T)$
77	75 76	eqtr4d	$⊢ (φ \land x \in B) \to F (x - T + T) = ({F ↾}_{A}) (x - T)$
78	51 58 77	3eqtrd	$⊢ (φ \land x \in B) \to ({F ↾}_{B}) (x) = ({F ↾}_{A}) (x - T)$
79	78	3adant3	$⊢ (φ \land x \in B \land v \in B) \to ({F ↾}_{B}) (x) = ({F ↾}_{A}) (x - T)$
80		eleq1	$⊢ x = v \to (x \in B \leftrightarrow v \in B)$
81	80	anbi2d	$⊢ x = v \to ((φ \land x \in B) \leftrightarrow (φ \land v \in B))$
82		fveq2	$⊢ x = v \to ({F ↾}_{B}) (x) = ({F ↾}_{B}) (v)$
83		fvoveq1	$⊢ x = v \to ({F ↾}_{A}) (x - T) = ({F ↾}_{A}) (v - T)$
84	82 83	eqeq12d	$⊢ x = v \to (({F ↾}_{B}) (x) = ({F ↾}_{A}) (x - T) \leftrightarrow ({F ↾}_{B}) (v) = ({F ↾}_{A}) (v - T))$
85	81 84	imbi12d	$⊢ x = v \to (((φ \land x \in B) \to ({F ↾}_{B}) (x) = ({F ↾}_{A}) (x - T)) \leftrightarrow ((φ \land v \in B) \to ({F ↾}_{B}) (v) = ({F ↾}_{A}) (v - T)))$
86	85 78	chvarvv	$⊢ (φ \land v \in B) \to ({F ↾}_{B}) (v) = ({F ↾}_{A}) (v - T)$
87	86	3adant2	$⊢ (φ \land x \in B \land v \in B) \to ({F ↾}_{B}) (v) = ({F ↾}_{A}) (v - T)$
88	79 87	oveq12d	$⊢ (φ \land x \in B \land v \in B) \to ({F ↾}_{B}) (x) - ({F ↾}_{B}) (v) = ({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (v - T)$
89	88	fveq2d	$⊢ (φ \land x \in B \land v \in B) \to \|({F ↾}_{B}) (x) - ({F ↾}_{B}) (v)\| = \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (v - T)\|$
90	45 48 49 89	syl3anc	$⊢ ((((φ \land (x \in B \land w \in ℝ^{+})) \land z \in ℝ^{+} \land \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)) \land v \in B) \land \|x - v\| < z) \to \|({F ↾}_{B}) (x) - ({F ↾}_{B}) (v)\| = \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (v - T)\|$
91		simpr	$⊢ ((((φ \land (x \in B \land w \in ℝ^{+})) \land z \in ℝ^{+} \land \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)) \land v \in B) \land \|x - v\| < z) \to \|x - v\| < z$
92	24	simpld	$⊢ (φ \land x \in B) \to x \in ℂ$
93	92	adantr	$⊢ ((φ \land x \in B) \land v \in B) \to x \in ℂ$
94	52	sseli	$⊢ v \in B \to v \in ℂ$
95	94	adantl	$⊢ ((φ \land x \in B) \land v \in B) \to v \in ℂ$
96	55	adantr	$⊢ ((φ \land x \in B) \land v \in B) \to T \in ℂ$
97	93 95 96	nnncan2d	$⊢ ((φ \land x \in B) \land v \in B) \to x - T - (v - T) = x - v$
98	97	fveq2d	$⊢ ((φ \land x \in B) \land v \in B) \to \|x - T - (v - T)\| = \|x - v\|$
99	98	adantr	$⊢ (((φ \land x \in B) \land v \in B) \land \|x - v\| < z) \to \|x - T - (v - T)\| = \|x - v\|$
100		simpr	$⊢ (((φ \land x \in B) \land v \in B) \land \|x - v\| < z) \to \|x - v\| < z$
101	99 100	eqbrtrd	$⊢ (((φ \land x \in B) \land v \in B) \land \|x - v\| < z) \to \|x - T - (v - T)\| < z$
102	45 48 49 91 101	syl1111anc	$⊢ ((((φ \land (x \in B \land w \in ℝ^{+})) \land z \in ℝ^{+} \land \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)) \land v \in B) \land \|x - v\| < z) \to \|x - T - (v - T)\| < z$
103		oveq2	$⊢ b = v - T \to x - T - b = x - T - (v - T)$
104	103	fveq2d	$⊢ b = v - T \to \|x - T - b\| = \|x - T - (v - T)\|$
105	104	breq1d	$⊢ b = v - T \to (\|x - T - b\| < z \leftrightarrow \|x - T - (v - T)\| < z)$
106		fveq2	$⊢ b = v - T \to ({F ↾}_{A}) (b) = ({F ↾}_{A}) (v - T)$
107	106	oveq2d	$⊢ b = v - T \to ({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b) = ({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (v - T)$
108	107	fveq2d	$⊢ b = v - T \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| = \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (v - T)\|$
109	108	breq1d	$⊢ b = v - T \to (\|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w \leftrightarrow \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (v - T)\| < w)$
110	105 109	imbi12d	$⊢ b = v - T \to ((\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w) \leftrightarrow (\|x - T - (v - T)\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (v - T)\| < w))$
111		simpll3	$⊢ ((((φ \land (x \in B \land w \in ℝ^{+})) \land z \in ℝ^{+} \land \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)) \land v \in B) \land \|x - v\| < z) \to \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)$
112		oveq1	$⊢ x = v \to x - T = v - T$
113	112	eleq1d	$⊢ x = v \to (x - T \in A \leftrightarrow v - T \in A)$
114	81 113	imbi12d	$⊢ x = v \to (((φ \land x \in B) \to x - T \in A) \leftrightarrow ((φ \land v \in B) \to v - T \in A))$
115	114 38	chvarvv	$⊢ (φ \land v \in B) \to v - T \in A$
116	45 49 115	syl2anc	$⊢ ((((φ \land (x \in B \land w \in ℝ^{+})) \land z \in ℝ^{+} \land \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)) \land v \in B) \land \|x - v\| < z) \to v - T \in A$
117	110 111 116	rspcdva	$⊢ ((((φ \land (x \in B \land w \in ℝ^{+})) \land z \in ℝ^{+} \land \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)) \land v \in B) \land \|x - v\| < z) \to (\|x - T - (v - T)\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (v - T)\| < w)$
118	102 117	mpd	$⊢ ((((φ \land (x \in B \land w \in ℝ^{+})) \land z \in ℝ^{+} \land \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)) \land v \in B) \land \|x - v\| < z) \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (v - T)\| < w$
119	90 118	eqbrtrd	$⊢ ((((φ \land (x \in B \land w \in ℝ^{+})) \land z \in ℝ^{+} \land \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)) \land v \in B) \land \|x - v\| < z) \to \|({F ↾}_{B}) (x) - ({F ↾}_{B}) (v)\| < w$
120	119	ex	$⊢ (((φ \land (x \in B \land w \in ℝ^{+})) \land z \in ℝ^{+} \land \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)) \land v \in B) \to (\|x - v\| < z \to \|({F ↾}_{B}) (x) - ({F ↾}_{B}) (v)\| < w)$
121	120	ralrimiva	$⊢ ((φ \land (x \in B \land w \in ℝ^{+})) \land z \in ℝ^{+} \land \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w)) \to \forall v \in B (\|x - v\| < z \to \|({F ↾}_{B}) (x) - ({F ↾}_{B}) (v)\| < w)$
122	121	3exp	$⊢ (φ \land (x \in B \land w \in ℝ^{+})) \to (z \in ℝ^{+} \to (\forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w) \to \forall v \in B (\|x - v\| < z \to \|({F ↾}_{B}) (x) - ({F ↾}_{B}) (v)\| < w)))$
123	122	reximdvai	$⊢ (φ \land (x \in B \land w \in ℝ^{+})) \to (\exists z \in ℝ^{+} \forall b \in A (\|x - T - b\| < z \to \|({F ↾}_{A}) (x - T) - ({F ↾}_{A}) (b)\| < w) \to \exists z \in ℝ^{+} \forall v \in B (\|x - v\| < z \to \|({F ↾}_{B}) (x) - ({F ↾}_{B}) (v)\| < w))$
124	43 123	mpd	$⊢ (φ \land (x \in B \land w \in ℝ^{+})) \to \exists z \in ℝ^{+} \forall v \in B (\|x - v\| < z \to \|({F ↾}_{B}) (x) - ({F ↾}_{B}) (v)\| < w)$
125	124	ralrimivva	$⊢ φ \to \forall x \in B \forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall v \in B (\|x - v\| < z \to \|({F ↾}_{B}) (x) - ({F ↾}_{B}) (v)\| < w)$
126	52	a1i	$⊢ φ \to B \subseteq ℂ$
127		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
128		elcncf	$⊢ (B \subseteq ℂ \land ℂ \subseteq ℂ) \to (({F ↾}_{B}) : B \underset{cn}{⟶} ℂ \leftrightarrow (({F ↾}_{B}) : B ⟶ ℂ \land \forall x \in B \forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall v \in B (\|x - v\| < z \to \|({F ↾}_{B}) (x) - ({F ↾}_{B}) (v)\| < w)))$
129	126 127 128	syl2anc	$⊢ φ \to (({F ↾}_{B}) : B \underset{cn}{⟶} ℂ \leftrightarrow (({F ↾}_{B}) : B ⟶ ℂ \land \forall x \in B \forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall v \in B (\|x - v\| < z \to \|({F ↾}_{B}) (x) - ({F ↾}_{B}) (v)\| < w)))$
130	8 125 129	mpbir2and	$⊢ φ \to ({F ↾}_{B}) : B \underset{cn}{⟶} ℂ$

Metamath Proof Explorer

Theorem cncfperiod

Proof