Metamath Proof Explorer

Theorem xrsdsreclb

Description: The metric of the extended real number structure is only real when both arguments are real. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis xrsds.d 
|- D = ( dist ` RR*s )
Assertion xrsdsreclb 
|- ( ( A e. RR* /\ B e. RR* /\ A =/= B ) -> ( ( A D B ) e. RR <-> ( A e. RR /\ B e. RR ) ) )

Proof

Step Hyp Ref Expression
1 xrsds.d 
 |-  D = ( dist ` RR*s )
2 1 xrsdsval 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A D B ) = if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) )
3 2 3adant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ A =/= B ) -> ( A D B ) = if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) )
4 3 eleq1d 
 |-  ( ( A e. RR* /\ B e. RR* /\ A =/= B ) -> ( ( A D B ) e. RR <-> if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) e. RR ) )
5 eleq1 
 |-  ( ( B +e -e A ) = if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) -> ( ( B +e -e A ) e. RR <-> if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) e. RR ) )
6 5 imbi1d 
 |-  ( ( B +e -e A ) = if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) -> ( ( ( B +e -e A ) e. RR -> ( A e. RR /\ B e. RR ) ) <-> ( if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) e. RR -> ( A e. RR /\ B e. RR ) ) ) )
7 eleq1 
 |-  ( ( A +e -e B ) = if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) -> ( ( A +e -e B ) e. RR <-> if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) e. RR ) )
8 7 imbi1d 
 |-  ( ( A +e -e B ) = if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) -> ( ( ( A +e -e B ) e. RR -> ( A e. RR /\ B e. RR ) ) <-> ( if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) e. RR -> ( A e. RR /\ B e. RR ) ) ) )
9 1 xrsdsreclblem 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A =/= B ) /\ A <_ B ) -> ( ( B +e -e A ) e. RR -> ( A e. RR /\ B e. RR ) ) )
10 xrletri 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A <_ B \/ B <_ A ) )
11 10 3adant3 
 |-  ( ( A e. RR* /\ B e. RR* /\ A =/= B ) -> ( A <_ B \/ B <_ A ) )
12 11 orcanai 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A =/= B ) /\ -. A <_ B ) -> B <_ A )
13 necom 
 |-  ( A =/= B <-> B =/= A )
14 13 3anbi3i 
 |-  ( ( A e. RR* /\ B e. RR* /\ A =/= B ) <-> ( A e. RR* /\ B e. RR* /\ B =/= A ) )
15 3ancoma 
 |-  ( ( A e. RR* /\ B e. RR* /\ B =/= A ) <-> ( B e. RR* /\ A e. RR* /\ B =/= A ) )
16 14 15 bitri 
 |-  ( ( A e. RR* /\ B e. RR* /\ A =/= B ) <-> ( B e. RR* /\ A e. RR* /\ B =/= A ) )
17 1 xrsdsreclblem 
 |-  ( ( ( B e. RR* /\ A e. RR* /\ B =/= A ) /\ B <_ A ) -> ( ( A +e -e B ) e. RR -> ( B e. RR /\ A e. RR ) ) )
18 16 17 sylanb 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A =/= B ) /\ B <_ A ) -> ( ( A +e -e B ) e. RR -> ( B e. RR /\ A e. RR ) ) )
19 ancom 
 |-  ( ( B e. RR /\ A e. RR ) <-> ( A e. RR /\ B e. RR ) )
20 18 19 syl6ib 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A =/= B ) /\ B <_ A ) -> ( ( A +e -e B ) e. RR -> ( A e. RR /\ B e. RR ) ) )
21 12 20 syldan 
 |-  ( ( ( A e. RR* /\ B e. RR* /\ A =/= B ) /\ -. A <_ B ) -> ( ( A +e -e B ) e. RR -> ( A e. RR /\ B e. RR ) ) )
22 6 8 9 21 ifbothda 
 |-  ( ( A e. RR* /\ B e. RR* /\ A =/= B ) -> ( if ( A <_ B , ( B +e -e A ) , ( A +e -e B ) ) e. RR -> ( A e. RR /\ B e. RR ) ) )
23 4 22 sylbid 
 |-  ( ( A e. RR* /\ B e. RR* /\ A =/= B ) -> ( ( A D B ) e. RR -> ( A e. RR /\ B e. RR ) ) )
24 1 xrsdsreval 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A D B ) = ( abs ` ( A - B ) ) )
25 recn 
 |-  ( A e. RR -> A e. CC )
26 recn 
 |-  ( B e. RR -> B e. CC )
27 subcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )
28 25 26 27 syl2an 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A - B ) e. CC )
29 28 abscld 
 |-  ( ( A e. RR /\ B e. RR ) -> ( abs ` ( A - B ) ) e. RR )
30 24 29 eqeltrd 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A D B ) e. RR )
31 23 30 impbid1 
 |-  ( ( A e. RR* /\ B e. RR* /\ A =/= B ) -> ( ( A D B ) e. RR <-> ( A e. RR /\ B e. RR ) ) )