This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 bitrid ⊢ ( 𝑥 = 𝑤 → ( ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 + 𝑇 ) ↔ ∃ 𝑧 ∈ 𝐴 𝑤 = ( 𝑧 + 𝑇 ) ) )
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ℂ ( 𝐷 + 𝑇 ) ) )