Theorem rpre 12967

Description: A positive real is a real. (Contributed by NM, 27-Oct-2007.) (Proof shortened by Steven Nguyen, 8-Oct-2022.)

Assertion

Ref	Expression
rpre	⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)

Proof of Theorem rpre

Step	Hyp	Ref	Expression
1		rpssre 12966	. 2 ⊢ ℝ+ ⊆ ℝ
2	1	sseli 3945	1 ⊢ (𝐴 ∈ ℝ+ → 𝐴 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11074  ℝ⁺crp 12958

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-ss 3934  df-rp 12959

This theorem is referenced by:  rpxr  12968  rpcn  12969  rpge0  12972  rprege0  12974  rprene0  12976  neglt  12978  rpaddcl  12982  rpmulcl  12983  rpdivcl  12985  rpgecl  12988  ledivge1le  13031  addlelt  13074  xralrple  13172  xlemul1  13257  infmrp1  13312  iccdil  13458  ltdifltdiv  13803  modcl  13842  mod0  13845  mulmod0  13846  modge0  13848  modlt  13849  modid0  13866  modabs  13873  modabs2  13874  modcyc  13875  muladdmod  13884  modmuladd  13885  modmuladdnn0  13887  modltm1p1mod  13895  2txmodxeq0  13903  2submod  13904  moddi  13911  modsubdir  13912  modeqmodmin  13913  modirr  13914  rpexpmord  14140  expnlbnd  14205  rennim  15212  cnpart  15213  01sqrexlem1  15215  01sqrexlem2  15216  01sqrexlem4  15218  01sqrexlem5  15219  01sqrexlem6  15220  01sqrexlem7  15221  resqrex  15223  rpsqrtcl  15237  sqreulem  15333  eqsqrt2d  15342  2clim  15545  reccn2  15570  cn1lem  15571  climsqz  15614  climsqz2  15615  rlimsqzlem  15622  climsup  15643  climcau  15644  caucvgrlem2  15648  iseralt  15658  cvgcmp  15789  cvgcmpce  15791  divrcnv  15825  rprisefaccl  15996  efgt1  16091  ef01bndlem  16159  sinltx  16164  stdbdmet  24411  stdbdmopn  24413  met2ndci  24417  cfilucfil  24454  ngptgp  24531  reperflem  24714  iccntr  24717  reconnlem2  24723  opnreen  24727  metdseq0  24750  xlebnum  24871  cphsqrtcl3  25094  iscmet3lem3  25197  iscmet3lem1  25198  iscmet3lem2  25199  caubl  25215  lmcau  25220  bcthlem4  25234  minveclem3b  25335  minveclem3  25336  ivthlem2  25360  ivthlem3  25361  nulmbl2  25444  opnmbllem  25509  itg2const2  25649  itg2mulclem  25654  dveflem  25890  lhop  25928  dvcnvre  25931  aalioulem2  26248  aaliou  26253  aaliou3lem4  26261  ulmcaulem  26310  ulmcau  26311  ulmcn  26315  itgulm  26324  reeff1o  26364  pilem2  26369  logleb  26519  logcj  26522  argimgt0  26528  logdmnrp  26557  logcnlem3  26560  logcnlem4  26561  advlog  26570  efopnlem1  26572  cxple2  26613  cxplt2  26614  cxple3  26617  2irrexpq  26647  cxpcn3  26665  resqrtcn  26666  relogbf  26708  asinneg  26803  atanbndlem  26842  cxplim  26889  cxp2limlem  26893  cxp2lim  26894  cxploglim  26895  cxploglim2  26896  logdiflbnd  26912  harmoniclbnd  26926  harmonicbnd4  26928  chtrpcl  27092  ppiltx  27094  chtleppi  27128  logfacubnd  27139  logfaclbnd  27140  logfacbnd3  27141  logexprlim  27143  bposlem7  27208  bposlem8  27209  bposlem9  27210  chebbnd1  27390  chtppilim  27393  chto1ub  27394  chpo1ub  27398  vmadivsum  27400  rpvmasumlem  27405  dchrisumlem3  27409  dchrvmasumlem2  27416  dchrvmasumiflem1  27419  dchrisum0  27438  mudivsum  27448  mulogsumlem  27449  mulogsum  27450  mulog2sumlem2  27453  log2sumbnd  27462  selberglem2  27464  selberglem3  27465  selberg  27466  selberg2lem  27468  selberg2  27469  pntrf  27481  pntrmax  27482  pntrsumo1  27483  selbergr  27486  selbergs  27492  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntibndlem1  27507  pntlem3  27527  pntlemp  27528  pntleml  27529  pnt2  27531  padicabvcxp  27550  vacn  30630  nmcvcn  30631  smcnlem  30633  blocnilem  30740  chscllem2  31574  nmcexi  31962  nmcopexi  31963  nmcfnexi  31987  dp2ltsuc  32813  dpval3rp  32827  dplti  32832  dpgti  32833  dpexpp1  32835  dpadd2  32837  pnfinf  33144  sqsscirc1  33905  dya2icoseg2  34276  probfinmeasb  34426  probfinmeasbALTV  34427  signshf  34586  divsqrtid  34592  logdivsqrle  34648  hgt750lem2  34650  subfacval3  35183  opnrebl  36315  opnrebl2  36316  taupilem1  37316  opnmbllem0  37657  itg2addnclem  37672  itg2addnclem2  37673  itg2addnclem3  37674  itg2addnc  37675  itg2gt0cn  37676  ftc1anclem5  37698  ftc1anclem7  37700  ftc1anc  37702  areacirclem1  37709  areacirclem4  37712  areacirc  37714  geomcau  37760  isbnd2  37784  ssbnd  37789  heiborlem7  37818  heiborlem8  37819  bfplem2  37824  rrncmslem  37833  rrnequiv  37836  dvrelog3  42060  aks4d1p1p6  42068  rpabsid  42316  irrapxlem1  42817  irrapxlem2  42818  irrapxlem3  42819  irrapxlem5  42821  2timesgt  45293  supxrge  45341  suplesup  45342  xrlexaddrp  45355  xralrple2  45357  infleinflem1  45373  xralrple4  45376  xralrple3  45377  xrralrecnnle  45386  climinf  45611  mullimc  45621  mullimcf  45628  limcrecl  45634  limcleqr  45649  addlimc  45653  0ellimcdiv  45654  limclner  45656  liminflimsupclim  45812  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  stoweidlem7  46012  fourierdlem73  46184  fourierdlem87  46198  fourierdlem103  46214  fourierdlem104  46215  sge0iunmptlemre  46420  smflimlem4  46779  fldivexpfllog2  48558  blenre  48567  itscnhlc0yqe  48752  itscnhlc0xyqsol  48758  itschlc0xyqsol  48760  itsclc0xyqsolr  48762  itsclinecirc0in  48768  itsclquadb  48769  itscnhlinecirc02plem3  48777  itscnhlinecirc02p  48778  inlinecirc02plem  48779  inlinecirc02p  48780  amgmwlem  49795