Theorem rpgt0 12770

Description: A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.)

Assertion

Ref	Expression
rpgt0	⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)

Proof of Theorem rpgt0

Step	Hyp	Ref	Expression
1		elrp 12760	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
2	1	simprbi 496	1 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2101   class class class wbr 5077  ℝcr 10898  0cc0 10899   < clt 11037  ℝ⁺crp 12758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2063  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3224  df-v 3436  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4260  df-if 4463  df-sn 4565  df-pr 4567  df-op 4571  df-br 5078  df-rp 12759

This theorem is referenced by:  rpge0  12771  rpgecl  12786  0nrp  12793  rpgt0d  12803  addlelt  12872  0mod  13650  sgnrrp  14830  sqrlem2  14983  sqrlem4  14985  sqrlem6  14987  resqrex  14990  rpsqrtcl  15004  climconst  15280  rlimconst  15281  divrcnv  15592  rprisefaccl  15761  blcntrps  23593  blcntr  23594  stdbdmet  23700  stdbdmopn  23702  prdsxmslem2  23713  metustid  23738  nmoix  23921  metdseq0  24045  lebnumii  24157  itgulm  25595  pilem2  25639  cos02pilt1  25710  tanregt0  25723  logdmnrp  25824  cxple2  25880  asinneg  26064  asin1  26072  reasinsin  26074  atanbndlem  26103  atanbnd  26104  atan1  26106  rlimcnp  26143  chtrpcl  26352  ppiltx  26354  bposlem8  26467  pntlem3  26785  padicabvcxp  26808  0cnop  30369  0cnfn  30370  rpdp2cl  31184  xdivpnfrp  31235  pnfinf  31465  hgt750lem2  32660  taupilem1  35520  itg2gt0cn  35860  areacirclem1  35893  areacirclem4  35896  prdstotbnd  35980  prdsbnd2  35981  aks4d1p1p6  40107  irrapxlem3  40669  neglt  42857  xralrple2  42927  constlimc  43200  0cnv  43318  ioodvbdlimc1lem1  43507  fourierdlem103  43785  fourierdlem104  43786  etransclem18  43828  etransclem46  43856  hoidmvlelem3  44171