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

Theorem prsrpos 7616
 Description: Mapping from a positive real to a signed real yields a result greater than zero. (Contributed by Jim Kingdon, 25-Jun-2021.)
Assertion
Ref Expression
prsrpos (𝐴P → 0R <R [⟨(𝐴 +P 1P), 1P⟩] ~R )

Proof of Theorem prsrpos
StepHypRef Expression
1 1pr 7385 . . . 4 1PP
2 ltaddpr 7428 . . . 4 ((1PP𝐴P) → 1P<P (1P +P 𝐴))
31, 2mpan 421 . . 3 (𝐴P → 1P<P (1P +P 𝐴))
4 addcomprg 7409 . . . 4 ((1PP𝐴P) → (1P +P 𝐴) = (𝐴 +P 1P))
51, 4mpan 421 . . 3 (𝐴P → (1P +P 𝐴) = (𝐴 +P 1P))
63, 5breqtrd 3961 . 2 (𝐴P → 1P<P (𝐴 +P 1P))
7 gt0srpr 7579 . 2 (0R <R [⟨(𝐴 +P 1P), 1P⟩] ~R ↔ 1P<P (𝐴 +P 1P))
86, 7sylibr 133 1 (𝐴P → 0R <R [⟨(𝐴 +P 1P), 1P⟩] ~R )
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1332   ∈ wcel 1481  ⟨cop 3534   class class class wbr 3936  (class class class)co 5781  [cec 6434  Pcnp 7122  1Pc1p 7123   +P cpp 7124
 Copyright terms: Public domain W3C validator