Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
cncfperiod.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
cncfperiod.b ⊢ 𝐵 = { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 + 𝑇 ) }
cncfperiod.f ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℂ )
cncfperiod.cssdmf ⊢ ( 𝜑 → 𝐵 ⊆ dom 𝐹 )
cncfperiod.fper ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
cncfperiod.fcn ⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) ∈ ( 𝐴 –cn→ ℂ ) )
Assertion cncfperiod ( 𝜑 → ( 𝐹 ↾ 𝐵 ) ∈ ( 𝐵 –cn→ ℂ ) )

Proof

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