Metamath Proof Explorer


Theorem metge0

Description: The distance function of a metric space is nonnegative. (Contributed by NM, 27-Aug-2006) (Revised by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion metge0 D Met X A X B X 0 A D B

Proof

Step Hyp Ref Expression
1 metxmet D Met X D ∞Met X
2 xmetge0 D ∞Met X A X B X 0 A D B
3 1 2 syl3an1 D Met X A X B X 0 A D B