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→ ℂ ) )