Step |
Hyp |
Ref |
Expression |
1 |
|
psmetcl |
|- ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> ( A D B ) e. RR* ) |
2 |
1
|
3expb |
|- ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) ) -> ( A D B ) e. RR* ) |
3 |
2
|
3adant3 |
|- ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) /\ ( C e. RR /\ ( A D B ) <_ C ) ) -> ( A D B ) e. RR* ) |
4 |
|
simp3l |
|- ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) /\ ( C e. RR /\ ( A D B ) <_ C ) ) -> C e. RR ) |
5 |
|
psmetge0 |
|- ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> 0 <_ ( A D B ) ) |
6 |
5
|
3expb |
|- ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) ) -> 0 <_ ( A D B ) ) |
7 |
6
|
3adant3 |
|- ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) /\ ( C e. RR /\ ( A D B ) <_ C ) ) -> 0 <_ ( A D B ) ) |
8 |
|
simp3r |
|- ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) /\ ( C e. RR /\ ( A D B ) <_ C ) ) -> ( A D B ) <_ C ) |
9 |
|
xrrege0 |
|- ( ( ( ( A D B ) e. RR* /\ C e. RR ) /\ ( 0 <_ ( A D B ) /\ ( A D B ) <_ C ) ) -> ( A D B ) e. RR ) |
10 |
3 4 7 8 9
|
syl22anc |
|- ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ B e. X ) /\ ( C e. RR /\ ( A D B ) <_ C ) ) -> ( A D B ) e. RR ) |