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