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

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

Metamath Proof Explorer