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	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion	divccn	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 𝐴 ) ) ∈ ( 𝐽 Cn 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		expcn.j	⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2		divrec	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 / 𝐴 ) = ( 𝑥 · ( 1 / 𝐴 ) ) )
3	2	3expb	⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ) → ( 𝑥 / 𝐴 ) = ( 𝑥 · ( 1 / 𝐴 ) ) )
4	3	ancoms	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝑥 ∈ ℂ ) → ( 𝑥 / 𝐴 ) = ( 𝑥 · ( 1 / 𝐴 ) ) )
5	4	mpteq2dva	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 𝐴 ) ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( 1 / 𝐴 ) ) ) )
6	1	cnfldtopon	⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
7	6	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → 𝐽 ∈ ( TopOn ‘ ℂ ) )
8	7	cnmptid	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ 𝑥 ) ∈ ( 𝐽 Cn 𝐽 ) )
9		reccl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 1 / 𝐴 ) ∈ ℂ )
10	7 7 9	cnmptc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 1 / 𝐴 ) ) ∈ ( 𝐽 Cn 𝐽 ) )
11	1	mpomulcn	⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
12	11	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
13		oveq12	⊢ ( ( 𝑢 = 𝑥 ∧ 𝑣 = ( 1 / 𝐴 ) ) → ( 𝑢 · 𝑣 ) = ( 𝑥 · ( 1 / 𝐴 ) ) )
14	7 8 10 7 7 12 13	cnmpt12	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( 1 / 𝐴 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
15	5 14	eqeltrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 𝐴 ) ) ∈ ( 𝐽 Cn 𝐽 ) )