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

Metamath Proof Explorer

Theorem addccncf

Description: Adding a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypothesis addccncf.1 ⊢ F = x ∈ ℂ ⟼ x + A
Assertion addccncf ⊢ A ∈ ℂ → F : ℂ ⟶cn ℂ

Proof

Step Hyp Ref Expression
1 addccncf.1 ⊢ F = x ∈ ℂ ⟼ x + A
2 eqid ⊢ TopOpen ⁡ ℂ fld = TopOpen ⁡ ℂ fld
3 2 addcn ⊢ + ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
4 3 a1i ⊢ A ∈ ℂ → + ∈ TopOpen ⁡ ℂ fld × t TopOpen ⁡ ℂ fld Cn TopOpen ⁡ ℂ fld
5 ssid ⊢ ℂ ⊆ ℂ
6 cncfmptid ⊢ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ → x ∈ ℂ ⟼ x : ℂ ⟶cn ℂ
7 5 5 6 mp2an ⊢ x ∈ ℂ ⟼ x : ℂ ⟶cn ℂ
8 7 a1i ⊢ A ∈ ℂ → x ∈ ℂ ⟼ x : ℂ ⟶cn ℂ
9 cncfmptc ⊢ A ∈ ℂ ∧ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ → x ∈ ℂ ⟼ A : ℂ ⟶cn ℂ
10 5 5 9 mp3an23 ⊢ A ∈ ℂ → x ∈ ℂ ⟼ A : ℂ ⟶cn ℂ
11 2 4 8 10 cncfmpt2f ⊢ A ∈ ℂ → x ∈ ℂ ⟼ x + A : ℂ ⟶cn ℂ
12 1 11 eqeltrid ⊢ A ∈ ℂ → F : ℂ ⟶cn ℂ