# Metamath Proof Explorer

## Theorem sub1cncf

Description: Subtracting a constant is a continuous function. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 12-Sep-2015)

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

### Proof

Step Hyp Ref Expression
1 sub1cncf.1 ${⊢}{F}=\left({x}\in ℂ⟼{x}-{A}\right)$
2 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
3 2 subcn ${⊢}-\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
4 3 a1i ${⊢}{A}\in ℂ\to -\in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){×}_{t}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$
5 eqid ${⊢}\left({x}\in ℂ⟼{x}\right)=\left({x}\in ℂ⟼{x}\right)$
6 5 idcncf ${⊢}\left({x}\in ℂ⟼{x}\right):ℂ\underset{cn}{⟶}ℂ$
7 6 a1i ${⊢}{A}\in ℂ\to \left({x}\in ℂ⟼{x}\right):ℂ\underset{cn}{⟶}ℂ$
8 ssid ${⊢}ℂ\subseteq ℂ$
9 cncfmptc ${⊢}\left({A}\in ℂ\wedge ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left({x}\in ℂ⟼{A}\right):ℂ\underset{cn}{⟶}ℂ$
10 8 8 9 mp3an23 ${⊢}{A}\in ℂ\to \left({x}\in ℂ⟼{A}\right):ℂ\underset{cn}{⟶}ℂ$
11 2 4 7 10 cncfmpt2f ${⊢}{A}\in ℂ\to \left({x}\in ℂ⟼{x}-{A}\right):ℂ\underset{cn}{⟶}ℂ$
12 1 11 eqeltrid ${⊢}{A}\in ℂ\to {F}:ℂ\underset{cn}{⟶}ℂ$