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

Proof

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