Theorem xmetge0

Description: The distance function of a metric space is nonnegative. (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Assertion	xmetge0	|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> D e. ( *Met ` X ) )
2		simp2	|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> A e. X )
3		simp3	|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> B e. X )
4		xmettri2	|- ( ( D e. ( *Met ` X ) /\ ( A e. X /\ B e. X /\ B e. X ) ) -> ( B D B ) <_ ( ( A D B ) +e ( A D B ) ) )
5	1 2 3 3 4	syl13anc	|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( B D B ) <_ ( ( A D B ) +e ( A D B ) ) )
6		2re	|- 2 e. RR
7		rexr	|- ( 2 e. RR -> 2 e. RR* )
8		xmul01	|- ( 2 e. RR* -> ( 2 *e 0 ) = 0 )
9	6 7 8	mp2b	|- ( 2 *e 0 ) = 0
10		xmet0	|- ( ( D e. ( *Met ` X ) /\ B e. X ) -> ( B D B ) = 0 )
11	10	3adant2	|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( B D B ) = 0 )
12	9 11	eqtr4id	|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( 2 *e 0 ) = ( B D B ) )
13		xmetcl	|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* )
14		x2times	|- ( ( A D B ) e. RR* -> ( 2 *e ( A D B ) ) = ( ( A D B ) +e ( A D B ) ) )
15	13 14	syl	|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( 2 *e ( A D B ) ) = ( ( A D B ) +e ( A D B ) ) )
16	5 12 15	3brtr4d	|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( 2 *e 0 ) <_ ( 2 *e ( A D B ) ) )
17		0xr	|- 0 e. RR*
18		2rp	|- 2 e. RR+
19	18	a1i	|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> 2 e. RR+ )
20		xlemul2	|- ( ( 0 e. RR* /\ ( A D B ) e. RR* /\ 2 e. RR+ ) -> ( 0 <_ ( A D B ) <-> ( 2 *e 0 ) <_ ( 2 *e ( A D B ) ) ) )
21	17 13 19 20	mp3an2i	|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( 0 <_ ( A D B ) <-> ( 2 *e 0 ) <_ ( 2 *e ( A D B ) ) ) )
22	16 21	mpbird	|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) )