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

Metamath Proof Explorer

Theorem add2cncf

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

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

Proof

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