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 e. ( Met ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )

Proof

Step Hyp Ref Expression
1 metxmet 
 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
2 xmetge0 
 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )
3 1 2 syl3an1 
 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )