This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Metric spaces Topology on the reals abscn
Description: The absolute value function on complex numbers is continuous.
(Contributed by NM , 22-Aug-2007) (Proof shortened by Mario Carneiro , 10-Jan-2014)
Ref
Expression
Hypotheses
abscn.3 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
abscn.4 ⊢ 𝐾 = ( topGen ‘ ran (,) )
Assertion
abscn ⊢ abs ∈ ( 𝐽 Cn 𝐾 )
Proof
Step
Hyp
Ref
Expression
1
abscn.3 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
2
abscn.4 ⊢ 𝐾 = ( topGen ‘ ran (,) )
3
cnngp ⊢ ℂfld ∈ NrmGrp
4
cnfldnm ⊢ abs = ( norm ‘ ℂfld )
5
4 1 2
nmcn ⊢ ( ℂfld ∈ NrmGrp → abs ∈ ( 𝐽 Cn 𝐾 ) )
6
3 5
ax-mp ⊢ abs ∈ ( 𝐽 Cn 𝐾 )