Theorem rpgt0 11844

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

Syntax hints:   → wi 4   ∈ wcel 1990   class class class wbr 4653  ℝcr 9935  0cc0 9936   < clt 10074  ℝ⁺crp 11832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-rp 11833

This theorem is referenced by:  rpge0  11845  rpgecl  11859  0nrp  11865  rpgt0d  11875  addlelt  11942  0mod  12701  sgnrrp  13831  sqrlem2  13984  sqrlem4  13986  sqrlem6  13988  resqrex  13991  rpsqrtcl  14005  climconst  14274  rlimconst  14275  divrcnv  14584  rprisefaccl  14754  blcntrps  22217  blcntr  22218  stdbdmet  22321  stdbdmopn  22323  prdsxmslem2  22334  metustid  22359  nmoix  22533  metdseq0  22657  lebnumii  22765  itgulm  24162  pilem2  24206  tanregt0  24285  logdmnrp  24387  cxple2  24443  asinneg  24613  asin1  24621  reasinsin  24623  atanbndlem  24652  atanbnd  24653  atan1  24655  rlimcnp  24692  chtrpcl  24901  ppiltx  24903  bposlem8  25016  pntlem3  25298  padicabvcxp  25321  0cnop  28838  0cnfn  28839  rpdp2cl  29589  xdivpnfrp  29641  pnfinf  29737  hgt750lem2  30730  taupilem1  33167  itg2gt0cn  33465  areacirclem1  33500  areacirclem4  33503  prdstotbnd  33593  prdsbnd2  33594  irrapxlem3  37388  neglt  39496  xralrple2  39570  constlimc  39856  0cnv  39974  ioodvbdlimc1lem1  40146  fourierdlem103  40426  fourierdlem104  40427  etransclem18  40469  etransclem46  40497  hoidmvlelem3  40811