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

Theorem 1red 9522
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 9506 . 2  |-  1  e.  RR
21a1i 11 1  |-  ( ph  ->  1  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1826   RRcr 9402   1c1 9404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-1cn 9461  ax-icn 9462  ax-addcl 9463  ax-mulcl 9465  ax-mulrcl 9466  ax-i2m1 9471  ax-1ne0 9472  ax-rrecex 9475  ax-cnre 9476
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-iota 5460  df-fv 5504  df-ov 6199
This theorem is referenced by:  recgt0  10303  ltrec  10342  nn0p1gt0  10742  nn0ge2m1nn  10778  suprzcl  10859  qbtwnre  11319  iccf1o  11585  xov1plusxeqvd  11587  fznatpl1  11656  elfz1b  11670  fzonn0p1p1  11793  elfzom1p1elfzo  11794  elfznelfzo  11814  elfznelfzob  11815  fladdz  11858  flhalf  11862  ltdifltdiv  11866  modltm1p1mod  11942  ltexp2a  12120  expcan  12121  ltexp2  12122  leexp2  12123  leexp2a  12124  leexp2r  12126  nnlesq  12174  bernneq3  12196  expnbnd  12197  expnlbnd2  12199  fzsdom2  12390  wrdlenge2n0  12485  swrd2lsw  12801  2swrd2eqwrdeq  12802  rddif  13175  reccn2  13421  rlimo1  13441  o1fsum  13629  abscvgcvg  13635  climcndslem1  13663  flo1  13668  harmonic  13672  geomulcvg  13687  fprodrecl  13762  efcllem  13815  efgt1  13853  tanhlt1  13897  sinltx  13926  eirrlem  13939  bitsfzolem  14086  bitsfzo  14087  bitsmod  14088  bitscmp  14090  bitsinv1lem  14093  smuval2  14134  prmind2  14230  isprm5  14255  divdenle  14284  zsqrtelqelz  14293  fermltl  14316  odzdvds  14324  modprm0  14332  iserodd  14361  pcfaclem  14419  prmreclem1  14436  4sqlem11  14475  4sqlem12  14476  ramub1lem1  14546  2expltfac  14579  pgpfaclem2  17246  znidomb  18691  chfacfisf  19440  chfacfisfcpmat  19441  chfacfscmulgsum  19446  chfacfpmmulgsum  19450  nrginvrcnlem  21284  nmoid  21334  xrsmopn  21402  metnrmlem1a  21447  iccpnfhmeo  21530  htpycc  21565  pcohtpylem  21604  pcoass  21609  pcorevlem  21611  nmhmcn  21688  cncmet  21846  ovoliunlem1  21998  dyadmaxlem  22091  vitalilem2  22103  mbfi1fseqlem6  22212  itg2mulc  22239  itg2monolem1  22242  itg2monolem3  22244  dveflem  22465  mvth  22478  dvlipcn  22480  lhop1lem  22499  dvfsumlem1  22512  dvfsumlem2  22513  dvfsumlem3  22514  dvfsumlem4  22515  dvfsum2  22520  fta1glem2  22652  plyeq0lem  22692  fta1lem  22788  vieta1lem2  22792  aalioulem3  22815  aalioulem4  22816  radcnvlem1  22893  radcnvlem2  22894  dvradcnv  22901  abelthlem2  22912  abelthlem5  22915  abelthlem7  22918  abelth2  22922  cosne0  23002  rplogcl  23076  logdivlti  23092  logno1  23104  advlog  23122  logtayllem  23127  cxplt  23162  cxple  23163  cxpaddlelem  23212  cxpaddle  23213  relogbf  23249  isosctrlem1  23268  isosctrlem2  23269  heron  23285  atanlogaddlem  23360  bndatandm  23376  leibpi  23389  log2tlbnd  23392  birthdaylem3  23400  rlimcnp  23412  rlimcnp2  23413  efrlim  23416  cxp2limlem  23422  divsqrtsumo1  23430  jensenlem2  23434  logdiflbnd  23441  fsumharmonic  23458  wilthlem2  23460  ftalem2  23464  basellem9  23479  vma1  23557  ppieq0  23567  mumullem2  23571  fsumfldivdiaglem  23582  chpeq0  23600  chtub  23604  chpval2  23610  chpchtsum  23611  chpub  23612  logfacrlim  23616  logexprlim  23617  mersenne  23619  dchrelbas4  23635  bcmono  23669  bposlem1  23676  bposlem2  23677  lgslem3  23690  lgslem4  23691  lgsmod  23713  lgsdir2lem4  23718  lgsdirprm  23721  lgsquadlem2  23747  2sqlem8  23764  chebbnd1lem1  23771  chebbnd1lem2  23772  chtppilimlem1  23775  chebbnd2  23779  chto1lb  23780  chpchtlim  23781  chpo1ubb  23783  vmadivsum  23784  rplogsumlem1  23786  rpvmasumlem  23789  dchrisumlem3  23793  dchrmusumlema  23795  dchrmusum2  23796  dchrvmasumlem2  23800  dchrvmasumlem3  23801  dchrvmasumiflem1  23803  dchrvmasumiflem2  23804  dchrisum0flblem1  23810  dchrisum0fno1  23813  dchrisum0re  23815  dchrisum0lema  23816  dchrisum0lem1b  23817  dchrisum0lem2a  23819  dchrisum0lem2  23820  dchrisum0lem3  23821  rplogsum  23829  dirith2  23830  mudivsum  23832  mulogsumlem  23833  mulogsum  23834  mulog2sumlem1  23836  mulog2sumlem2  23837  vmalogdivsum2  23840  vmalogdivsum  23841  2vmadivsumlem  23842  log2sumbnd  23846  selberglem2  23848  selberg2lem  23852  chpdifbnd  23857  selberg3lem1  23859  selberg3  23861  selberg4lem1  23862  selberg4  23863  pntrmax  23866  pntrsumo1  23867  pntrsumbnd  23868  selberg3r  23871  selberg4r  23872  selberg34r  23873  pntrlog2bndlem1  23879  pntrlog2bndlem2  23880  pntrlog2bndlem3  23881  pntrlog2bndlem4  23882  pntrlog2bndlem5  23883  pntrlog2bndlem6  23885  pntrlog2bnd  23886  pntpbnd1  23888  pntibndlem2a  23892  pntibndlem2  23893  pntibnd  23895  pntlemc  23897  pntlemg  23900  pntlemr  23904  pntlemk  23908  qabvle  23927  ostth2lem3  23937  ostth2  23939  trgcgrg  24026  ttgcontlem1  24309  axpaschlem  24364  axlowdimlem16  24381  axcontlem2  24389  axcontlem7  24394  wwlkm1edg  24856  wwlkextproplem1  24862  wwlkextproplem2  24863  clwlkisclwwlklem2fv1  24903  clwlkisclwwlklem2fv2  24904  clwlkisclwwlklem1  24908  clwlkisclwwlk2  24911  clwwlkf1  24917  clwwlkext2edg  24923  clwwisshclwwlem  24927  usg2cwwkdifex  24942  extwwlkfablem2  25199  numclwwlkovf2ex  25207  numclwlk1lem2f1  25215  numclwwlk7  25235  frgrareggt1  25237  frgraregord013  25239  frgraogt3nreg  25241  smcnlem  25724  nmoub3i  25805  blocnilem  25836  ubthlem2  25904  minvecolem4  25913  htthlem  25951  nmcexi  27061  nmopcoi  27130  cdj1i  27468  nn0sqeq1  27712  nndiffz1  27749  fzsplit3  27752  unitdivcld  28037  sqsscirc1  28044  nexple  28158  indf1o  28172  esumdivc  28231  dya2ub  28397  dya2iocress  28401  dya2iocbrsiga  28402  dya2icobrsiga  28403  dya2icoseg  28404  dya2iocucvr  28411  sxbrsigalem2  28413  fibp1  28523  probmeasb  28552  dstrvprob  28593  dstfrvunirn  28596  ballotlemfc0  28614  ballotlemfcc  28615  ballotlemsgt1  28632  ballotlemsel1i  28634  ballotlemfrcn0  28651  signsply0  28691  lgamgulmlem2  28761  lgamgulmlem3  28762  lgamgulmlem4  28763  lgamgulmlem5  28764  lgamgulmlem6  28765  lgamcvg2  28786  regamcl  28792  subfaclim  28821  cvmliftlem2  28920  cvmliftlem13  28930  snmlff  28963  faclim  29337  bpoly4  29974  itg2addnclem2  30233  itg2addnclem3  30234  areacirclem1  30273  areacirclem4  30276  nn0prpwlem  30306  incsequz  30407  totbndbnd  30451  bfplem2  30485  lzenom  30868  irrapxlem1  30923  irrapxlem2  30924  irrapxlem4  30926  irrapxlem5  30927  pellexlem2  30931  pell1qrge1  30971  pell1qr1  30972  elpell1qr2  30973  pell14qrgapw  30977  pellfundgt1  30984  pellfundglb  30986  pellfundex  30987  pellfundrp  30989  pellfundne1  30990  rmspecnonsq  31008  rmspecfund  31010  rmspecpos  31017  monotoddzzfi  31043  rmygeid  31067  areaquad  31352  isprm7  31360  cvgdvgrat  31362  radcnvrat  31363  hashnzfzclim  31395  lhe4.4ex1a  31402  binomcxplemnn0  31422  binomcxplemdvbinom  31426  binomcxplemnotnn0  31429  oddfl  31626  abscosbd  31627  zltlesub  31635  abssinbd  31656  monoords  31662  fzisoeu  31666  fzdifsuc2  31678  fmul01  31740  fmul01lt1lem1  31744  fmul01lt1lem2  31745  fprodle  31770  climsuselem1  31779  sumnnodd  31802  0ellimcdiv  31821  dvmptidg  31878  dvcosax  31889  ioodvbdlimc1lem1  31894  ioodvbdlimc1lem2  31895  ioodvbdlimc2lem  31897  dvxpaek  31903  dvnmul  31906  iblspltprt  31938  itgspltprt  31944  stoweidlem5  31953  stoweidlem7  31955  stoweidlem10  31958  stoweidlem11  31959  stoweidlem12  31960  stoweidlem13  31961  stoweidlem14  31962  stoweidlem16  31964  stoweidlem18  31966  stoweidlem20  31968  stoweidlem24  31972  stoweidlem25  31973  stoweidlem34  31982  stoweidlem36  31984  stoweidlem38  31986  stoweidlem40  31988  stoweidlem41  31989  stoweidlem42  31990  stoweidlem45  31993  stoweidlem51  31999  stoweidlem60  32008  wallispilem3  32015  wallispilem4  32016  wallispilem5  32017  wallispi  32018  wallispi2lem1  32019  wallispi2lem2  32020  wallispi2  32021  stirlinglem1  32022  stirlinglem3  32024  stirlinglem5  32026  stirlinglem6  32027  stirlinglem7  32028  stirlinglem8  32029  stirlinglem10  32031  stirlinglem11  32032  stirlinglem12  32033  stirlinglem13  32034  stirlinglem15  32036  dirker2re  32040  dirkerval2  32042  dirkerre  32043  dirkertrigeqlem1  32046  dirkertrigeqlem3  32048  dirkeritg  32050  dirkercncflem1  32051  dirkercncflem2  32052  dirkercncflem4  32054  fourierdlem5  32060  fourierdlem6  32061  fourierdlem11  32066  fourierdlem15  32070  fourierdlem19  32074  fourierdlem20  32075  fourierdlem24  32079  fourierdlem26  32081  fourierdlem28  32083  fourierdlem30  32085  fourierdlem39  32094  fourierdlem41  32096  fourierdlem43  32098  fourierdlem47  32102  fourierdlem48  32103  fourierdlem56  32111  fourierdlem60  32115  fourierdlem61  32116  fourierdlem62  32117  fourierdlem64  32119  fourierdlem65  32120  fourierdlem66  32121  fourierdlem68  32123  fourierdlem73  32128  fourierdlem78  32133  fourierdlem79  32134  fourierdlem87  32142  fourierdlem103  32158  fourierdlem104  32159  sqwvfoura  32177  fouriersw  32180  etransclem4  32187  etransclem23  32206  etransclem24  32207  etransclem31  32214  etransclem32  32215  etransclem35  32218  etransclem41  32224  etransclem46  32229  etransclem48  32231  etransc  32232  sigaradd  32249  m1mod0mod1  32460  mod2eq1n2dvds  32462  nnoALTV  32537  proththdlem  32547  proththd  32548  pfx2  32587  p1lep2  32643  zm1nn  32646  cznnring  32964  nn0le2is012  33156  divge1b  33316  divgt1b  33317  m1modmmod  33334  difmodm1lt  33335  nn0o1gt2  33337  nno  33338  nn0eo  33345  regt1loggt0  33357  rege1logbrege0  33379  logblt1b  33385  fllog2  33389  nnolog2flm1  33411  dignn0flhalflem1  33436  reseccl  33483  recsccl  33484  imo72b2lem0  38511  imo72b2lem1  38517  imo72b2  38522
  Copyright terms: Public domain W3C validator