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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
add2cncf.f ⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ ( 𝐴 + 𝑥 ) )
Assertion add2cncf ( 𝜑 → 𝐹 ∈ ( ℂ –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 add2cncf.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2 add2cncf.f ⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ ( 𝐴 + 𝑥 ) )
3 ssid ⊢ ℂ ⊆ ℂ
4 3 a1i ⊢ ( 𝐴 ∈ ℂ → ℂ ⊆ ℂ )
5 cncfmptc ⊢ ( ( 𝐴 ∈ ℂ ∧ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ℂ ↦ 𝐴 ) ∈ ( ℂ –cn→ ℂ ) )
6 4 4 5 mpd3an23 ⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℂ ↦ 𝐴 ) ∈ ( ℂ –cn→ ℂ ) )
7 1 6 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ 𝐴 ) ∈ ( ℂ –cn→ ℂ ) )
8 cncfmptid ⊢ ( ( ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ℂ –cn→ ℂ ) )
9 3 3 8 mp2an ⊢ ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ℂ –cn→ ℂ )
10 9 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( ℂ –cn→ ℂ ) )
11 7 10 addcncf ⊢ ( 𝜑 → ( 𝑥 ∈ ℂ ↦ ( 𝐴 + 𝑥 ) ) ∈ ( ℂ –cn→ ℂ ) )
12 2 11 eqeltrid ⊢ ( 𝜑 → 𝐹 ∈ ( ℂ –cn→ ℂ ) )