Theorem rpgt0 12953

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

Syntax hints:   → wi 4   ∈ wcel 2119   class class class wbr 5079  ℝcr 11035  0cc0 11036   < clt 11177  ℝ⁺crp 12940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-rp 12941

This theorem is referenced by:  rpge0  12954  neglt  12960  rpgecl  12970  0nrp  12977  rpgt0d  12987  addlelt  13056  0mod  13859  sgnrrp  15051  01sqrexlem2  15203  01sqrexlem4  15205  01sqrexlem6  15207  resqrex  15210  rpsqrtcl  15224  climconst  15503  rlimconst  15504  divrcnv  15815  rprisefaccl  15986  blcntrps  24402  blcntr  24403  stdbdmet  24506  stdbdmopn  24508  prdsxmslem2  24519  metustid  24544  nmoix  24719  metdseq0  24845  lebnumii  24958  itgulm  26398  pilem2  26442  cos02pilt1  26515  tanregt0  26528  logdmnrp  26630  cxple2  26686  asinneg  26875  asin1  26883  reasinsin  26885  atanbndlem  26914  atanbnd  26915  atan1  26917  rlimcnp  26954  chtrpcl  27163  ppiltx  27165  bposlem8  27279  pntlem3  27597  padicabvcxp  27620  0cnop  32075  0cnfn  32076  rpdp2cl  32967  xdivpnfrp  33018  pnfinf  33271  hgt750lem2  34843  taupilem1  37682  itg2gt0cn  38043  areacirclem1  38076  areacirclem4  38079  prdstotbnd  38162  prdsbnd2  38163  aks4d1p1p6  42559  irrapxlem3  43270  xralrple2  45800  constlimc  46070  0cnv  46186  ioodvbdlimc1lem1  46375  fourierdlem103  46653  fourierdlem104  46654  etransclem18  46696  etransclem46  46724  hoidmvlelem3  47041