Theorem constcncf

Description: A constant function is a continuous function on CC . (Contributed by Jeff Madsen, 2-Sep-2009) (Moved into main set.mm as cncfmptc and may be deleted by mathbox owner, JM. --MC 12-Sep-2015.) (Revised by Mario Carneiro, 12-Sep-2015)

	Ref	Expression
Hypothesis	constcncf.1	⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ 𝐴 )
Assertion	constcncf	⊢ ( 𝐴 ∈ ℂ → 𝐹 ∈ ( ℂ –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		constcncf.1	⊢ 𝐹 = ( 𝑥 ∈ ℂ ↦ 𝐴 )
2		ssid	⊢ ℂ ⊆ ℂ
3		cncfmptc	⊢ ( ( 𝐴 ∈ ℂ ∧ ℂ ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ℂ ↦ 𝐴 ) ∈ ( ℂ –cn→ ℂ ) )
4	2 2 3	mp3an23	⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ℂ ↦ 𝐴 ) ∈ ( ℂ –cn→ ℂ ) )
5	1 4	eqeltrid	⊢ ( 𝐴 ∈ ℂ → 𝐹 ∈ ( ℂ –cn→ ℂ ) )