limcperiod

Description: If F is a periodic function with period T , the limit doesn't change if we shift the limiting point by T . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	limcperiod.f	$⊢ φ \to F : dom F ⟶ ℂ$
	limcperiod.assc	$⊢ φ \to A \subseteq ℂ$
	limcperiod.3	$⊢ φ \to A \subseteq dom F$
	limcperiod.t	$⊢ φ \to T \in ℂ$
	limcperiod.b	$⊢ B = \{x \in ℂ \| \exists y \in A x = y + T\}$
	limcperiod.bss	$⊢ φ \to B \subseteq dom F$
	limcperiod.fper	$⊢ (φ \land y \in A) \to F (y + T) = F (y)$
	limcperiod.clim	$⊢ φ \to C \in (({F ↾}_{A}) {lim}_{ℂ} D)$
Assertion	limcperiod	$⊢ φ \to C \in (({F ↾}_{B}) {lim}_{ℂ} (D + T))$

Proof

Step	Hyp	Ref	Expression
1		limcperiod.f	$⊢ φ \to F : dom F ⟶ ℂ$
2		limcperiod.assc	$⊢ φ \to A \subseteq ℂ$
3		limcperiod.3	$⊢ φ \to A \subseteq dom F$
4		limcperiod.t	$⊢ φ \to T \in ℂ$
5		limcperiod.b	$⊢ B = \{x \in ℂ \| \exists y \in A x = y + T\}$
6		limcperiod.bss	$⊢ φ \to B \subseteq dom F$
7		limcperiod.fper	$⊢ (φ \land y \in A) \to F (y + T) = F (y)$
8		limcperiod.clim	$⊢ φ \to C \in (({F ↾}_{A}) {lim}_{ℂ} D)$
9		limccl	$⊢ ({F ↾}_{A}) {lim}_{ℂ} D \subseteq ℂ$
10	9 8	sselid	$⊢ φ \to C \in ℂ$
11	1 3	fssresd	$⊢ φ \to ({F ↾}_{A}) : A ⟶ ℂ$
12		limcrcl	$⊢ C \in (({F ↾}_{A}) {lim}_{ℂ} D) \to (({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ ℂ \land dom ({F ↾}_{A}) \subseteq ℂ \land D \in ℂ)$
13	8 12	syl	$⊢ φ \to (({F ↾}_{A}) : dom ({F ↾}_{A}) ⟶ ℂ \land dom ({F ↾}_{A}) \subseteq ℂ \land D \in ℂ)$
14	13	simp3d	$⊢ φ \to D \in ℂ$
15	11 2 14	ellimc3	$⊢ φ \to (C \in (({F ↾}_{A}) {lim}_{ℂ} D) \leftrightarrow (C \in ℂ \land \forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)))$
16	8 15	mpbid	$⊢ φ \to (C \in ℂ \land \forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w))$
17	16	simprd	$⊢ φ \to \forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)$
18	17	r19.21bi	$⊢ (φ \land w \in ℝ^{+}) \to \exists z \in ℝ^{+} \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)$
19		simpl1l	$⊢ (((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \to φ$
20	19	adantr	$⊢ ((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \to φ$
21		simplr	$⊢ ((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \to b \in B$
22		id	$⊢ b \in B \to b \in B$
23		oveq1	$⊢ y = z \to y + T = z + T$
24	23	eqeq2d	$⊢ y = z \to (x = y + T \leftrightarrow x = z + T)$
25	24	cbvrexvw	$⊢ \exists y \in A x = y + T \leftrightarrow \exists z \in A x = z + T$
26		eqeq1	$⊢ x = w \to (x = z + T \leftrightarrow w = z + T)$
27	26	rexbidv	$⊢ x = w \to (\exists z \in A x = z + T \leftrightarrow \exists z \in A w = z + T)$
28	25 27	syl5bb	$⊢ x = w \to (\exists y \in A x = y + T \leftrightarrow \exists z \in A w = z + T)$
29	28	cbvrabv	$⊢ \{x \in ℂ \| \exists y \in A x = y + T\} = \{w \in ℂ \| \exists z \in A w = z + T\}$
30	5 29	eqtri	$⊢ B = \{w \in ℂ \| \exists z \in A w = z + T\}$
31	22 30	eleqtrdi	$⊢ b \in B \to b \in \{w \in ℂ \| \exists z \in A w = z + T\}$
32		eqeq1	$⊢ w = b \to (w = z + T \leftrightarrow b = z + T)$
33	32	rexbidv	$⊢ w = b \to (\exists z \in A w = z + T \leftrightarrow \exists z \in A b = z + T)$
34	33	elrab	$⊢ b \in \{w \in ℂ \| \exists z \in A w = z + T\} \leftrightarrow (b \in ℂ \land \exists z \in A b = z + T)$
35	31 34	sylib	$⊢ b \in B \to (b \in ℂ \land \exists z \in A b = z + T)$
36	35	simprd	$⊢ b \in B \to \exists z \in A b = z + T$
37	36	adantl	$⊢ (φ \land b \in B) \to \exists z \in A b = z + T$
38		oveq1	$⊢ b = z + T \to b - T = z + T - T$
39	38	3ad2ant3	$⊢ (φ \land z \in A \land b = z + T) \to b - T = z + T - T$
40	2	sselda	$⊢ (φ \land z \in A) \to z \in ℂ$
41	4	adantr	$⊢ (φ \land z \in A) \to T \in ℂ$
42	40 41	pncand	$⊢ (φ \land z \in A) \to z + T - T = z$
43	42	3adant3	$⊢ (φ \land z \in A \land b = z + T) \to z + T - T = z$
44	39 43	eqtrd	$⊢ (φ \land z \in A \land b = z + T) \to b - T = z$
45		simp2	$⊢ (φ \land z \in A \land b = z + T) \to z \in A$
46	44 45	eqeltrd	$⊢ (φ \land z \in A \land b = z + T) \to b - T \in A$
47	46	3exp	$⊢ φ \to (z \in A \to (b = z + T \to b - T \in A))$
48	47	adantr	$⊢ (φ \land b \in B) \to (z \in A \to (b = z + T \to b - T \in A))$
49	48	rexlimdv	$⊢ (φ \land b \in B) \to (\exists z \in A b = z + T \to b - T \in A)$
50	37 49	mpd	$⊢ (φ \land b \in B) \to b - T \in A$
51	5	ssrab3	$⊢ B \subseteq ℂ$
52	51	a1i	$⊢ φ \to B \subseteq ℂ$
53	52	sselda	$⊢ (φ \land b \in B) \to b \in ℂ$
54	4	adantr	$⊢ (φ \land b \in B) \to T \in ℂ$
55	53 54	npcand	$⊢ (φ \land b \in B) \to b - T + T = b$
56	55	eqcomd	$⊢ (φ \land b \in B) \to b = b - T + T$
57		oveq1	$⊢ x = b - T \to x + T = b - T + T$
58	57	rspceeqv	$⊢ (b - T \in A \land b = b - T + T) \to \exists x \in A b = x + T$
59	50 56 58	syl2anc	$⊢ (φ \land b \in B) \to \exists x \in A b = x + T$
60	20 21 59	syl2anc	$⊢ ((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \to \exists x \in A b = x + T$
61		nfv	$⊢ Ⅎ x ((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w))$
62		nfrab1	$⊢ \underline{Ⅎ} x \{x \in ℂ \| \exists y \in A x = y + T\}$
63	5 62	nfcxfr	$⊢ \underline{Ⅎ} x B$
64	63	nfcri	$⊢ Ⅎ x b \in B$
65	61 64	nfan	$⊢ Ⅎ x (((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B)$
66		nfv	$⊢ Ⅎ x (b \neq D + T \land \|b - (D + T)\| < z)$
67	65 66	nfan	$⊢ Ⅎ x ((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z))$
68		nfcv	$⊢ \underline{Ⅎ} x abs$
69		nfcv	$⊢ \underline{Ⅎ} x F$
70	69 63	nfres	$⊢ \underline{Ⅎ} x ({F ↾}_{B})$
71		nfcv	$⊢ \underline{Ⅎ} x b$
72	70 71	nffv	$⊢ \underline{Ⅎ} x ({F ↾}_{B}) (b)$
73		nfcv	$⊢ \underline{Ⅎ} x -$
74		nfcv	$⊢ \underline{Ⅎ} x C$
75	72 73 74	nfov	$⊢ \underline{Ⅎ} x (({F ↾}_{B}) (b) - C)$
76	68 75	nffv	$⊢ \underline{Ⅎ} x \|({F ↾}_{B}) (b) - C\|$
77		nfcv	$⊢ \underline{Ⅎ} x <$
78		nfcv	$⊢ \underline{Ⅎ} x w$
79	76 77 78	nfbr	$⊢ Ⅎ x \|({F ↾}_{B}) (b) - C\| < w$
80		simp3	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to b = x + T$
81	80	fveq2d	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to ({F ↾}_{B}) (b) = ({F ↾}_{B}) (x + T)$
82	21	3ad2ant1	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to b \in B$
83	80 82	eqeltrrd	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to x + T \in B$
84	83	fvresd	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to ({F ↾}_{B}) (x + T) = F (x + T)$
85	20	3ad2ant1	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to φ$
86		simp2	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to x \in A$
87		eleq1w	$⊢ y = x \to (y \in A \leftrightarrow x \in A)$
88	87	anbi2d	$⊢ y = x \to ((φ \land y \in A) \leftrightarrow (φ \land x \in A))$
89		fvoveq1	$⊢ y = x \to F (y + T) = F (x + T)$
90		fveq2	$⊢ y = x \to F (y) = F (x)$
91	89 90	eqeq12d	$⊢ y = x \to (F (y + T) = F (y) \leftrightarrow F (x + T) = F (x))$
92	88 91	imbi12d	$⊢ y = x \to (((φ \land y \in A) \to F (y + T) = F (y)) \leftrightarrow ((φ \land x \in A) \to F (x + T) = F (x)))$
93	92 7	chvarvv	$⊢ (φ \land x \in A) \to F (x + T) = F (x)$
94	85 86 93	syl2anc	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to F (x + T) = F (x)$
95	86	fvresd	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to ({F ↾}_{A}) (x) = F (x)$
96	94 95	eqtr4d	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to F (x + T) = ({F ↾}_{A}) (x)$
97	81 84 96	3eqtrd	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to ({F ↾}_{B}) (b) = ({F ↾}_{A}) (x)$
98	97	fvoveq1d	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to \|({F ↾}_{B}) (b) - C\| = \|({F ↾}_{A}) (x) - C\|$
99		simpll3	$⊢ ((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \to \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)$
100	99	3ad2ant1	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)$
101	100 86	jca	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to (\forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w) \land x \in A)$
102		simp1rl	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to b \neq D + T$
103	102	neneqd	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to \neg b = D + T$
104		oveq1	$⊢ x = D \to x + T = D + T$
105	80 104	sylan9eq	$⊢ ((((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \land x = D) \to b = D + T$
106	103 105	mtand	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to \neg x = D$
107	106	neqned	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to x \neq D$
108	80	oveq1d	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to b - (D + T) = x + T - (D + T)$
109	2	sselda	$⊢ (φ \land x \in A) \to x \in ℂ$
110	85 86 109	syl2anc	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to x \in ℂ$
111	85 14	syl	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to D \in ℂ$
112	85 4	syl	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to T \in ℂ$
113	110 111 112	pnpcan2d	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to x + T - (D + T) = x - D$
114	108 113	eqtr2d	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to x - D = b - (D + T)$
115	114	fveq2d	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to \|x - D\| = \|b - (D + T)\|$
116		simp1rr	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to \|b - (D + T)\| < z$
117	115 116	eqbrtrd	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to \|x - D\| < z$
118	107 117	jca	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to (x \neq D \land \|x - D\| < z)$
119		neeq1	$⊢ y = x \to (y \neq D \leftrightarrow x \neq D)$
120		fvoveq1	$⊢ y = x \to \|y - D\| = \|x - D\|$
121	120	breq1d	$⊢ y = x \to (\|y - D\| < z \leftrightarrow \|x - D\| < z)$
122	119 121	anbi12d	$⊢ y = x \to ((y \neq D \land \|y - D\| < z) \leftrightarrow (x \neq D \land \|x - D\| < z))$
123	122	imbrov2fvoveq	$⊢ y = x \to (((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w) \leftrightarrow ((x \neq D \land \|x - D\| < z) \to \|({F ↾}_{A}) (x) - C\| < w))$
124	123	rspccva	$⊢ (\forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w) \land x \in A) \to ((x \neq D \land \|x - D\| < z) \to \|({F ↾}_{A}) (x) - C\| < w)$
125	101 118 124	sylc	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to \|({F ↾}_{A}) (x) - C\| < w$
126	98 125	eqbrtrd	$⊢ (((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \land x \in A \land b = x + T) \to \|({F ↾}_{B}) (b) - C\| < w$
127	126	3exp	$⊢ ((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \to (x \in A \to (b = x + T \to \|({F ↾}_{B}) (b) - C\| < w))$
128	67 79 127	rexlimd	$⊢ ((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \to (\exists x \in A b = x + T \to \|({F ↾}_{B}) (b) - C\| < w)$
129	60 128	mpd	$⊢ ((((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \land (b \neq D + T \land \|b - (D + T)\| < z)) \to \|({F ↾}_{B}) (b) - C\| < w$
130	129	ex	$⊢ (((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \land b \in B) \to ((b \neq D + T \land \|b - (D + T)\| < z) \to \|({F ↾}_{B}) (b) - C\| < w)$
131	130	ralrimiva	$⊢ ((φ \land w \in ℝ^{+}) \land z \in ℝ^{+} \land \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w)) \to \forall b \in B ((b \neq D + T \land \|b - (D + T)\| < z) \to \|({F ↾}_{B}) (b) - C\| < w)$
132	131	3exp	$⊢ (φ \land w \in ℝ^{+}) \to (z \in ℝ^{+} \to (\forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w) \to \forall b \in B ((b \neq D + T \land \|b - (D + T)\| < z) \to \|({F ↾}_{B}) (b) - C\| < w)))$
133	132	reximdvai	$⊢ (φ \land w \in ℝ^{+}) \to (\exists z \in ℝ^{+} \forall y \in A ((y \neq D \land \|y - D\| < z) \to \|({F ↾}_{A}) (y) - C\| < w) \to \exists z \in ℝ^{+} \forall b \in B ((b \neq D + T \land \|b - (D + T)\| < z) \to \|({F ↾}_{B}) (b) - C\| < w))$
134	18 133	mpd	$⊢ (φ \land w \in ℝ^{+}) \to \exists z \in ℝ^{+} \forall b \in B ((b \neq D + T \land \|b - (D + T)\| < z) \to \|({F ↾}_{B}) (b) - C\| < w)$
135	134	ralrimiva	$⊢ φ \to \forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall b \in B ((b \neq D + T \land \|b - (D + T)\| < z) \to \|({F ↾}_{B}) (b) - C\| < w)$
136	1 6	fssresd	$⊢ φ \to ({F ↾}_{B}) : B ⟶ ℂ$
137	14 4	addcld	$⊢ φ \to D + T \in ℂ$
138	136 52 137	ellimc3	$⊢ φ \to (C \in (({F ↾}_{B}) {lim}_{ℂ} (D + T)) \leftrightarrow (C \in ℂ \land \forall w \in ℝ^{+} \exists z \in ℝ^{+} \forall b \in B ((b \neq D + T \land \|b - (D + T)\| < z) \to \|({F ↾}_{B}) (b) - C\| < w)))$
139	10 135 138	mpbir2and	$⊢ φ \to C \in (({F ↾}_{B}) {lim}_{ℂ} (D + T))$

Metamath Proof Explorer

Theorem limcperiod

Proof