Theorem 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	⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℂ )
	limcperiod.assc	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
	limcperiod.3	⊢ ( 𝜑 → 𝐴 ⊆ dom 𝐹 )
	limcperiod.t	⊢ ( 𝜑 → 𝑇 ∈ ℂ )
	limcperiod.b	⊢ 𝐵 = { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 + 𝑇 ) }
	limcperiod.bss	⊢ ( 𝜑 → 𝐵 ⊆ dom 𝐹 )
	limcperiod.fper	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) )
	limcperiod.clim	⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐹 ↾ 𝐴 ) limℂ 𝐷 ) )
Assertion	limcperiod	⊢ ( 𝜑 → 𝐶 ∈ ( ( 𝐹 ↾ 𝐵 ) limℂ ( 𝐷 + 𝑇 ) ) )

Proof

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