Theorem divccn

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

	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	mulcn	⊢ · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
12	11	a1i	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → · ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
13	7 8 10 12	cnmpt12f	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 · ( 1 / 𝐴 ) ) ) ∈ ( 𝐽 Cn 𝐽 ) )
14	5 13	eqeltrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) → ( 𝑥 ∈ ℂ ↦ ( 𝑥 / 𝐴 ) ) ∈ ( 𝐽 Cn 𝐽 ) )