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

Metamath Proof Explorer

Theorem add1cncf

Description: Addition to a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses add1cncf.a ⊢ φ → A ∈ ℂ
add1cncf.f ⊢ F = x ∈ ℂ ⟼ x + A
Assertion add1cncf ⊢ φ → F : ℂ ⟶cn ℂ

Proof

Step Hyp Ref Expression
1 add1cncf.a ⊢ φ → A ∈ ℂ
2 add1cncf.f ⊢ F = x ∈ ℂ ⟼ x + A
3 ssid ⊢ ℂ ⊆ ℂ
4 cncfmptid ⊢ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ → x ∈ ℂ ⟼ x : ℂ ⟶cn ℂ
5 3 3 4 mp2an ⊢ x ∈ ℂ ⟼ x : ℂ ⟶cn ℂ
6 5 a1i ⊢ φ → x ∈ ℂ ⟼ x : ℂ ⟶cn ℂ
7 id ⊢ A ∈ ℂ → A ∈ ℂ
8 3 a1i ⊢ A ∈ ℂ → ℂ ⊆ ℂ
9 cncfmptc ⊢ A ∈ ℂ ∧ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ → x ∈ ℂ ⟼ A : ℂ ⟶cn ℂ
10 7 8 8 9 syl3anc ⊢ A ∈ ℂ → x ∈ ℂ ⟼ A : ℂ ⟶cn ℂ
11 1 10 syl ⊢ φ → x ∈ ℂ ⟼ A : ℂ ⟶cn ℂ
12 6 11 addcncf ⊢ φ → x ∈ ℂ ⟼ x + A : ℂ ⟶cn ℂ
13 2 12 eqeltrid ⊢ φ → F : ℂ ⟶cn ℂ