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

Theorem 1red 9614
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 9598 . 2  |-  1  e.  RR
21a1i 11 1  |-  ( ph  ->  1  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804   RRcr 9494   1c1 9496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-1cn 9553  ax-icn 9554  ax-addcl 9555  ax-mulcl 9557  ax-mulrcl 9558  ax-i2m1 9563  ax-1ne0 9564  ax-rrecex 9567  ax-cnre 9568
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284
This theorem is referenced by:  recgt0  10392  ltrec  10432  nn0p1gt0  10831  nn0ge2m1nn  10867  suprzcl  10948  qbtwnre  11407  iccf1o  11673  xov1plusxeqvd  11675  fznatpl1  11743  elfz1b  11757  fzonn0p1p1  11873  elfzom1p1elfzo  11874  elfznelfzo  11894  elfznelfzob  11895  fladdz  11937  flhalf  11941  ltdifltdiv  11945  modltm1p1mod  12018  ltexp2a  12196  expcan  12197  ltexp2  12198  leexp2  12199  leexp2a  12200  leexp2r  12202  nnlesq  12250  bernneq3  12273  expnbnd  12274  expnlbnd2  12276  fzsdom2  12465  wrdlenge2n0  12556  lswccatn0lsw  12586  swrdn0  12634  swrd2lsw  12869  2swrd2eqwrdeq  12870  rddif  13152  reccn2  13398  rlimo1  13418  o1fsum  13606  abscvgcvg  13612  climcndslem1  13640  flo1  13645  harmonic  13649  geomulcvg  13664  efcllem  13691  efgt1  13728  tanhlt1  13772  sinltx  13801  eirrlem  13814  bitsfzolem  13961  bitsfzo  13962  bitsmod  13963  bitscmp  13965  bitsinv1lem  13968  smuval2  14009  prmind2  14105  isprm5  14130  divdenle  14159  zsqrtelqelz  14168  fermltl  14191  odzdvds  14199  modprm0  14207  iserodd  14236  pcfaclem  14294  prmreclem1  14311  4sqlem11  14350  4sqlem12  14351  ramub1lem1  14421  2expltfac  14454  pgpfaclem2  17007  znidomb  18473  chfacfisf  19228  chfacfisfcpmat  19229  chfacfscmulgsum  19234  chfacfpmmulgsum  19238  nrginvrcnlem  21072  nmoid  21122  xrsmopn  21190  metnrmlem1a  21235  iccpnfhmeo  21318  htpycc  21353  pcohtpylem  21392  pcoass  21397  pcorevlem  21399  nmhmcn  21476  cncmet  21634  ovoliunlem1  21786  dyadmaxlem  21879  vitalilem2  21891  mbfi1fseqlem6  22000  itg2mulc  22027  itg2monolem1  22030  itg2monolem3  22032  dveflem  22253  mvth  22266  dvlipcn  22268  lhop1lem  22287  dvfsumlem1  22300  dvfsumlem2  22301  dvfsumlem3  22302  dvfsumlem4  22303  dvfsum2  22308  fta1glem2  22440  plyeq0lem  22480  fta1lem  22575  vieta1lem2  22579  aalioulem3  22602  aalioulem4  22603  radcnvlem1  22680  radcnvlem2  22681  dvradcnv  22688  abelthlem2  22699  abelthlem5  22702  abelthlem7  22705  abelth2  22709  cosne0  22789  rplogcl  22861  logdivlti  22877  logno1  22889  advlog  22907  logtayllem  22912  cxplt  22947  cxple  22948  cxpaddlelem  22997  cxpaddle  22998  isosctrlem1  23024  isosctrlem2  23025  heron  23041  atanlogaddlem  23116  bndatandm  23132  leibpi  23145  log2tlbnd  23148  birthdaylem3  23155  rlimcnp  23167  rlimcnp2  23168  efrlim  23171  cxp2limlem  23177  divsqrtsumo1  23185  jensenlem2  23189  logdiflbnd  23196  fsumharmonic  23213  wilthlem2  23215  ftalem2  23219  basellem9  23234  vma1  23312  ppieq0  23322  mumullem2  23326  fsumfldivdiaglem  23337  chpeq0  23355  chtub  23359  chpval2  23365  chpchtsum  23366  chpub  23367  logfacrlim  23371  logexprlim  23372  mersenne  23374  dchrelbas4  23390  bcmono  23424  bposlem1  23431  bposlem2  23432  lgslem3  23445  lgslem4  23446  lgsmod  23468  lgsdir2lem4  23473  lgsdirprm  23476  lgsquadlem2  23502  2sqlem8  23519  chebbnd1lem1  23526  chebbnd1lem2  23527  chtppilimlem1  23530  chebbnd2  23534  chto1lb  23535  chpchtlim  23536  chpo1ubb  23538  vmadivsum  23539  rplogsumlem1  23541  rpvmasumlem  23544  dchrisumlem3  23548  dchrmusumlema  23550  dchrmusum2  23551  dchrvmasumlem2  23555  dchrvmasumlem3  23556  dchrvmasumiflem1  23558  dchrvmasumiflem2  23559  dchrisum0flblem1  23565  dchrisum0fno1  23568  dchrisum0re  23570  dchrisum0lema  23571  dchrisum0lem1b  23572  dchrisum0lem2a  23574  dchrisum0lem2  23575  dchrisum0lem3  23576  rplogsum  23584  dirith2  23585  mudivsum  23587  mulogsumlem  23588  mulogsum  23589  mulog2sumlem1  23591  mulog2sumlem2  23592  vmalogdivsum2  23595  vmalogdivsum  23596  2vmadivsumlem  23597  log2sumbnd  23601  selberglem2  23603  selberg2lem  23607  chpdifbnd  23612  selberg3lem1  23614  selberg3  23616  selberg4lem1  23617  selberg4  23618  pntrmax  23621  pntrsumo1  23622  pntrsumbnd  23623  selberg3r  23626  selberg4r  23627  selberg34r  23628  pntrlog2bndlem1  23634  pntrlog2bndlem2  23635  pntrlog2bndlem3  23636  pntrlog2bndlem4  23637  pntrlog2bndlem5  23638  pntrlog2bndlem6  23640  pntrlog2bnd  23641  pntpbnd1  23643  pntibndlem2a  23647  pntibndlem2  23648  pntibnd  23650  pntlemc  23652  pntlemg  23655  pntlemr  23659  pntlemk  23663  qabvle  23682  ostth2lem3  23692  ostth2  23694  trgcgrg  23778  ttgcontlem1  24060  axpaschlem  24115  axlowdimlem16  24132  axcontlem2  24140  axcontlem7  24145  wwlkm1edg  24607  wwlkextproplem1  24613  wwlkextproplem2  24614  clwlkisclwwlklem2fv1  24654  clwlkisclwwlklem2fv2  24655  clwlkisclwwlklem1  24659  clwlkisclwwlk2  24662  clwwlkf1  24668  clwwlkext2edg  24674  clwwisshclwwlem  24678  usg2cwwkdifex  24693  extwwlkfablem2  24950  numclwwlkovf2ex  24958  numclwlk1lem2f1  24966  numclwwlk7  24986  frgrareggt1  24988  frgraregord013  24990  frgraogt3nreg  24992  smcnlem  25479  nmoub3i  25560  blocnilem  25591  ubthlem2  25659  minvecolem4  25668  htthlem  25706  nmcexi  26817  nmopcoi  26886  cdj1i  27224  nn0sqeq1  27434  nndiffz1  27468  fzsplit3  27471  unitdivcld  27756  sqsscirc1  27763  nexple  27878  indf1o  27910  esumdivc  27962  dya2ub  28114  dya2iocress  28118  dya2iocbrsiga  28119  dya2icobrsiga  28120  dya2icoseg  28121  dya2iocucvr  28128  sxbrsigalem2  28130  fibp1  28213  probmeasb  28242  dstrvprob  28283  dstfrvunirn  28286  ballotlemfc0  28304  ballotlemfcc  28305  ballotlemsgt1  28322  ballotlemsel1i  28324  ballotlemfrcn0  28341  signsply0  28381  lgamgulmlem2  28445  lgamgulmlem3  28446  lgamgulmlem4  28447  lgamgulmlem5  28448  lgamgulmlem6  28449  lgamcvg2  28470  regamcl  28476  subfaclim  28505  cvmliftlem2  28604  cvmliftlem13  28614  snmlff  28647  fprodrecl  29060  faclim  29146  bpoly4  29796  itg2addnclem2  30042  itg2addnclem3  30043  areacirclem1  30082  areacirclem4  30085  nn0prpwlem  30115  incsequz  30216  totbndbnd  30260  bfplem2  30294  lzenom  30678  irrapxlem1  30733  irrapxlem2  30734  irrapxlem4  30736  irrapxlem5  30737  pellexlem2  30741  pell1qrge1  30781  pell1qr1  30782  elpell1qr2  30783  pell14qrgapw  30787  pellfundgt1  30794  pellfundglb  30796  pellfundex  30797  pellfundrp  30799  pellfundne1  30800  rmspecnonsq  30818  rmspecfund  30820  rmspecpos  30827  monotoddzzfi  30853  rmygeid  30877  areaquad  31160  isprm7  31168  cvgdvgrat  31170  radcnvrat  31171  hashnzfzclim  31203  lhe4.4ex1a  31210  oddfl  31408  abscosbd  31409  zltlesub  31417  abssinbd  31439  monoords  31445  fzisoeu  31449  fmul01  31502  fmul01lt1lem1  31506  fmul01lt1lem2  31507  climsuselem1  31521  sumnnodd  31544  0ellimcdiv  31563  dvmptidg  31616  dvcosax  31627  ioodvbdlimc1lem1  31632  ioodvbdlimc1lem2  31633  ioodvbdlimc2lem  31635  iblspltprt  31662  itgspltprt  31668  stoweidlem5  31676  stoweidlem7  31678  stoweidlem10  31681  stoweidlem11  31682  stoweidlem12  31683  stoweidlem13  31684  stoweidlem14  31685  stoweidlem16  31687  stoweidlem18  31689  stoweidlem20  31691  stoweidlem24  31695  stoweidlem25  31696  stoweidlem34  31705  stoweidlem36  31707  stoweidlem38  31709  stoweidlem40  31711  stoweidlem41  31712  stoweidlem42  31713  stoweidlem45  31716  stoweidlem51  31722  stoweidlem60  31731  wallispilem3  31738  wallispilem4  31739  wallispilem5  31740  wallispi  31741  wallispi2lem1  31742  wallispi2lem2  31743  wallispi2  31744  stirlinglem1  31745  stirlinglem3  31747  stirlinglem5  31749  stirlinglem6  31750  stirlinglem7  31751  stirlinglem8  31752  stirlinglem10  31754  stirlinglem11  31755  stirlinglem12  31756  stirlinglem13  31757  stirlinglem15  31759  dirker2re  31763  dirkerval2  31765  dirkerre  31766  dirkertrigeqlem1  31769  dirkertrigeqlem3  31771  dirkeritg  31773  dirkercncflem1  31774  dirkercncflem2  31775  dirkercncflem4  31777  fourierdlem5  31783  fourierdlem6  31784  fourierdlem11  31789  fourierdlem15  31793  fourierdlem19  31797  fourierdlem20  31798  fourierdlem24  31802  fourierdlem26  31804  fourierdlem28  31806  fourierdlem30  31808  fourierdlem39  31817  fourierdlem41  31819  fourierdlem43  31821  fourierdlem47  31825  fourierdlem48  31826  fourierdlem56  31834  fourierdlem60  31838  fourierdlem61  31839  fourierdlem62  31840  fourierdlem64  31842  fourierdlem65  31843  fourierdlem66  31844  fourierdlem68  31846  fourierdlem73  31851  fourierdlem78  31856  fourierdlem79  31857  fourierdlem87  31865  fourierdlem103  31881  fourierdlem104  31882  sqwvfoura  31900  fouriersw  31903  sigaradd  31921  p1lep2  32160  zm1nn  32163  cznnring  32471  nn0le2is012  32684  reseccl  32877  recsccl  32878  imo72b2lem0  37645  imo72b2lem1  37651  imo72b2  37656
  Copyright terms: Public domain W3C validator