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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 <_ℝ 𝐵 ↔ ( 1^st ‘ 𝐴 ) <_R ( 1^st ‘ 𝐵 ) ) )

Step	Hyp	Ref	Expression
1		elreal2	⊢ ( 𝐴 ∈ ℝ ↔ ( ( 1^st ‘ 𝐴 ) ∈ R ∧ 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , 0_R ⟩ ) )
2	1	simprbi	⊢ ( 𝐴 ∈ ℝ → 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , 0_R ⟩ )
3		elreal2	⊢ ( 𝐵 ∈ ℝ ↔ ( ( 1^st ‘ 𝐵 ) ∈ R ∧ 𝐵 = ⟨ ( 1^st ‘ 𝐵 ) , 0_R ⟩ ) )
4	3	simprbi	⊢ ( 𝐵 ∈ ℝ → 𝐵 = ⟨ ( 1^st ‘ 𝐵 ) , 0_R ⟩ )
5	2 4	breqan12d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 <_ℝ 𝐵 ↔ ⟨ ( 1^st ‘ 𝐴 ) , 0_R ⟩ <_ℝ ⟨ ( 1^st ‘ 𝐵 ) , 0_R ⟩ ) )
6		ltresr	⊢ ( ⟨ ( 1^st ‘ 𝐴 ) , 0_R ⟩ <_ℝ ⟨ ( 1^st ‘ 𝐵 ) , 0_R ⟩ ↔ ( 1^st ‘ 𝐴 ) <_R ( 1^st ‘ 𝐵 ) )
7	5 6	bitrdi	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 <_ℝ 𝐵 ↔ ( 1^st ‘ 𝐴 ) <_R ( 1^st ‘ 𝐵 ) ) )

Metamath Proof Explorer