Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltresr2 GIF version

Theorem ltresr2 6916
 Description: Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
Assertion
Ref Expression
ltresr2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (1st𝐴) <R (1st𝐵)))

Proof of Theorem ltresr2
StepHypRef Expression
1 elreal2 6907 . . . 4 (𝐴 ∈ ℝ ↔ ((1st𝐴) ∈ R𝐴 = ⟨(1st𝐴), 0R⟩))
21simprbi 260 . . 3 (𝐴 ∈ ℝ → 𝐴 = ⟨(1st𝐴), 0R⟩)
3 elreal2 6907 . . . 4 (𝐵 ∈ ℝ ↔ ((1st𝐵) ∈ R𝐵 = ⟨(1st𝐵), 0R⟩))
43simprbi 260 . . 3 (𝐵 ∈ ℝ → 𝐵 = ⟨(1st𝐵), 0R⟩)
52, 4breqan12d 3779 . 2 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ ⟨(1st𝐴), 0R⟩ < ⟨(1st𝐵), 0R⟩))
6 ltresr 6915 . 2 (⟨(1st𝐴), 0R⟩ < ⟨(1st𝐵), 0R⟩ ↔ (1st𝐴) <R (1st𝐵))
75, 6syl6bb 185 1 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (1st𝐴) <R (1st𝐵)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1243   ∈ wcel 1393  ⟨cop 3378   class class class wbr 3764  ‘cfv 4902  1st c1st 5765  Rcnr 6395  0Rc0r 6396
 Copyright terms: Public domain W3C validator