Theorem sub1cncfd

Description: Subtracting a constant is a continuous function. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	sub1cncfd.1	$$⊢\phi \to A\in ℂ$$
	sub1cncfd.2	$$⊢F=\left(x\in ℂ⟼x-A\right)$$
Assertion	sub1cncfd	$$⊢\phi \to F:ℂ\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		sub1cncfd.1	$$⊢\phi \to A\in ℂ$$
2		sub1cncfd.2	$$⊢F=\left(x\in ℂ⟼x-A\right)$$
3		ssid	$$⊢ℂ\subseteq ℂ$$
4		cncfmptid	$$⊢\left(ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left(x\in ℂ⟼x\right):ℂ\underset{cn}{⟶}ℂ$$
5	3 3 4	mp2an	$$⊢\left(x\in ℂ⟼x\right):ℂ\underset{cn}{⟶}ℂ$$
6	5	a1i	$$⊢\phi \to \left(x\in ℂ⟼x\right):ℂ\underset{cn}{⟶}ℂ$$
7	3	a1i	$$⊢\phi \to ℂ\subseteq ℂ$$
8		cncfmptc	$$⊢\left(A\in ℂ\wedge ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left(x\in ℂ⟼A\right):ℂ\underset{cn}{⟶}ℂ$$
9	1 7 7 8	syl3anc	$$⊢\phi \to \left(x\in ℂ⟼A\right):ℂ\underset{cn}{⟶}ℂ$$
10	6 9	subcncf	$$⊢\phi \to \left(x\in ℂ⟼x-A\right):ℂ\underset{cn}{⟶}ℂ$$
11	2 10	eqeltrid	$$⊢\phi \to F:ℂ\underset{cn}{⟶}ℂ$$