# Metamath Proof Explorer

## Theorem divccn

Description: Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014)

Ref Expression
Hypothesis expcn.j ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
Assertion divccn ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left({x}\in ℂ⟼\frac{{x}}{{A}}\right)\in \left({J}\mathrm{Cn}{J}\right)$

### Proof

Step Hyp Ref Expression
1 expcn.j ${⊢}{J}=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
2 divrec ${⊢}\left({x}\in ℂ\wedge {A}\in ℂ\wedge {A}\ne 0\right)\to \frac{{x}}{{A}}={x}\left(\frac{1}{{A}}\right)$
3 2 3expb ${⊢}\left({x}\in ℂ\wedge \left({A}\in ℂ\wedge {A}\ne 0\right)\right)\to \frac{{x}}{{A}}={x}\left(\frac{1}{{A}}\right)$
4 3 ancoms ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge {x}\in ℂ\right)\to \frac{{x}}{{A}}={x}\left(\frac{1}{{A}}\right)$
5 4 mpteq2dva ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left({x}\in ℂ⟼\frac{{x}}{{A}}\right)=\left({x}\in ℂ⟼{x}\left(\frac{1}{{A}}\right)\right)$
6 1 cnfldtopon ${⊢}{J}\in \mathrm{TopOn}\left(ℂ\right)$
7 6 a1i ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to {J}\in \mathrm{TopOn}\left(ℂ\right)$
8 7 cnmptid ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left({x}\in ℂ⟼{x}\right)\in \left({J}\mathrm{Cn}{J}\right)$
9 reccl ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \frac{1}{{A}}\in ℂ$
10 7 7 9 cnmptc ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left({x}\in ℂ⟼\frac{1}{{A}}\right)\in \left({J}\mathrm{Cn}{J}\right)$
11 1 mulcn ${⊢}×\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$
12 11 a1i ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to ×\in \left(\left({J}{×}_{t}{J}\right)\mathrm{Cn}{J}\right)$
13 7 8 10 12 cnmpt12f ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left({x}\in ℂ⟼{x}\left(\frac{1}{{A}}\right)\right)\in \left({J}\mathrm{Cn}{J}\right)$
14 5 13 eqeltrd ${⊢}\left({A}\in ℂ\wedge {A}\ne 0\right)\to \left({x}\in ℂ⟼\frac{{x}}{{A}}\right)\in \left({J}\mathrm{Cn}{J}\right)$