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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( 1st𝐴 ) <R ( 1st𝐵 ) ) )

Proof

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