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 |
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 |
6 | ltresr | |- ( <. ( 1st ` A ) , 0R >. |
|
7 | 5 6 | bitrdi | |- ( ( A e. RR /\ B e. RR ) -> ( A |