Theorem cnxmet

Description: The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Assertion	cnxmet	⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )

Proof

Step	Hyp	Ref	Expression
1		cnmet	⊢ ( abs ∘ − ) ∈ ( Met ‘ ℂ )
2		metxmet	⊢ ( ( abs ∘ − ) ∈ ( Met ‘ ℂ ) → ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) )
3	1 2	ax-mp	⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )