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

Theorem 1red 10636
Description: The number 1 is real, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
1red (𝜑 → 1 ∈ ℝ)

Proof of Theorem 1red
StepHypRef Expression
1 1re 10635 . 2 1 ∈ ℝ
21a1i 11 1 (𝜑 → 1 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cr 10530  1c1 10532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-mulcl 10593  ax-mulrcl 10594  ax-i2m1 10599  ax-1ne0 10600  ax-rrecex 10603  ax-cnre 10604
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-iota 6313  df-fv 6362  df-ov 7153
This theorem is referenced by:  recgt0  11480  ltrec  11516  nnne0  11665  nn0p1gt0  11920  nn0ge2m1nn  11958  nn0le2is012  12040  suprzcl  12056  ledivge1le  12455  qbtwnre  12587  lincmb01cmp  12876  iccf1o  12877  xov1plusxeqvd  12879  zltaddlt1le  12885  fznatpl1  12956  elfz1b  12971  fzonn0p1p1  13111  elfznelfzo  13137  elfznelfzob  13138  fladdz  13190  2tnp1ge0ge0  13194  flhalf  13195  ltdifltdiv  13199  fldiv4lem1div2uz2  13201  mulp1mod1  13275  m1modge3gt1  13281  modltm1p1mod  13286  addmodlteq  13309  ltexp2a  13525  expcan  13528  ltexp2  13529  leexp2  13530  leexp2a  13531  leexp2r  13533  nnlesq  13563  bernneq3  13587  expnbnd  13588  expnlbnd2  13590  expnngt1  13597  fzsdom2  13784  wrdlenge2n0  13899  swrd2lsw  14309  2swrd2eqwrdeq  14310  sqrlem7  14603  rddif  14695  reccn2  14948  rlimo1  14968  o1fsum  15163  abscvgcvg  15169  climcndslem1  15199  flo1  15204  harmonic  15209  geomulcvg  15227  fprodrecl  15302  fprodreclf  15308  fprodle  15345  bpoly4  15408  efcllem  15426  efgt1  15464  tanhlt1  15508  sinltx  15537  eirrlem  15552  p1modz1  15609  mod2eq1n2dvds  15691  oddge22np1  15693  ltoddhalfle  15705  nn0o1gt2  15727  nno  15728  nn0oddm1d2  15731  nnoddm1d2  15732  bitsfzolem  15778  bitsfzo  15779  bitsmod  15780  bitscmp  15782  bitsinv1lem  15785  smuval2  15826  coprmgcdb  15988  prmind2  16024  dvdsnprmd  16029  2mulprm  16032  isprm5  16046  isprm7  16047  divdenle  16084  zsqrtelqelz  16093  fermltl  16116  odzdvds  16127  modprm0  16137  iserodd  16167  difsqpwdvds  16218  pcfaclem  16229  prmreclem1  16247  4sqlem11  16286  4sqlem12  16287  ramub1lem1  16357  prmgaplem8  16389  2expltfac  16421  pgpfaclem2  19140  znidomb  20643  chfacfisf  21397  chfacfisfcpmat  21398  chfacfscmulgsum  21403  chfacfpmmulgsum  21407  nrginvrcnlem  23234  nmoid  23285  xrsmopn  23354  metnrmlem1a  23400  iccpnfhmeo  23483  lebnumii  23504  htpycc  23518  pcohtpylem  23557  pcoass  23562  pcorevlem  23564  nmhmcn  23658  cncmet  23859  ovoliunlem1  24037  dyadmaxlem  24132  vitalilem2  24144  mbfi1fseqlem6  24255  itg2mulc  24282  itg2monolem1  24285  itg2monolem3  24287  dveflem  24510  mvth  24523  dvlipcn  24525  lhop1lem  24544  dvfsumlem1  24557  dvfsumlem2  24558  dvfsumlem3  24559  dvfsumlem4  24560  dvfsum2  24565  fta1glem2  24694  plyeq0lem  24734  fta1lem  24830  vieta1lem2  24834  aalioulem3  24857  aalioulem4  24858  radcnvlem1  24935  radcnvlem2  24936  dvradcnv  24943  abelthlem2  24954  abelthlem5  24957  abelthlem7  24960  abelth2  24964  cosne0  25046  rplogcl  25119  logdivlti  25135  logno1  25151  dvlog2lem  25167  advlog  25169  logtayllem  25174  cxplt  25209  cxple  25210  cxpaddlelem  25264  cxpaddle  25265  relogbf  25301  logbgt0b  25303  isosctrlem1  25328  isosctrlem2  25329  chordthmlem4  25345  heron  25348  atanlogaddlem  25423  bndatandm  25439  leibpi  25453  log2tlbnd  25456  birthdaylem3  25464  rlimcnp  25476  rlimcnp2  25477  efrlim  25480  cxp2limlem  25486  cxp2lim  25487  divsqrtsumo1  25494  jensenlem2  25498  logdiflbnd  25505  fsumharmonic  25522  lgamgulmlem2  25540  lgamgulmlem3  25541  lgamgulmlem4  25542  lgamgulmlem5  25543  lgamgulmlem6  25544  lgamcvg2  25565  regamcl  25571  wilthlem2  25579  ftalem2  25584  basellem9  25599  vma1  25676  ppieq0  25686  mumullem2  25690  fsumfldivdiaglem  25699  chpeq0  25717  chtub  25721  chpval2  25727  chpchtsum  25728  chpub  25729  logfacrlim  25733  logexprlim  25734  mersenne  25736  perfectlem2  25739  dchrelbas4  25752  bcmono  25786  bposlem1  25793  bposlem2  25794  zabsle1  25805  lgslem3  25808  lgsmod  25832  lgsdir2lem4  25837  lgsdirprm  25840  gausslemma2dlem1a  25874  gausslemma2d  25883  lgsquadlem2  25890  2sqlem8  25935  chebbnd1lem1  25978  chebbnd1lem2  25979  chtppilimlem1  25982  chebbnd2  25986  chto1lb  25987  chpchtlim  25988  chpo1ubb  25990  vmadivsum  25991  rplogsumlem1  25993  rpvmasumlem  25996  dchrisumlem3  26000  dchrmusumlema  26002  dchrmusum2  26003  dchrvmasumlem2  26007  dchrvmasumlem3  26008  dchrvmasumiflem1  26010  dchrvmasumiflem2  26011  dchrisum0flblem1  26017  dchrisum0flblem2  26018  dchrisum0fno1  26020  dchrisum0re  26022  dchrisum0lema  26023  dchrisum0lem1b  26024  dchrisum0lem2a  26026  dchrisum0lem2  26027  dchrisum0lem3  26028  rplogsum  26036  dirith2  26037  mudivsum  26039  mulogsumlem  26040  mulogsum  26041  mulog2sumlem1  26043  mulog2sumlem2  26044  vmalogdivsum2  26047  vmalogdivsum  26048  2vmadivsumlem  26049  log2sumbnd  26053  selberglem2  26055  selberg2lem  26059  chpdifbnd  26064  selberg3lem1  26066  selberg3  26068  selberg4lem1  26069  selberg4  26070  pntrmax  26073  pntrsumo1  26074  pntrsumbnd  26075  selberg3r  26078  selberg4r  26079  selberg34r  26080  pntrlog2bndlem1  26086  pntrlog2bndlem2  26087  pntrlog2bndlem3  26088  pntrlog2bndlem4  26089  pntrlog2bndlem5  26090  pntrlog2bndlem6  26092  pntrlog2bnd  26093  pntpbnd1a  26094  pntpbnd1  26095  pntibndlem2a  26099  pntibndlem2  26100  pntibnd  26102  pntlemc  26104  pntlemg  26107  pntlemr  26111  pntlemk  26115  pnt  26123  qabvle  26134  ostth2lem3  26144  ostth2  26146  trgcgrg  26234  tgcgr4  26250  ttgcontlem1  26604  axpaschlem  26659  axlowdimlem16  26676  axcontlem2  26684  axcontlem7  26689  nbusgrvtxm1  27094  upgrewlkle2  27321  pthdlem1  27480  crctcshwlkn0lem3  27523  crctcshwlkn0lem5  27525  wwlksm1edg  27592  wwlksnextproplem2  27622  clwlkclwwlklem2fv1  27706  clwlkclwwlklem2fv2  27707  clwlkclwwlklem2  27711  clwlkclwwlk2  27714  clwwisshclwwslem  27725  clwwlkf1  27761  clwwlkext2edg  27768  clwlknf1oclwwlknlem1  27793  clwwlknonex2lem2  27820  numclwwlk7  28103  frgrreggt1  28105  frgrogt3nreg  28109  smcnlem  28407  nmoub3i  28483  blocnilem  28514  ubthlem2  28581  minvecolem4  28590  htthlem  28627  nmcexi  29736  nmopcoi  29805  stadd3i  29958  cdj1i  30143  nnmulge  30406  nndiffz1  30441  fzsplit3  30449  wrdt2ind  30560  pmtrto1cl  30674  fzto1st1  30677  fzto1st  30678  psgnfzto1st  30680  cycpmco2lem6  30706  cycpmco2lem7  30707  cycpmrn  30718  qsidomlem1  30888  1smat1  30974  submateqlem1  30977  madjusmdetlem2  30998  unitdivcld  31049  sqsscirc1  31056  nexple  31173  indf1o  31188  esumdivc  31247  dya2ub  31433  dya2iocress  31437  dya2iocbrsiga  31438  dya2icobrsiga  31439  dya2icoseg  31440  dya2iocucvr  31447  sxbrsigalem2  31449  fibp1  31564  probmeasb  31593  dstrvprob  31634  dstfrvunirn  31637  ballotlemfc0  31655  ballotlemfcc  31656  ballotlemsgt1  31673  ballotlemsel1i  31675  ballotlemfrcn0  31692  signsply0  31726  itgexpif  31782  reprlt  31795  chtvalz  31805  breprexplemc  31808  breprexp  31809  circlemeth  31816  tgoldbachgnn  31835  acycgr1v  32299  subfaclim  32338  cvmliftlem2  32436  cvmliftlem13  32446  snmlff  32479  bccolsum  32874  faclim  32881  nn0prpwlem  33573  dnibndlem10  33729  dnibndlem12  33731  knoppcnlem4  33738  unblimceq0  33749  knoppndvlem1  33754  knoppndvlem2  33755  knoppndvlem3  33756  knoppndvlem7  33760  knoppndvlem11  33764  knoppndvlem12  33765  knoppndvlem14  33767  knoppndvlem15  33768  knoppndvlem17  33770  knoppndvlem18  33771  knoppndvlem20  33773  poimirlem6  34784  poimirlem7  34785  poimirlem15  34793  poimirlem19  34797  poimirlem29  34807  poimirlem30  34808  poimirlem31  34809  poimirlem32  34810  broucube  34812  itg2addnclem2  34830  itg2addnclem3  34831  areacirclem1  34868  areacirclem4  34871  incsequz  34910  totbndbnd  34954  bfplem2  34988  sn-1ne2  39042  rtprmirr  39078  sn-00idlem2  39113  sn-0ne2  39120  fltnlta  39159  3cubeslem1  39165  3cubeslem3r  39168  3cubeslem4  39170  lzenom  39251  irrapxlem1  39303  irrapxlem2  39304  irrapxlem4  39306  irrapxlem5  39307  pellexlem2  39311  pell1qrge1  39351  pell1qr1  39352  elpell1qr2  39353  pell14qrgapw  39357  pellfundgt1  39364  pellfundglb  39366  pellfundex  39367  pellfundrp  39369  pellfundne1  39370  rmspecsqrtnq  39387  rmspecnonsq  39388  rmspecfund  39390  rmspecpos  39397  monotoddzzfi  39423  rmygeid  39445  areaquad  39707  imo72b2lem0  40400  imo72b2lem1  40406  imo72b2  40410  cvgdvgrat  40529  radcnvrat  40530  hashnzfzclim  40538  lhe4.4ex1a  40545  binomcxplemnn0  40565  binomcxplemdvbinom  40569  binomcxplemnotnn0  40572  oddfl  41427  abscosbd  41428  zltlesub  41435  abssinbd  41446  monoords  41448  fzisoeu  41451  fzdifsuc2  41461  suplesup  41491  xralrple2  41506  infxr  41519  infleinflem2  41523  reclt0d  41542  xrralrecnnge  41546  sqrlearg  41713  iooiinioc  41716  fmul01  41745  fmul01lt1lem1  41749  fmul01lt1lem2  41750  climsuselem1  41772  sumnnodd  41795  0ellimcdiv  41814  dvmptidg  42085  dvcosax  42095  ioodvbdlimc1lem1  42100  ioodvbdlimc1lem2  42101  ioodvbdlimc2lem  42103  dvxpaek  42109  dvnmul  42112  iblspltprt  42142  itgspltprt  42148  stoweidlem5  42175  stoweidlem7  42177  stoweidlem10  42180  stoweidlem11  42181  stoweidlem12  42182  stoweidlem13  42183  stoweidlem14  42184  stoweidlem16  42186  stoweidlem18  42188  stoweidlem20  42190  stoweidlem24  42194  stoweidlem25  42195  stoweidlem34  42204  stoweidlem36  42206  stoweidlem38  42208  stoweidlem40  42210  stoweidlem41  42211  stoweidlem42  42212  stoweidlem45  42215  stoweidlem51  42221  stoweidlem60  42230  wallispilem3  42237  wallispilem4  42238  wallispilem5  42239  wallispi  42240  wallispi2lem1  42241  wallispi2lem2  42242  wallispi2  42243  stirlinglem1  42244  stirlinglem3  42246  stirlinglem5  42248  stirlinglem6  42249  stirlinglem7  42250  stirlinglem8  42251  stirlinglem10  42253  stirlinglem11  42254  stirlinglem12  42255  stirlinglem13  42256  stirlinglem15  42258  dirker2re  42262  dirkerval2  42264  dirkerre  42265  dirkertrigeqlem1  42268  dirkertrigeqlem3  42270  dirkeritg  42272  dirkercncflem1  42273  dirkercncflem2  42274  dirkercncflem4  42276  fourierdlem5  42282  fourierdlem6  42283  fourierdlem11  42288  fourierdlem15  42292  fourierdlem19  42296  fourierdlem20  42297  fourierdlem24  42301  fourierdlem26  42303  fourierdlem28  42305  fourierdlem30  42307  fourierdlem39  42316  fourierdlem41  42318  fourierdlem43  42320  fourierdlem47  42323  fourierdlem48  42324  fourierdlem56  42332  fourierdlem60  42336  fourierdlem61  42337  fourierdlem62  42338  fourierdlem64  42340  fourierdlem65  42341  fourierdlem66  42342  fourierdlem68  42344  fourierdlem73  42349  fourierdlem78  42354  fourierdlem79  42355  fourierdlem87  42363  fourierdlem103  42379  fourierdlem104  42380  sqwvfoura  42398  fouriersw  42401  etransclem4  42408  etransclem23  42427  etransclem24  42428  etransclem31  42435  etransclem32  42436  etransclem35  42439  etransclem41  42445  etransclem46  42450  etransclem48  42452  etransc  42453  ioorrnopnxrlem  42476  nnfoctbdjlem  42622  iundjiun  42627  hoidmvlelem1  42762  hoidmvlelem2  42763  hoidmvlelem3  42764  hoidmvlelem4  42765  ovnhoilem1  42768  vonioolem2  42848  vonicclem2  42851  pimrecltneg  42886  smfrec  42949  smfmullem1  42951  smfmullem2  42952  smfdiv  42957  sigaradd  43008  p1lep2  43385  zm1nn  43387  m1mod0mod1  43414  iccpartiltu  43433  iccpartlt  43435  iccpartgt  43438  fmtnoge3  43543  fmtnodvds  43557  fmtnoprmfac2lem1  43579  2pwp1prm  43602  flsqrt  43607  sfprmdvdsmersenne  43619  lighneallem2  43622  lighneallem4a  43624  proththdlem  43629  proththd  43630  nnoALTV  43711  bgoldbtbndlem4  43824  cznnring  44129  divge1b  44469  divgt1b  44470  m1modmmod  44483  difmodm1lt  44484  nn0eo  44490  regt1loggt0  44498  rege1logbrege0  44520  logblt1b  44526  fllog2  44530  nnolog2flm1  44552  dignn0flhalflem1  44577  rrxlinesc  44624  rrxlinec  44625  eenglngeehlnmlem1  44626  eenglngeehlnmlem2  44627  line2ylem  44640  line2  44641  line2xlem  44642  reseccl  44754  recsccl  44755  amgmwlem  44805  amgmlemALT  44806
  Copyright terms: Public domain W3C validator