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	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A{<}_{ℝ}B\leftrightarrow 1^{st}\left(A\right){<}_{𝑹}{1}^{st}\left(B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		elreal2	$$⊢A\in ℝ\leftrightarrow \left(1^{st}\left(A\right)\in 𝑹\wedge A=⟨1^{st}\left(A\right),0_{𝑹}⟩\right)$$
2	1	simprbi	$$⊢A\in ℝ\to A=⟨1^{st}\left(A\right),0_{𝑹}⟩$$
3		elreal2	$$⊢B\in ℝ\leftrightarrow \left(1^{st}\left(B\right)\in 𝑹\wedge B=⟨1^{st}\left(B\right),0_{𝑹}⟩\right)$$
4	3	simprbi	$$⊢B\in ℝ\to B=⟨1^{st}\left(B\right),0_{𝑹}⟩$$
5	2 4	breqan12d	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A{<}_{ℝ}B\leftrightarrow ⟨1^{st}\left(A\right),0_{𝑹}⟩{<}_{ℝ}⟨1^{st}\left(B\right),0_{𝑹}⟩\right)$$
6		ltresr	$$⊢⟨1^{st}\left(A\right),0_{𝑹}⟩{<}_{ℝ}⟨1^{st}\left(B\right),0_{𝑹}⟩\leftrightarrow 1^{st}\left(A\right){<}_{𝑹}{1}^{st}\left(B\right)$$
7	5 6	syl6bb	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A{<}_{ℝ}B\leftrightarrow 1^{st}\left(A\right){<}_{𝑹}{1}^{st}\left(B\right)\right)$$