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

Metamath Proof Explorer

Theorem mulc1cncf

Description: Multiplication by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007) (Revised by Mario Carneiro, 30-Apr-2014)

Ref Expression
Hypothesis mulc1cncf.1 ⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) )
Assertion mulc1cncf ( 𝐴 ∈ ℂ → 𝐹 ∈ ( ℂ –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 mulc1cncf.1 ⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ ( 𝐴 · 𝑥 ) )
2 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝐴 · 𝑥 ) ∈ ℂ )
3 2 1 fmptd ⊢ ( 𝐴 ∈ ℂ → 𝐹 : ℂ ⟶ ℂ )
4 simprr ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) → 𝑧 ∈ ℝ+ )
5 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) → 𝐴 ∈ ℂ )
6 simprl ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) → 𝑦 ∈ ℂ )
7 mulcn2 ⊢ ( ( 𝑧 ∈ ℝ+ ∧ 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ∃ 𝑡 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ℂ ∀ 𝑢 ∈ ℂ ( ( ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑣 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) )
8 4 5 6 7 syl3anc ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) → ∃ 𝑡 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ℂ ∀ 𝑢 ∈ ℂ ( ( ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑣 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) )
9 fvoveq1 ⊢ ( 𝑣 = 𝐴 → ( abs ‘ ( 𝑣 − 𝐴 ) ) = ( abs ‘ ( 𝐴 − 𝐴 ) ) )
10 9 breq1d ⊢ ( 𝑣 = 𝐴 → ( ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑡 ↔ ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑡 ) )
11 10 anbi1d ⊢ ( 𝑣 = 𝐴 → ( ( ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) ↔ ( ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) ) )
12 oveq1 ⊢ ( 𝑣 = 𝐴 → ( 𝑣 · 𝑢 ) = ( 𝐴 · 𝑢 ) )
13 12 fvoveq1d ⊢ ( 𝑣 = 𝐴 → ( abs ‘ ( ( 𝑣 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) = ( abs ‘ ( ( 𝐴 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) )
14 13 breq1d ⊢ ( 𝑣 = 𝐴 → ( ( abs ‘ ( ( 𝑣 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ↔ ( abs ‘ ( ( 𝐴 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) )
15 11 14 imbi12d ⊢ ( 𝑣 = 𝐴 → ( ( ( ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑣 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) ↔ ( ( ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐴 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) ) )
16 15 ralbidv ⊢ ( 𝑣 = 𝐴 → ( ∀ 𝑢 ∈ ℂ ( ( ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑣 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) ↔ ∀ 𝑢 ∈ ℂ ( ( ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐴 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) ) )
17 16 rspcv ⊢ ( 𝐴 ∈ ℂ → ( ∀ 𝑣 ∈ ℂ ∀ 𝑢 ∈ ℂ ( ( ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑣 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) → ∀ 𝑢 ∈ ℂ ( ( ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐴 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) ) )
18 17 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ) → ( ∀ 𝑣 ∈ ℂ ∀ 𝑢 ∈ ℂ ( ( ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑣 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) → ∀ 𝑢 ∈ ℂ ( ( ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐴 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) ) )
19 subid ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 − 𝐴 ) = 0 )
20 19 ad2antrr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑢 ∈ ℂ ) ) → ( 𝐴 − 𝐴 ) = 0 )
21 20 abs00bd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑢 ∈ ℂ ) ) → ( abs ‘ ( 𝐴 − 𝐴 ) ) = 0 )
22 simprll ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑢 ∈ ℂ ) ) → 𝑡 ∈ ℝ+ )
23 22 rpgt0d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑢 ∈ ℂ ) ) → 0 < 𝑡 )
24 21 23 eqbrtrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑢 ∈ ℂ ) ) → ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑡 )
25 24 biantrurd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑢 ∈ ℂ ) ) → ( ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ↔ ( ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) ) )
26 simprr ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑢 ∈ ℂ ) ) → 𝑢 ∈ ℂ )
27 oveq2 ⊢ ( 𝑥 = 𝑢 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝑢 ) )
28 ovex ⊢ ( 𝐴 · 𝑢 ) ∈ V
29 27 1 28 fvmpt ⊢ ( 𝑢 ∈ ℂ → ( 𝐹 ‘ 𝑢 ) = ( 𝐴 · 𝑢 ) )
30 26 29 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑢 ∈ ℂ ) ) → ( 𝐹 ‘ 𝑢 ) = ( 𝐴 · 𝑢 ) )
31 simplrl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑢 ∈ ℂ ) ) → 𝑦 ∈ ℂ )
32 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 · 𝑥 ) = ( 𝐴 · 𝑦 ) )
33 ovex ⊢ ( 𝐴 · 𝑦 ) ∈ V
34 32 1 33 fvmpt ⊢ ( 𝑦 ∈ ℂ → ( 𝐹 ‘ 𝑦 ) = ( 𝐴 · 𝑦 ) )
35 31 34 syl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑢 ∈ ℂ ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐴 · 𝑦 ) )
36 30 35 oveq12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑢 ∈ ℂ ) ) → ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐴 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) )
37 36 fveq2d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑢 ∈ ℂ ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑦 ) ) ) = ( abs ‘ ( ( 𝐴 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) )
38 37 breq1d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑢 ∈ ℂ ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑧 ↔ ( abs ‘ ( ( 𝐴 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) )
39 25 38 imbi12d ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ∧ 𝑢 ∈ ℂ ) ) → ( ( ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑧 ) ↔ ( ( ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐴 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) ) )
40 39 anassrs ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ) ∧ 𝑢 ∈ ℂ ) → ( ( ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑧 ) ↔ ( ( ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐴 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) ) )
41 40 ralbidva ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ) → ( ∀ 𝑢 ∈ ℂ ( ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑧 ) ↔ ∀ 𝑢 ∈ ℂ ( ( ( abs ‘ ( 𝐴 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝐴 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) ) )
42 18 41 sylibrd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ ( 𝑡 ∈ ℝ+ ∧ 𝑤 ∈ ℝ+ ) ) → ( ∀ 𝑣 ∈ ℂ ∀ 𝑢 ∈ ℂ ( ( ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑣 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) → ∀ 𝑢 ∈ ℂ ( ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑧 ) ) )
43 42 anassrs ⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑡 ∈ ℝ+ ) ∧ 𝑤 ∈ ℝ+ ) → ( ∀ 𝑣 ∈ ℂ ∀ 𝑢 ∈ ℂ ( ( ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑣 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) → ∀ 𝑢 ∈ ℂ ( ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑧 ) ) )
44 43 reximdva ⊢ ( ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) ∧ 𝑡 ∈ ℝ+ ) → ( ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ℂ ∀ 𝑢 ∈ ℂ ( ( ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑣 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ( ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑧 ) ) )
45 44 rexlimdva ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) → ( ∃ 𝑡 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑣 ∈ ℂ ∀ 𝑢 ∈ ℂ ( ( ( abs ‘ ( 𝑣 − 𝐴 ) ) < 𝑡 ∧ ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 ) → ( abs ‘ ( ( 𝑣 · 𝑢 ) − ( 𝐴 · 𝑦 ) ) ) < 𝑧 ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ( ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑧 ) ) )
46 8 45 mpd ⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℝ+ ) ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ( ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑧 ) )
47 46 ralrimivva ⊢ ( 𝐴 ∈ ℂ → ∀ 𝑦 ∈ ℂ ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ( ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑧 ) )
48 ssid ⊢ ℂ ⊆ ℂ
49 elcncf2 ⊢ ( ( ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐹 ∈ ( ℂ –cn→ ℂ ) ↔ ( 𝐹 : ℂ ⟶ ℂ ∧ ∀ 𝑦 ∈ ℂ ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ( ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑧 ) ) ) )
50 48 48 49 mp2an ⊢ ( 𝐹 ∈ ( ℂ –cn→ ℂ ) ↔ ( 𝐹 : ℂ ⟶ ℂ ∧ ∀ 𝑦 ∈ ℂ ∀ 𝑧 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑢 ∈ ℂ ( ( abs ‘ ( 𝑢 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 𝑢 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑧 ) ) )
51 3 47 50 sylanbrc ⊢ ( 𝐴 ∈ ℂ → 𝐹 ∈ ( ℂ –cn→ ℂ ) )