Theorem subcn

Description: Complex number subtraction is a continuous function. Part of Proposition 14-4.16 of Gleason p. 243. (Contributed by NM, 4-Aug-2007) (Proof shortened by Mario Carneiro, 5-May-2014)

	Ref	Expression
Hypothesis	addcn.j	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	subcn	$$⊢-\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}J\right)$$

Proof

Step	Hyp	Ref	Expression
1		addcn.j	$$⊢J=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
2		subf	$$⊢-:ℂ\times ℂ⟶ℂ$$
3		subcn2	$$⊢\left(a\in {ℝ}^{+}\wedge b\in ℂ\wedge c\in ℂ\right)\to \exists y\in {ℝ}^{+}\exists z\in {ℝ}^{+}\forall u\in ℂ\forall v\in ℂ\left(\left(\left|u-b\right|<y\wedge \left|v-c\right|<z\right)\to \left|u-v-\left(b-c\right)\right|<a\right)$$
4	1 2 3	addcnlem	$$⊢-\in \left(\left(J{\times }_{t}J\right)\mathrm{Cn}J\right)$$