Theorem rpregt0 11846

Description: A positive real is a positive real number. (Contributed by NM, 11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.)

Assertion

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

Proof of Theorem rpregt0

Step	Hyp	Ref	Expression
1		elrp 11834	. 2 ⊢ (𝐴 ∈ ℝ+ ↔ (𝐴 ∈ ℝ ∧ 0 < 𝐴))
2	1	biimpi 206	1 ⊢ (𝐴 ∈ ℝ+ → (𝐴 ∈ ℝ ∧ 0 < 𝐴))

Syntax hints:   → wi 4   ∧ wa 384   ∈ 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:  rpne0  11848  divlt1lt  11899  divle1le  11900  ledivge1le  11901  nnledivrp  11940  modge0  12678  modlt  12679  modid  12695  modmuladdnn0  12714  expnlbnd  12994  o1fsum  14545  isprm6  15426  gexexlem  18255  lmnn  23061  aaliou2b  24096  harmonicbnd4  24737  logfaclbnd  24947  logfacrlim  24949  chto1ub  25165  vmadivsum  25171  dchrmusumlema  25182  dchrvmasumlem2  25187  dchrisum0lem2a  25206  dchrisum0lem2  25207  dchrisum0lem3  25208  mulogsumlem  25220  mulog2sumlem2  25224  selberg2lem  25239  selberg3lem1  25246  pntrmax  25253  pntrsumo1  25254  pntibndlem3  25281  divge1b  42302  divgt1b  42303