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	$$⊢F=\left(x\in ℂ⟼A\right)$$
Assertion	constcncf	$$⊢A\in ℂ\to F:ℂ\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		constcncf.1	$$⊢F=\left(x\in ℂ⟼A\right)$$
2		ssid	$$⊢ℂ\subseteq ℂ$$
3		cncfmptc	$$⊢\left(A\in ℂ\wedge ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left(x\in ℂ⟼A\right):ℂ\underset{cn}{⟶}ℂ$$
4	2 2 3	mp3an23	$$⊢A\in ℂ\to \left(x\in ℂ⟼A\right):ℂ\underset{cn}{⟶}ℂ$$
5	1 4	eqeltrid	$$⊢A\in ℂ\to F:ℂ\underset{cn}{⟶}ℂ$$