Theorem cdivcncf

Description: Division with a constant numerator is continuous. (Contributed by Mario Carneiro, 28-Dec-2016)

	Ref	Expression
Hypothesis	cdivcncf.1	⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) )
Assertion	cdivcncf	⊢ ( 𝐴 ∈ ℂ → 𝐹 ∈ ( ( ℂ ∖ { 0 } ) –cn→ ℂ ) )

Proof

Step	Hyp	Ref	Expression
1		cdivcncf.1	⊢ 𝐹 = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) )
2		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
3	2	cnfldtopon	⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
4	3	a1i	⊢ ( 𝐴 ∈ ℂ → ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) )
5		difss	⊢ ( ℂ ∖ { 0 } ) ⊆ ℂ
6		resttopon	⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( ℂ ∖ { 0 } ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ∈ ( TopOn ‘ ( ℂ ∖ { 0 } ) ) )
7	4 5 6	sylancl	⊢ ( 𝐴 ∈ ℂ → ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ∈ ( TopOn ‘ ( ℂ ∖ { 0 } ) ) )
8		id	⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
9	7 4 8	cnmptc	⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ 𝐴 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
10	7	cnmptid	⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ 𝑥 ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) Cn ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) )
11		eqid	⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) )
12	2 11	divcn	⊢ / ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) Cn ( TopOpen ‘ ℂfld ) )
13	12	a1i	⊢ ( 𝐴 ∈ ℂ → / ∈ ( ( ( TopOpen ‘ ℂfld ) ×t ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) ) Cn ( TopOpen ‘ ℂfld ) ) )
14	7 9 10 13	cnmpt12f	⊢ ( 𝐴 ∈ ℂ → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝐴 / 𝑥 ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
15		ssid	⊢ ℂ ⊆ ℂ
16	3	toponrestid	⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
17	2 11 16	cncfcn	⊢ ( ( ( ℂ ∖ { 0 } ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( ℂ ∖ { 0 } ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
18	5 15 17	mp2an	⊢ ( ( ℂ ∖ { 0 } ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( ℂ ∖ { 0 } ) ) Cn ( TopOpen ‘ ℂfld ) )
19	14 1 18	3eltr4g	⊢ ( 𝐴 ∈ ℂ → 𝐹 ∈ ( ( ℂ ∖ { 0 } ) –cn→ ℂ ) )