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

Theorem 1red 9689
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 9673 . 2  |-  1  e.  RR
21a1i 11 1  |-  ( ph  ->  1  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1898   RRcr 9569   1c1 9571
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-1cn 9628  ax-icn 9629  ax-addcl 9630  ax-mulcl 9632  ax-mulrcl 9633  ax-i2m1 9638  ax-1ne0 9639  ax-rrecex 9642  ax-cnre 9643
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4419  df-iota 5569  df-fv 5613  df-ov 6323
This theorem is referenced by:  recgt0  10482  ltrec  10521  nn0p1gt0  10933  nn0ge2m1nn  10968  suprzcl  11049  qbtwnre  11526  iccf1o  11811  xov1plusxeqvd  11813  fznatpl1  11885  elfz1b  11899  fzonn0p1p1  12029  elfzom1p1elfzo  12030  elfznelfzo  12051  elfznelfzob  12052  fladdz  12096  flhalf  12100  ltdifltdiv  12104  modltm1p1mod  12180  ltexp2a  12362  expcan  12363  ltexp2  12364  leexp2  12365  leexp2a  12366  leexp2r  12368  nnlesq  12416  bernneq3  12438  expnbnd  12439  expnlbnd2  12441  fzsdom2  12639  wrdlenge2n0  12745  swrd2lsw  13082  2swrd2eqwrdeq  13083  rddif  13458  reccn2  13715  rlimo1  13735  o1fsum  13928  abscvgcvg  13934  climcndslem1  13962  flo1  13967  harmonic  13972  geomulcvg  13987  fprodrecl  14062  fprodle  14105  bpoly4  14167  efcllem  14187  efgt1  14225  tanhlt1  14269  sinltx  14298  eirrlem  14311  bitsfzolem  14462  bitsfzolemOLD  14463  bitsfzo  14464  bitsmod  14465  bitscmp  14467  bitsinv1lem  14470  smuval2  14511  prmind2  14690  isprm5  14706  coprmgcdb  14709  divdenle  14753  zsqrtelqelz  14762  fermltl  14787  odzdvds  14795  odzdvdsOLD  14801  modprm0  14811  iserodd  14840  pcfaclem  14898  prmreclem1  14915  4sqlem11  14954  4sqlem12  14955  ramub1lem1  15039  prmgaplem8  15083  2expltfac  15118  pgpfaclem2  17770  znidomb  19187  chfacfisf  19933  chfacfisfcpmat  19934  chfacfscmulgsum  19939  chfacfpmmulgsum  19943  nrginvrcnlem  21748  nmoid  21818  xrsmopn  21885  metnrmlem1a  21930  metnrmlem1aOLD  21945  iccpnfhmeo  22028  htpycc  22066  pcohtpylem  22105  pcoass  22110  pcorevlem  22112  nmhmcn  22189  cncmet  22345  ovoliunlem1  22510  dyadmaxlem  22611  vitalilem2  22623  mbfi1fseqlem6  22734  itg2mulc  22761  itg2monolem1  22764  itg2monolem3  22766  dveflem  22987  mvth  23000  dvlipcn  23002  lhop1lem  23021  dvfsumlem1  23034  dvfsumlem2  23035  dvfsumlem3  23036  dvfsumlem4  23037  dvfsum2  23042  fta1glem2  23173  plyeq0lem  23220  fta1lem  23316  vieta1lem2  23320  aalioulem3  23346  aalioulem4  23347  radcnvlem1  23424  radcnvlem2  23425  dvradcnv  23432  abelthlem2  23443  abelthlem5  23446  abelthlem7  23449  abelth2  23453  cosne0  23535  rplogcl  23609  logdivlti  23625  logno1  23637  advlog  23655  logtayllem  23660  cxplt  23695  cxple  23696  cxpaddlelem  23747  cxpaddle  23748  relogbf  23784  isosctrlem1  23803  isosctrlem2  23804  heron  23820  atanlogaddlem  23895  bndatandm  23911  leibpi  23924  log2tlbnd  23927  birthdaylem3  23935  rlimcnp  23947  rlimcnp2  23948  efrlim  23951  cxp2limlem  23957  divsqrtsumo1  23965  jensenlem2  23969  logdiflbnd  23976  fsumharmonic  23993  lgamgulmlem2  24011  lgamgulmlem3  24012  lgamgulmlem4  24013  lgamgulmlem5  24014  lgamgulmlem6  24015  lgamcvg2  24036  regamcl  24042  wilthlem2  24050  ftalem2  24054  basellem9  24071  vma1  24149  ppieq0  24159  mumullem2  24163  fsumfldivdiaglem  24174  chpeq0  24192  chtub  24196  chpval2  24202  chpchtsum  24203  chpub  24204  logfacrlim  24208  logexprlim  24209  mersenne  24211  perfectlem2  24214  dchrelbas4  24227  bcmono  24261  bposlem1  24268  bposlem2  24269  lgslem3  24282  lgslem4  24283  lgsmod  24305  lgsdir2lem4  24310  lgsdirprm  24313  lgsquadlem2  24339  2sqlem8  24356  chebbnd1lem1  24363  chebbnd1lem2  24364  chtppilimlem1  24367  chebbnd2  24371  chto1lb  24372  chpchtlim  24373  chpo1ubb  24375  vmadivsum  24376  rplogsumlem1  24378  rpvmasumlem  24381  dchrisumlem3  24385  dchrmusumlema  24387  dchrmusum2  24388  dchrvmasumlem2  24392  dchrvmasumlem3  24393  dchrvmasumiflem1  24395  dchrvmasumiflem2  24396  dchrisum0flblem1  24402  dchrisum0flblem2  24403  dchrisum0fno1  24405  dchrisum0re  24407  dchrisum0lema  24408  dchrisum0lem1b  24409  dchrisum0lem2a  24411  dchrisum0lem2  24412  dchrisum0lem3  24413  rplogsum  24421  dirith2  24422  mudivsum  24424  mulogsumlem  24425  mulogsum  24426  mulog2sumlem1  24428  mulog2sumlem2  24429  vmalogdivsum2  24432  vmalogdivsum  24433  2vmadivsumlem  24434  log2sumbnd  24438  selberglem2  24440  selberg2lem  24444  chpdifbnd  24449  selberg3lem1  24451  selberg3  24453  selberg4lem1  24454  selberg4  24455  pntrmax  24458  pntrsumo1  24459  pntrsumbnd  24460  selberg3r  24463  selberg4r  24464  selberg34r  24465  pntrlog2bndlem1  24471  pntrlog2bndlem2  24472  pntrlog2bndlem3  24473  pntrlog2bndlem4  24474  pntrlog2bndlem5  24475  pntrlog2bndlem6  24477  pntrlog2bnd  24478  pntpbnd1a  24479  pntpbnd1  24480  pntibndlem2a  24484  pntibndlem2  24485  pntibnd  24487  pntlemc  24489  pntlemg  24492  pntlemr  24496  pntlemk  24500  qabvle  24519  ostth2lem3  24529  ostth2  24531  trgcgrg  24616  tgcgr4  24632  ttgcontlem1  24971  axpaschlem  25026  axlowdimlem16  25043  axcontlem2  25051  axcontlem7  25056  wwlkm1edg  25519  wwlkextproplem1  25525  wwlkextproplem2  25526  clwlkisclwwlklem2fv1  25566  clwlkisclwwlklem2fv2  25567  clwlkisclwwlklem1  25571  clwlkisclwwlk2  25574  clwwlkf1  25580  clwwlkext2edg  25586  clwwisshclwwlem  25590  usg2cwwkdifex  25605  extwwlkfablem2  25862  numclwwlkovf2ex  25870  numclwlk1lem2f1  25878  numclwwlk7  25898  frgrareggt1  25900  frgraregord013  25902  frgraogt3nreg  25904  smcnlem  26389  nmoub3i  26470  blocnilem  26501  ubthlem2  26569  minvecolem4  26578  minvecolem4OLD  26588  htthlem  26626  nmcexi  27735  nmopcoi  27804  cdj1i  28142  nn0sqeq1  28376  nndiffz1  28418  fzsplit3  28422  pmtrto1cl  28663  fzto1st1  28666  fzto1st  28667  psgnfzto1st  28669  1smat1  28681  submateqlem1  28684  madjusmdetlem2  28705  unitdivcld  28758  sqsscirc1  28765  nexple  28882  indf1o  28896  esumdivc  28955  dya2ub  29142  dya2iocress  29146  dya2iocbrsiga  29147  dya2icobrsiga  29148  dya2icoseg  29149  dya2iocucvr  29156  sxbrsigalem2  29158  fibp1  29284  probmeasb  29313  dstrvprob  29354  dstfrvunirn  29357  ballotlemfc0  29375  ballotlemfcc  29376  ballotlemsgt1  29393  ballotlemsel1i  29395  ballotlemfrcn0  29412  ballotlemsgt1OLD  29431  ballotlemsel1iOLD  29433  ballotlemfrcn0OLD  29450  signsply0  29490  subfaclim  29961  cvmliftlem2  30059  cvmliftlem13  30069  snmlff  30102  bccolsum  30425  faclim  30432  nn0prpwlem  31028  poimirlem6  31992  poimirlem7  31993  poimirlem15  32001  poimirlem19  32005  poimirlem29  32015  poimirlem30  32016  poimirlem31  32017  poimirlem32  32018  broucube  32020  itg2addnclem2  32040  itg2addnclem3  32041  areacirclem1  32078  areacirclem4  32081  incsequz  32123  totbndbnd  32167  bfplem2  32201  lzenom  35658  irrapxlem1  35712  irrapxlem2  35713  irrapxlem4  35715  irrapxlem5  35716  pellexlem2  35720  pell1qrge1  35762  pell1qr1  35763  elpell1qr2  35764  pell14qrgapw  35768  pellfundgt1  35777  pellfundglb  35779  pellfundex  35780  pellfundrp  35782  pellfundne1  35783  rmspecnonsq  35801  rmspecfund  35803  rmspecpos  35810  monotoddzzfi  35836  rmygeid  35860  areaquad  36147  imo72b2lem0  36654  imo72b2lem1  36660  imo72b2  36664  isprm7  36705  cvgdvgrat  36707  radcnvrat  36708  hashnzfzclim  36716  lhe4.4ex1a  36723  binomcxplemnn0  36743  binomcxplemdvbinom  36747  binomcxplemnotnn0  36750  oddfl  37562  abscosbd  37563  zltlesub  37570  abssinbd  37587  monoords  37589  fzisoeu  37593  fzdifsuc2  37605  suplesup  37637  xralrple2  37652  infxr  37666  infleinflem2  37670  fmul01  37744  fmul01lt1lem1  37748  fmul01lt1lem2  37749  climsuselem1  37772  sumnnodd  37796  0ellimcdiv  37816  dvmptidg  37873  dvcosax  37884  ioodvbdlimc1lem1  37889  ioodvbdlimc1lem2  37890  ioodvbdlimc1lem1OLD  37891  ioodvbdlimc1lem2OLD  37892  ioodvbdlimc2lem  37894  ioodvbdlimc2lemOLD  37895  dvxpaek  37901  dvnmul  37904  iblspltprt  37936  itgspltprt  37942  stoweidlem5  37966  stoweidlem7  37968  stoweidlem10  37971  stoweidlem11  37972  stoweidlem12  37973  stoweidlem13  37974  stoweidlem14  37975  stoweidlem16  37977  stoweidlem18  37979  stoweidlem20  37981  stoweidlem24  37985  stoweidlem25  37986  stoweidlem34  37996  stoweidlem36  37998  stoweidlem38  38000  stoweidlem40  38002  stoweidlem41  38003  stoweidlem42  38004  stoweidlem45  38007  stoweidlem51  38013  stoweidlem60  38022  wallispilem3  38030  wallispilem4  38031  wallispilem5  38032  wallispi  38033  wallispi2lem1  38034  wallispi2lem2  38035  wallispi2  38036  stirlinglem1  38037  stirlinglem3  38039  stirlinglem5  38041  stirlinglem6  38042  stirlinglem7  38043  stirlinglem8  38044  stirlinglem10  38046  stirlinglem11  38047  stirlinglem12  38048  stirlinglem13  38049  stirlinglem15  38051  dirker2re  38055  dirkerval2  38057  dirkerre  38058  dirkertrigeqlem1  38061  dirkertrigeqlem3  38063  dirkeritg  38065  dirkercncflem1  38066  dirkercncflem2  38067  dirkercncflem4  38069  fourierdlem5  38075  fourierdlem6  38076  fourierdlem11  38081  fourierdlem15  38085  fourierdlem19  38089  fourierdlem20  38090  fourierdlem24  38094  fourierdlem26  38096  fourierdlem28  38098  fourierdlem30  38100  fourierdlem39  38110  fourierdlem41  38112  fourierdlem43  38115  fourierdlem47  38118  fourierdlem48  38119  fourierdlem56  38127  fourierdlem60  38131  fourierdlem61  38132  fourierdlem62  38133  fourierdlem64  38135  fourierdlem65  38136  fourierdlem66  38137  fourierdlem68  38139  fourierdlem73  38144  fourierdlem78  38149  fourierdlem79  38150  fourierdlem87  38158  fourierdlem103  38174  fourierdlem104  38175  sqwvfoura  38193  fouriersw  38196  etransclem4  38204  etransclem23  38223  etransclem24  38224  etransclem31  38231  etransclem32  38232  etransclem35  38235  etransclem41  38241  etransclem46  38246  etransclem48OLD  38248  etransclem48  38249  etransc  38250  nnfoctbdjlem  38398  iundjiun  38403  hoidmvlelem1  38524  hoidmvlelem2  38525  hoidmvlelem3  38526  hoidmvlelem4  38527  ovnhoilem1  38530  sigaradd  38610  m1mod0mod1  38858  mod2eq1n2dvds  38860  iccpartiltu  38871  iccpartlt  38873  iccpartgt  38876  nnoALTV  38959  bgoldbtbndlem4  39038  proththdlem  39048  proththd  39049  pfx2  39090  p1lep2  39184  zm1nn  39187  nbusgrvtxm1  39599  upgrewlkle2  39769  pthdlem1  39888  cznnring  40327  nn0le2is012  40517  divge1b  40677  divgt1b  40678  m1modmmod  40693  difmodm1lt  40694  nn0o1gt2  40696  nno  40697  nn0eo  40704  regt1loggt0  40716  rege1logbrege0  40738  logblt1b  40744  fllog2  40748  nnolog2flm1  40770  dignn0flhalflem1  40795  reseccl  40842  recsccl  40843
  Copyright terms: Public domain W3C validator