MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1red Structured version   Unicode version

Theorem 1red 9665
Description: 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
1red  |-  ( ph  ->  1  e.  RR )

Proof of Theorem 1red
StepHypRef Expression
1 1re 9649 . 2  |-  1  e.  RR
21a1i 11 1  |-  ( ph  ->  1  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1872   RRcr 9545   1c1 9547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-1cn 9604  ax-icn 9605  ax-addcl 9606  ax-mulcl 9608  ax-mulrcl 9609  ax-i2m1 9614  ax-1ne0 9615  ax-rrecex 9618  ax-cnre 9619
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-iota 5565  df-fv 5609  df-ov 6308
This theorem is referenced by:  recgt0  10456  ltrec  10495  nn0p1gt0  10906  nn0ge2m1nn  10941  suprzcl  11022  qbtwnre  11499  iccf1o  11783  xov1plusxeqvd  11785  fznatpl1  11857  elfz1b  11871  fzonn0p1p1  11998  elfzom1p1elfzo  11999  elfznelfzo  12020  elfznelfzob  12021  fladdz  12064  flhalf  12068  ltdifltdiv  12072  modltm1p1mod  12148  ltexp2a  12330  expcan  12331  ltexp2  12332  leexp2  12333  leexp2a  12334  leexp2r  12336  nnlesq  12384  bernneq3  12406  expnbnd  12407  expnlbnd2  12409  fzsdom2  12604  wrdlenge2n0  12707  swrd2lsw  13027  2swrd2eqwrdeq  13028  rddif  13403  reccn2  13659  rlimo1  13679  o1fsum  13872  abscvgcvg  13878  climcndslem1  13906  flo1  13911  harmonic  13916  geomulcvg  13931  fprodrecl  14006  fprodle  14049  bpoly4  14111  efcllem  14131  efgt1  14169  tanhlt1  14213  sinltx  14242  eirrlem  14255  bitsfzolem  14406  bitsfzolemOLD  14407  bitsfzo  14408  bitsmod  14409  bitscmp  14411  bitsinv1lem  14414  smuval2  14455  prmind2  14634  isprm5  14650  coprmgcdb  14653  divdenle  14697  zsqrtelqelz  14706  fermltl  14731  odzdvds  14739  odzdvdsOLD  14745  modprm0  14755  iserodd  14784  pcfaclem  14842  prmreclem1  14859  4sqlem11  14898  4sqlem12  14899  ramub1lem1  14983  prmgaplem8  15027  2expltfac  15062  pgpfaclem2  17714  znidomb  19130  chfacfisf  19876  chfacfisfcpmat  19877  chfacfscmulgsum  19882  chfacfpmmulgsum  19886  nrginvrcnlem  21691  nmoid  21761  xrsmopn  21828  metnrmlem1a  21873  metnrmlem1aOLD  21888  iccpnfhmeo  21971  htpycc  22009  pcohtpylem  22048  pcoass  22053  pcorevlem  22055  nmhmcn  22132  cncmet  22288  ovoliunlem1  22453  dyadmaxlem  22553  vitalilem2  22565  mbfi1fseqlem6  22676  itg2mulc  22703  itg2monolem1  22706  itg2monolem3  22708  dveflem  22929  mvth  22942  dvlipcn  22944  lhop1lem  22963  dvfsumlem1  22976  dvfsumlem2  22977  dvfsumlem3  22978  dvfsumlem4  22979  dvfsum2  22984  fta1glem2  23115  plyeq0lem  23162  fta1lem  23258  vieta1lem2  23262  aalioulem3  23288  aalioulem4  23289  radcnvlem1  23366  radcnvlem2  23367  dvradcnv  23374  abelthlem2  23385  abelthlem5  23388  abelthlem7  23391  abelth2  23395  cosne0  23477  rplogcl  23551  logdivlti  23567  logno1  23579  advlog  23597  logtayllem  23602  cxplt  23637  cxple  23638  cxpaddlelem  23689  cxpaddle  23690  relogbf  23726  isosctrlem1  23745  isosctrlem2  23746  heron  23762  atanlogaddlem  23837  bndatandm  23853  leibpi  23866  log2tlbnd  23869  birthdaylem3  23877  rlimcnp  23889  rlimcnp2  23890  efrlim  23893  cxp2limlem  23899  divsqrtsumo1  23907  jensenlem2  23911  logdiflbnd  23918  fsumharmonic  23935  lgamgulmlem2  23953  lgamgulmlem3  23954  lgamgulmlem4  23955  lgamgulmlem5  23956  lgamgulmlem6  23957  lgamcvg2  23978  regamcl  23984  wilthlem2  23992  ftalem2  23996  basellem9  24013  vma1  24091  ppieq0  24101  mumullem2  24105  fsumfldivdiaglem  24116  chpeq0  24134  chtub  24138  chpval2  24144  chpchtsum  24145  chpub  24146  logfacrlim  24150  logexprlim  24151  mersenne  24153  perfectlem2  24156  dchrelbas4  24169  bcmono  24203  bposlem1  24210  bposlem2  24211  lgslem3  24224  lgslem4  24225  lgsmod  24247  lgsdir2lem4  24252  lgsdirprm  24255  lgsquadlem2  24281  2sqlem8  24298  chebbnd1lem1  24305  chebbnd1lem2  24306  chtppilimlem1  24309  chebbnd2  24313  chto1lb  24314  chpchtlim  24315  chpo1ubb  24317  vmadivsum  24318  rplogsumlem1  24320  rpvmasumlem  24323  dchrisumlem3  24327  dchrmusumlema  24329  dchrmusum2  24330  dchrvmasumlem2  24334  dchrvmasumlem3  24335  dchrvmasumiflem1  24337  dchrvmasumiflem2  24338  dchrisum0flblem1  24344  dchrisum0flblem2  24345  dchrisum0fno1  24347  dchrisum0re  24349  dchrisum0lema  24350  dchrisum0lem1b  24351  dchrisum0lem2a  24353  dchrisum0lem2  24354  dchrisum0lem3  24355  rplogsum  24363  dirith2  24364  mudivsum  24366  mulogsumlem  24367  mulogsum  24368  mulog2sumlem1  24370  mulog2sumlem2  24371  vmalogdivsum2  24374  vmalogdivsum  24375  2vmadivsumlem  24376  log2sumbnd  24380  selberglem2  24382  selberg2lem  24386  chpdifbnd  24391  selberg3lem1  24393  selberg3  24395  selberg4lem1  24396  selberg4  24397  pntrmax  24400  pntrsumo1  24401  pntrsumbnd  24402  selberg3r  24405  selberg4r  24406  selberg34r  24407  pntrlog2bndlem1  24413  pntrlog2bndlem2  24414  pntrlog2bndlem3  24415  pntrlog2bndlem4  24416  pntrlog2bndlem5  24417  pntrlog2bndlem6  24419  pntrlog2bnd  24420  pntpbnd1a  24421  pntpbnd1  24422  pntibndlem2a  24426  pntibndlem2  24427  pntibnd  24429  pntlemc  24431  pntlemg  24434  pntlemr  24438  pntlemk  24442  qabvle  24461  ostth2lem3  24471  ostth2  24473  trgcgrg  24558  tgcgr4  24574  ttgcontlem1  24913  axpaschlem  24968  axlowdimlem16  24985  axcontlem2  24993  axcontlem7  24998  wwlkm1edg  25461  wwlkextproplem1  25467  wwlkextproplem2  25468  clwlkisclwwlklem2fv1  25508  clwlkisclwwlklem2fv2  25509  clwlkisclwwlklem1  25513  clwlkisclwwlk2  25516  clwwlkf1  25522  clwwlkext2edg  25528  clwwisshclwwlem  25532  usg2cwwkdifex  25547  extwwlkfablem2  25804  numclwwlkovf2ex  25812  numclwlk1lem2f1  25820  numclwwlk7  25840  frgrareggt1  25842  frgraregord013  25844  frgraogt3nreg  25846  smcnlem  26331  nmoub3i  26412  blocnilem  26443  ubthlem2  26511  minvecolem4  26520  minvecolem4OLD  26530  htthlem  26568  nmcexi  27677  nmopcoi  27746  cdj1i  28084  nn0sqeq1  28330  nndiffz1  28372  fzsplit3  28376  pmtrto1cl  28620  fzto1st1  28623  fzto1st  28624  psgnfzto1st  28626  1smat1  28638  submateqlem1  28641  madjusmdetlem2  28662  unitdivcld  28715  sqsscirc1  28722  nexple  28839  indf1o  28853  esumdivc  28912  dya2ub  29100  dya2iocress  29104  dya2iocbrsiga  29105  dya2icobrsiga  29106  dya2icoseg  29107  dya2iocucvr  29114  sxbrsigalem2  29116  fibp1  29242  probmeasb  29271  dstrvprob  29312  dstfrvunirn  29315  ballotlemfc0  29333  ballotlemfcc  29334  ballotlemsgt1  29351  ballotlemsel1i  29353  ballotlemfrcn0  29370  ballotlemsgt1OLD  29389  ballotlemsel1iOLD  29391  ballotlemfrcn0OLD  29408  signsply0  29448  subfaclim  29919  cvmliftlem2  30017  cvmliftlem13  30027  snmlff  30060  bccolsum  30382  faclim  30389  nn0prpwlem  30983  poimirlem6  31910  poimirlem7  31911  poimirlem15  31919  poimirlem19  31923  poimirlem29  31933  poimirlem30  31934  poimirlem31  31935  poimirlem32  31936  broucube  31938  itg2addnclem2  31958  itg2addnclem3  31959  areacirclem1  31996  areacirclem4  31999  incsequz  32041  totbndbnd  32085  bfplem2  32119  lzenom  35581  irrapxlem1  35636  irrapxlem2  35637  irrapxlem4  35639  irrapxlem5  35640  pellexlem2  35644  pell1qrge1  35686  pell1qr1  35687  elpell1qr2  35688  pell14qrgapw  35692  pellfundgt1  35701  pellfundglb  35703  pellfundex  35704  pellfundrp  35706  pellfundne1  35707  rmspecnonsq  35725  rmspecfund  35727  rmspecpos  35734  monotoddzzfi  35760  rmygeid  35784  areaquad  36071  imo72b2lem0  36578  imo72b2lem1  36584  imo72b2  36589  isprm7  36630  cvgdvgrat  36632  radcnvrat  36633  hashnzfzclim  36641  lhe4.4ex1a  36648  binomcxplemnn0  36668  binomcxplemdvbinom  36672  binomcxplemnotnn0  36675  oddfl  37441  abscosbd  37442  zltlesub  37449  abssinbd  37466  monoords  37468  fzisoeu  37472  fzdifsuc2  37484  suplesup  37516  xralrple2  37531  fmul01  37598  fmul01lt1lem1  37602  fmul01lt1lem2  37603  climsuselem1  37626  sumnnodd  37650  0ellimcdiv  37670  dvmptidg  37727  dvcosax  37738  ioodvbdlimc1lem1  37743  ioodvbdlimc1lem2  37744  ioodvbdlimc1lem1OLD  37745  ioodvbdlimc1lem2OLD  37746  ioodvbdlimc2lem  37748  ioodvbdlimc2lemOLD  37749  dvxpaek  37755  dvnmul  37758  iblspltprt  37790  itgspltprt  37796  stoweidlem5  37805  stoweidlem7  37807  stoweidlem10  37810  stoweidlem11  37811  stoweidlem12  37812  stoweidlem13  37813  stoweidlem14  37814  stoweidlem16  37816  stoweidlem18  37818  stoweidlem20  37820  stoweidlem24  37824  stoweidlem25  37825  stoweidlem34  37835  stoweidlem36  37837  stoweidlem38  37839  stoweidlem40  37841  stoweidlem41  37842  stoweidlem42  37843  stoweidlem45  37846  stoweidlem51  37852  stoweidlem60  37861  wallispilem3  37869  wallispilem4  37870  wallispilem5  37871  wallispi  37872  wallispi2lem1  37873  wallispi2lem2  37874  wallispi2  37875  stirlinglem1  37876  stirlinglem3  37878  stirlinglem5  37880  stirlinglem6  37881  stirlinglem7  37882  stirlinglem8  37883  stirlinglem10  37885  stirlinglem11  37886  stirlinglem12  37887  stirlinglem13  37888  stirlinglem15  37890  dirker2re  37894  dirkerval2  37896  dirkerre  37897  dirkertrigeqlem1  37900  dirkertrigeqlem3  37902  dirkeritg  37904  dirkercncflem1  37905  dirkercncflem2  37906  dirkercncflem4  37908  fourierdlem5  37914  fourierdlem6  37915  fourierdlem11  37920  fourierdlem15  37924  fourierdlem19  37928  fourierdlem20  37929  fourierdlem24  37933  fourierdlem26  37935  fourierdlem28  37937  fourierdlem30  37939  fourierdlem39  37949  fourierdlem41  37951  fourierdlem43  37954  fourierdlem47  37957  fourierdlem48  37958  fourierdlem56  37966  fourierdlem60  37970  fourierdlem61  37971  fourierdlem62  37972  fourierdlem64  37974  fourierdlem65  37975  fourierdlem66  37976  fourierdlem68  37978  fourierdlem73  37983  fourierdlem78  37988  fourierdlem79  37989  fourierdlem87  37997  fourierdlem103  38013  fourierdlem104  38014  sqwvfoura  38032  fouriersw  38035  etransclem4  38043  etransclem23  38062  etransclem24  38063  etransclem31  38070  etransclem32  38071  etransclem35  38074  etransclem41  38080  etransclem46  38085  etransclem48OLD  38087  etransclem48  38088  etransc  38089  nnfoctbdjlem  38201  iundjiun  38206  hoidmvlelem1  38321  hoidmvlelem2  38322  hoidmvlelem3  38323  hoidmvlelem4  38324  ovnhoilem1  38327  sigaradd  38346  m1mod0mod1  38593  mod2eq1n2dvds  38595  iccpartiltu  38606  iccpartlt  38608  iccpartgt  38611  nnoALTV  38694  bgoldbtbndlem4  38773  proththdlem  38783  proththd  38784  pfx2  38823  p1lep2  38900  zm1nn  38903  cznnring  39577  nn0le2is012  39769  divge1b  39929  divgt1b  39930  m1modmmod  39945  difmodm1lt  39946  nn0o1gt2  39948  nno  39949  nn0eo  39956  regt1loggt0  39968  rege1logbrege0  39990  logblt1b  39996  fllog2  40000  nnolog2flm1  40022  dignn0flhalflem1  40047  reseccl  40094  recsccl  40095
  Copyright terms: Public domain W3C validator