This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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→ ℂ ) )