Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  gt0srpr Structured version   Visualization version   GIF version

Theorem gt0srpr 9778
 Description: Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
Assertion
Ref Expression
gt0srpr (0R <R [⟨𝐴, 𝐵⟩] ~R𝐵<P 𝐴)

Proof of Theorem gt0srpr
StepHypRef Expression
1 ltsrpr 9777 . 2 ([⟨1P, 1P⟩] ~R <R [⟨𝐴, 𝐵⟩] ~R ↔ (1P +P 𝐵)<P (1P +P 𝐴))
2 df-0r 9761 . . 3 0R = [⟨1P, 1P⟩] ~R
32breq1i 4590 . 2 (0R <R [⟨𝐴, 𝐵⟩] ~R ↔ [⟨1P, 1P⟩] ~R <R [⟨𝐴, 𝐵⟩] ~R )
4 1pr 9716 . . 3 1PP
5 ltapr 9746 . . 3 (1PP → (𝐵<P 𝐴 ↔ (1P +P 𝐵)<P (1P +P 𝐴)))
64, 5ax-mp 5 . 2 (𝐵<P 𝐴 ↔ (1P +P 𝐵)<P (1P +P 𝐴))
71, 3, 63bitr4i 291 1 (0R <R [⟨𝐴, 𝐵⟩] ~R𝐵<P 𝐴)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∈ wcel 1977  ⟨cop 4131   class class class wbr 4583  (class class class)co 6549  [cec 7627  Pcnp 9560  1Pc1p 9561   +P cpp 9562
 Copyright terms: Public domain W3C validator