Metamath Proof Explorer

Theorem cncfshift

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

Ref Expression
Hypotheses cncfshift.a ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
cncfshift.t ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
cncfshift.b ⊢ 𝐵 = { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ 𝐴 𝑥 = ( 𝑦 + 𝑇 ) }
cncfshift.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 –cn→ ℂ ) )
cncfshift.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐹 ‘ ( 𝑥 − 𝑇 ) ) )
Assertion cncfshift ( 𝜑 → 𝐺 ∈ ( 𝐵 –cn→ ℂ ) )

Proof

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