Metamath Proof Explorer


Theorem ltresr2

Description: Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion ltresr2
|- ( ( A e. RR /\ B e. RR ) -> ( A  ( 1st ` A ) 

Proof

Step Hyp Ref Expression
1 elreal2
 |-  ( A e. RR <-> ( ( 1st ` A ) e. R. /\ A = <. ( 1st ` A ) , 0R >. ) )
2 1 simprbi
 |-  ( A e. RR -> A = <. ( 1st ` A ) , 0R >. )
3 elreal2
 |-  ( B e. RR <-> ( ( 1st ` B ) e. R. /\ B = <. ( 1st ` B ) , 0R >. ) )
4 3 simprbi
 |-  ( B e. RR -> B = <. ( 1st ` B ) , 0R >. )
5 2 4 breqan12d
 |-  ( ( A e. RR /\ B e. RR ) -> ( A  <. ( 1st ` A ) , 0R >. . ) )
6 ltresr
 |-  ( <. ( 1st ` A ) , 0R >. . <-> ( 1st ` A ) 
7 5 6 bitrdi
 |-  ( ( A e. RR /\ B e. RR ) -> ( A  ( 1st ` A )