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 B A < B 1 st A < 𝑹 1 st B

Proof

Step Hyp Ref Expression
1 elreal2 A 1 st A 𝑹 A = 1 st A 0 𝑹
2 1 simprbi A A = 1 st A 0 𝑹
3 elreal2 B 1 st B 𝑹 B = 1 st B 0 𝑹
4 3 simprbi B B = 1 st B 0 𝑹
5 2 4 breqan12d A B A < B 1 st A 0 𝑹 < 1 st B 0 𝑹
6 ltresr 1 st A 0 𝑹 < 1 st B 0 𝑹 1 st A < 𝑹 1 st B
7 5 6 bitrdi A B A < B 1 st A < 𝑹 1 st B