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→ ℂ ) )