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 )