Theorem rpgt0 13047

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 13036	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
2	1	simprbi 496	1 ⊢ (𝐴 ∈ ℝ+ → 0 < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5143  ℝcr 11154  0cc0 11155   < clt 11295  ℝ⁺crp 13034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-rp 13035

This theorem is referenced by:  rpge0  13048  rpgecl  13063  0nrp  13070  rpgt0d  13080  addlelt  13149  0mod  13942  sgnrrp  15130  01sqrexlem2  15282  01sqrexlem4  15284  01sqrexlem6  15286  resqrex  15289  rpsqrtcl  15303  climconst  15579  rlimconst  15580  divrcnv  15888  rprisefaccl  16059  blcntrps  24422  blcntr  24423  stdbdmet  24529  stdbdmopn  24531  prdsxmslem2  24542  metustid  24567  nmoix  24750  metdseq0  24876  lebnumii  24998  itgulm  26451  pilem2  26496  cos02pilt1  26568  tanregt0  26581  logdmnrp  26683  cxple2  26739  asinneg  26929  asin1  26937  reasinsin  26939  atanbndlem  26968  atanbnd  26969  atan1  26971  rlimcnp  27008  chtrpcl  27218  ppiltx  27220  bposlem8  27335  pntlem3  27653  padicabvcxp  27676  0cnop  31998  0cnfn  31999  rpdp2cl  32864  xdivpnfrp  32915  pnfinf  33190  hgt750lem2  34667  taupilem1  37322  itg2gt0cn  37682  areacirclem1  37715  areacirclem4  37718  prdstotbnd  37801  prdsbnd2  37802  aks4d1p1p6  42074  irrapxlem3  42835  neglt  45296  xralrple2  45365  constlimc  45639  0cnv  45757  ioodvbdlimc1lem1  45946  fourierdlem103  46224  fourierdlem104  46225  etransclem18  46267  etransclem46  46295  hoidmvlelem3  46612