Metamath Proof Explorer

Theorem divccn

Description: Division by a nonzero constant is a continuous operation. (Contributed by Mario Carneiro, 5-May-2014) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		expcn.j	$⊢ J = TopOpen (ℂ_{fld})$
2		divrec	$⊢ (x \in ℂ \land A \in ℂ \land A \neq 0) \to \frac{x}{A} = x (\frac{1}{A})$
3	2	3expb	$⊢ (x \in ℂ \land (A \in ℂ \land A \neq 0)) \to \frac{x}{A} = x (\frac{1}{A})$
4	3	ancoms	$⊢ ((A \in ℂ \land A \neq 0) \land x \in ℂ) \to \frac{x}{A} = x (\frac{1}{A})$
5	4	mpteq2dva	$⊢ (A \in ℂ \land A \neq 0) \to (x \in ℂ ⟼ \frac{x}{A}) = (x \in ℂ ⟼ x (\frac{1}{A}))$
6	1	cnfldtopon	$⊢ J \in TopOn (ℂ)$
7	6	a1i	$⊢ (A \in ℂ \land A \neq 0) \to J \in TopOn (ℂ)$
8	7	cnmptid	$⊢ (A \in ℂ \land A \neq 0) \to (x \in ℂ ⟼ x) \in (J Cn J)$
9		reccl	$⊢ (A \in ℂ \land A \neq 0) \to \frac{1}{A} \in ℂ$
10	7 7 9	cnmptc	$⊢ (A \in ℂ \land A \neq 0) \to (x \in ℂ ⟼ \frac{1}{A}) \in (J Cn J)$
11	1	mpomulcn	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) Cn J)$
12	11	a1i	$⊢ (A \in ℂ \land A \neq 0) \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) Cn J)$
13		oveq12	$⊢ (u = x \land v = \frac{1}{A}) \to u v = x (\frac{1}{A})$
14	7 8 10 7 7 12 13	cnmpt12	$⊢ (A \in ℂ \land A \neq 0) \to (x \in ℂ ⟼ x (\frac{1}{A})) \in (J Cn J)$
15	5 14	eqeltrd	$⊢ (A \in ℂ \land A \neq 0) \to (x \in ℂ ⟼ \frac{x}{A}) \in (J Cn J)$