Theorem divccncf

Description: Division by a constant is continuous. (Contributed by Paul Chapman, 28-Nov-2007)

	Ref	Expression
Hypothesis	divccncf.1	$$⊢F=\left(x\in ℂ⟼\frac{x}{A}\right)$$
Assertion	divccncf	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to F:ℂ\underset{cn}{⟶}ℂ$$

Proof

Step	Hyp	Ref	Expression
1		divccncf.1	$$⊢F=\left(x\in ℂ⟼\frac{x}{A}\right)$$
2		divrec2	$$⊢\left(x\in ℂ\wedge A\in ℂ\wedge A\ne 0\right)\to \frac{x}{A}=\left(\frac{1}{A}\right)x$$
3	2	3expb	$$⊢\left(x\in ℂ\wedge \left(A\in ℂ\wedge A\ne 0\right)\right)\to \frac{x}{A}=\left(\frac{1}{A}\right)x$$
4	3	ancoms	$$⊢\left(\left(A\in ℂ\wedge A\ne 0\right)\wedge x\in ℂ\right)\to \frac{x}{A}=\left(\frac{1}{A}\right)x$$
5	4	mpteq2dva	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(x\in ℂ⟼\frac{x}{A}\right)=\left(x\in ℂ⟼\left(\frac{1}{A}\right)x\right)$$
6	1 5	eqtrid	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to F=\left(x\in ℂ⟼\left(\frac{1}{A}\right)x\right)$$
7		reccl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{1}{A}\in ℂ$$
8		eqid	$$⊢\left(x\in ℂ⟼\left(\frac{1}{A}\right)x\right)=\left(x\in ℂ⟼\left(\frac{1}{A}\right)x\right)$$
9	8	mulc1cncf	$$⊢\frac{1}{A}\in ℂ\to \left(x\in ℂ⟼\left(\frac{1}{A}\right)x\right):ℂ\underset{cn}{⟶}ℂ$$
10	7 9	syl	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \left(x\in ℂ⟼\left(\frac{1}{A}\right)x\right):ℂ\underset{cn}{⟶}ℂ$$
11	6 10	eqeltrd	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to F:ℂ\underset{cn}{⟶}ℂ$$