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

Theorem rpregt0d 8727
Description: A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
rpred.1 (𝜑𝐴 ∈ ℝ+)
Assertion
Ref Expression
rpregt0d (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Proof of Theorem rpregt0d
StepHypRef Expression
1 rpred.1 . . 3 (𝜑𝐴 ∈ ℝ+)
21rpred 8720 . 2 (𝜑𝐴 ∈ ℝ)
31rpgt0d 8723 . 2 (𝜑 → 0 < 𝐴)
42, 3jca 294 1 (𝜑 → (𝐴 ∈ ℝ ∧ 0 < 𝐴))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  wcel 1409   class class class wbr 3792  cr 6946  0cc0 6947   < clt 7119  +crp 8681
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-rab 2332  df-v 2576  df-un 2950  df-in 2952  df-ss 2959  df-sn 3409  df-pr 3410  df-op 3412  df-br 3793  df-rp 8682
This theorem is referenced by:  reclt1d  8734  recgt1d  8735  ltrecd  8739  lerecd  8740  ltrec1d  8741  lerec2d  8742  lediv2ad  8743  ltdiv2d  8744  lediv2d  8745  ledivdivd  8746  divge0d  8761  ltmul1d  8762  ltmul2d  8763  lemul1d  8764  lemul2d  8765  ltdiv1d  8766  lediv1d  8767  ltmuldivd  8768  ltmuldiv2d  8769  lemuldivd  8770  lemuldiv2d  8771  ltdivmuld  8772  ltdivmul2d  8773  ledivmuld  8774  ledivmul2d  8775  ltdiv23d  8781  lediv23d  8782  lt2mul2divd  8783
  Copyright terms: Public domain W3C validator