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

Theorem 1red 10329
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 10328 . 2 1 ∈ ℝ
21a1i 11 1 (𝜑 → 1 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  cr 10223  1c1 10225
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-mulcl 10286  ax-mulrcl 10287  ax-i2m1 10292  ax-1ne0 10293  ax-rrecex 10296  ax-cnre 10297
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3400  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-nul 4124  df-if 4287  df-sn 4378  df-pr 4380  df-op 4384  df-uni 4638  df-br 4852  df-iota 6067  df-fv 6112  df-ov 6880
This theorem is referenced by:  recgt0  11155  ltrec  11193  nn0p1gt0  11591  nn0ge2m1nn  11629  nn0le2is012  11710  suprzcl  11726  ledivge1le  12118  qbtwnre  12251  iccf1o  12542  xov1plusxeqvd  12544  zltaddlt1le  12550  fznatpl1  12621  elfz1b  12635  fzonn0p1p1  12774  elfzom1p1elfzo  12775  elfznelfzo  12800  elfznelfzob  12801  fladdz  12853  2tnp1ge0ge0  12857  flhalf  12858  ltdifltdiv  12862  fldiv4lem1div2uz2  12864  mulp1mod1  12938  m1modge3gt1  12944  modltm1p1mod  12949  addmodlteq  12972  ltexp2a  13138  expcan  13139  ltexp2  13140  leexp2  13141  leexp2a  13142  leexp2r  13144  nnlesq  13194  bernneq3  13218  expnbnd  13219  expnlbnd2  13221  fzsdom2  13435  wrdlenge2n0  13556  swrd2lsw  13923  2swrd2eqwrdeq  13924  sqrlem7  14215  rddif  14306  reccn2  14553  rlimo1  14573  o1fsum  14770  abscvgcvg  14776  climcndslem1  14806  flo1  14811  harmonic  14816  geomulcvg  14832  fprodrecl  14907  fprodle  14950  bpoly4  15013  efcllem  15031  efgt1  15069  tanhlt1  15113  sinltx  15142  eirrlem  15155  p1modz1  15213  mod2eq1n2dvds  15294  oddge22np1  15296  ltoddhalfle  15308  nn0o1gt2  15320  nno  15321  nn0oddm1d2  15324  nnoddm1d2  15325  bitsfzolem  15378  bitsfzo  15379  bitsmod  15380  bitscmp  15382  bitsinv1lem  15385  smuval2  15426  coprmgcdb  15584  prmind2  15619  dvdsnprmd  15624  isprm5  15639  isprm7  15640  divdenle  15677  zsqrtelqelz  15686  fermltl  15709  odzdvds  15720  modprm0  15730  iserodd  15760  difsqpwdvds  15811  pcfaclem  15822  prmreclem1  15840  4sqlem11  15879  4sqlem12  15880  ramub1lem1  15950  prmgaplem8  15982  2expltfac  16014  pgpfaclem2  18686  znidomb  20120  chfacfisf  20876  chfacfisfcpmat  20877  chfacfscmulgsum  20882  chfacfpmmulgsum  20886  nrginvrcnlem  22712  nmoid  22763  xrsmopn  22832  metnrmlem1a  22878  iccpnfhmeo  22961  htpycc  22996  pcohtpylem  23035  pcoass  23040  pcorevlem  23042  nmhmcn  23136  cncmet  23336  ovoliunlem1  23489  dyadmaxlem  23584  vitalilem2  23596  mbfi1fseqlem6  23707  itg2mulc  23734  itg2monolem1  23737  itg2monolem3  23739  dveflem  23962  mvth  23975  dvlipcn  23977  lhop1lem  23996  dvfsumlem1  24009  dvfsumlem2  24010  dvfsumlem3  24011  dvfsumlem4  24012  dvfsum2  24017  fta1glem2  24146  plyeq0lem  24186  fta1lem  24282  vieta1lem2  24286  aalioulem3  24309  aalioulem4  24310  radcnvlem1  24387  radcnvlem2  24388  dvradcnv  24395  abelthlem2  24406  abelthlem5  24409  abelthlem7  24412  abelth2  24416  cosne0  24497  rplogcl  24570  logdivlti  24586  logno1  24602  advlog  24620  logtayllem  24625  cxplt  24660  cxple  24661  cxpaddlelem  24712  cxpaddle  24713  relogbf  24749  isosctrlem1  24768  isosctrlem2  24769  heron  24785  atanlogaddlem  24860  bndatandm  24876  leibpi  24889  log2tlbnd  24892  birthdaylem3  24900  rlimcnp  24912  rlimcnp2  24913  efrlim  24916  cxp2limlem  24922  divsqrtsumo1  24930  jensenlem2  24934  logdiflbnd  24941  fsumharmonic  24958  lgamgulmlem2  24976  lgamgulmlem3  24977  lgamgulmlem4  24978  lgamgulmlem5  24979  lgamgulmlem6  24980  lgamcvg2  25001  regamcl  25007  wilthlem2  25015  ftalem2  25020  basellem9  25035  vma1  25112  ppieq0  25122  mumullem2  25126  fsumfldivdiaglem  25135  chpeq0  25153  chtub  25157  chpval2  25163  chpchtsum  25164  chpub  25165  logfacrlim  25169  logexprlim  25170  mersenne  25172  perfectlem2  25175  dchrelbas4  25188  bcmono  25222  bposlem1  25229  bposlem2  25230  zabsle1  25241  lgslem3  25244  lgsmod  25268  lgsdir2lem4  25273  lgsdirprm  25276  gausslemma2dlem1a  25310  gausslemma2d  25319  lgsquadlem2  25326  2sqlem8  25371  chebbnd1lem1  25378  chebbnd1lem2  25379  chtppilimlem1  25382  chebbnd2  25386  chto1lb  25387  chpchtlim  25388  chpo1ubb  25390  vmadivsum  25391  rplogsumlem1  25393  rpvmasumlem  25396  dchrisumlem3  25400  dchrmusumlema  25402  dchrmusum2  25403  dchrvmasumlem2  25407  dchrvmasumlem3  25408  dchrvmasumiflem1  25410  dchrvmasumiflem2  25411  dchrisum0flblem1  25417  dchrisum0flblem2  25418  dchrisum0fno1  25420  dchrisum0re  25422  dchrisum0lema  25423  dchrisum0lem1b  25424  dchrisum0lem2a  25426  dchrisum0lem2  25427  dchrisum0lem3  25428  rplogsum  25436  dirith2  25437  mudivsum  25439  mulogsumlem  25440  mulogsum  25441  mulog2sumlem1  25443  mulog2sumlem2  25444  vmalogdivsum2  25447  vmalogdivsum  25448  2vmadivsumlem  25449  log2sumbnd  25453  selberglem2  25455  selberg2lem  25459  chpdifbnd  25464  selberg3lem1  25466  selberg3  25468  selberg4lem1  25469  selberg4  25470  pntrmax  25473  pntrsumo1  25474  pntrsumbnd  25475  selberg3r  25478  selberg4r  25479  selberg34r  25480  pntrlog2bndlem1  25486  pntrlog2bndlem2  25487  pntrlog2bndlem3  25488  pntrlog2bndlem4  25489  pntrlog2bndlem5  25490  pntrlog2bndlem6  25492  pntrlog2bnd  25493  pntpbnd1a  25494  pntpbnd1  25495  pntibndlem2a  25499  pntibndlem2  25500  pntibnd  25502  pntlemc  25504  pntlemg  25507  pntlemr  25511  pntlemk  25515  qabvle  25534  ostth2lem3  25544  ostth2  25546  trgcgrg  25630  tgcgr4  25646  ttgcontlem1  25985  axpaschlem  26040  axlowdimlem16  26057  axcontlem2  26065  axcontlem7  26070  nbusgrvtxm1  26503  upgrewlkle2  26736  pthdlem1  26896  crctcshwlkn0lem3  26939  crctcshwlkn0lem5  26941  wwlksm1edg  27014  wwlksnextproplem2  27054  clwlkclwwlklem2fv1  27144  clwlkclwwlklem2fv2  27145  clwlkclwwlklem2  27149  clwlkclwwlk2  27152  clwwisshclwwslem  27163  clwwlkf1  27204  clwwlkext2edg  27212  clwlknf1oclwwlknlem1  27251  clwwlknonex2lem2  27283  numclwwlk7  27585  frgrreggt1  27587  frgrogt3nreg  27591  smcnlem  27886  nmoub3i  27962  blocnilem  27993  ubthlem2  28061  minvecolem4  28070  htthlem  28108  nmcexi  29219  nmopcoi  29288  stadd3i  29441  cdj1i  29626  nn0sqeq1  29846  nnmulge  29848  nndiffz1  29881  fzsplit3  29886  pmtrto1cl  30180  fzto1st1  30183  fzto1st  30184  psgnfzto1st  30186  1smat1  30201  submateqlem1  30204  madjusmdetlem2  30225  unitdivcld  30278  sqsscirc1  30285  nexple  30402  indf1o  30417  esumdivc  30476  dya2ub  30663  dya2iocress  30667  dya2iocbrsiga  30668  dya2icobrsiga  30669  dya2icoseg  30670  dya2iocucvr  30677  sxbrsigalem2  30679  fibp1  30794  probmeasb  30823  dstrvprob  30864  dstfrvunirn  30867  ballotlemfc0  30885  ballotlemfcc  30886  ballotlemsgt1  30903  ballotlemsel1i  30905  ballotlemfrcn0  30922  signsply0  30959  itgexpif  31015  reprlt  31028  chtvalz  31038  breprexplemc  31041  breprexp  31042  circlemeth  31049  tgoldbachgnn  31068  subfaclim  31498  cvmliftlem2  31596  cvmliftlem13  31606  snmlff  31639  bccolsum  31952  faclim  31959  nn0prpwlem  32643  dnibndlem10  32799  dnibndlem12  32801  knoppcnlem4  32808  unblimceq0  32820  knoppndvlem1  32825  knoppndvlem2  32826  knoppndvlem3  32827  knoppndvlem7  32831  knoppndvlem11  32835  knoppndvlem12  32836  knoppndvlem14  32838  knoppndvlem15  32839  knoppndvlem17  32841  knoppndvlem18  32842  knoppndvlem20  32844  poimirlem6  33730  poimirlem7  33731  poimirlem15  33739  poimirlem19  33743  poimirlem29  33753  poimirlem30  33754  poimirlem31  33755  poimirlem32  33756  broucube  33758  itg2addnclem2  33776  itg2addnclem3  33777  areacirclem1  33814  areacirclem4  33817  incsequz  33857  totbndbnd  33901  bfplem2  33935  lzenom  37836  irrapxlem1  37889  irrapxlem2  37890  irrapxlem4  37892  irrapxlem5  37893  pellexlem2  37897  pell1qrge1  37937  pell1qr1  37938  elpell1qr2  37939  pell14qrgapw  37943  pellfundgt1  37950  pellfundglb  37952  pellfundex  37953  pellfundrp  37955  pellfundne1  37956  rmspecsqrtnq  37973  rmspecnonsq  37974  rmspecfund  37976  rmspecpos  37983  monotoddzzfi  38009  rmygeid  38033  areaquad  38303  imo72b2lem0  38966  imo72b2lem1  38972  imo72b2  38976  cvgdvgrat  39013  radcnvrat  39014  hashnzfzclim  39022  lhe4.4ex1a  39029  binomcxplemnn0  39049  binomcxplemdvbinom  39053  binomcxplemnotnn0  39056  oddfl  39972  abscosbd  39973  zltlesub  39980  abssinbd  39991  monoords  39993  fzisoeu  39996  fzdifsuc2  40006  suplesup  40036  xralrple2  40051  infxr  40064  infleinflem2  40068  reclt0d  40088  xrralrecnnge  40093  sqrlearg  40261  iooiinioc  40264  fmul01  40293  fmul01lt1lem1  40297  fmul01lt1lem2  40298  climsuselem1  40320  sumnnodd  40343  0ellimcdiv  40362  dvmptidg  40612  dvcosax  40622  ioodvbdlimc1lem1  40627  ioodvbdlimc1lem2  40628  ioodvbdlimc2lem  40630  dvxpaek  40636  dvnmul  40639  iblspltprt  40669  itgspltprt  40675  stoweidlem5  40702  stoweidlem7  40704  stoweidlem10  40707  stoweidlem11  40708  stoweidlem12  40709  stoweidlem13  40710  stoweidlem14  40711  stoweidlem16  40713  stoweidlem18  40715  stoweidlem20  40717  stoweidlem24  40721  stoweidlem25  40722  stoweidlem34  40731  stoweidlem36  40733  stoweidlem38  40735  stoweidlem40  40737  stoweidlem41  40738  stoweidlem42  40739  stoweidlem45  40742  stoweidlem51  40748  stoweidlem60  40757  wallispilem3  40764  wallispilem4  40765  wallispilem5  40766  wallispi  40767  wallispi2lem1  40768  wallispi2lem2  40769  wallispi2  40770  stirlinglem1  40771  stirlinglem3  40773  stirlinglem5  40775  stirlinglem6  40776  stirlinglem7  40777  stirlinglem8  40778  stirlinglem10  40780  stirlinglem11  40781  stirlinglem12  40782  stirlinglem13  40783  stirlinglem15  40785  dirker2re  40789  dirkerval2  40791  dirkerre  40792  dirkertrigeqlem1  40795  dirkertrigeqlem3  40797  dirkeritg  40799  dirkercncflem1  40800  dirkercncflem2  40801  dirkercncflem4  40803  fourierdlem5  40809  fourierdlem6  40810  fourierdlem11  40815  fourierdlem15  40819  fourierdlem19  40823  fourierdlem20  40824  fourierdlem24  40828  fourierdlem26  40830  fourierdlem28  40832  fourierdlem30  40834  fourierdlem39  40843  fourierdlem41  40845  fourierdlem43  40847  fourierdlem47  40850  fourierdlem48  40851  fourierdlem56  40859  fourierdlem60  40863  fourierdlem61  40864  fourierdlem62  40865  fourierdlem64  40867  fourierdlem65  40868  fourierdlem66  40869  fourierdlem68  40871  fourierdlem73  40876  fourierdlem78  40881  fourierdlem79  40882  fourierdlem87  40890  fourierdlem103  40906  fourierdlem104  40907  sqwvfoura  40925  fouriersw  40928  etransclem4  40935  etransclem23  40954  etransclem24  40955  etransclem31  40962  etransclem32  40963  etransclem35  40966  etransclem41  40972  etransclem46  40977  etransclem48  40979  etransc  40980  ioorrnopnxrlem  41006  nnfoctbdjlem  41152  iundjiun  41157  hoidmvlelem1  41292  hoidmvlelem2  41293  hoidmvlelem3  41294  hoidmvlelem4  41295  ovnhoilem1  41298  vonioolem2  41378  vonicclem2  41381  pimrecltneg  41416  smfrec  41479  smfmullem1  41481  smfmullem2  41482  smfdiv  41487  sigaradd  41538  p1lep2  41891  zm1nn  41893  m1mod0mod1  41915  iccpartiltu  41934  iccpartlt  41936  iccpartgt  41939  pfx2  41988  fmtnoge3  42018  fmtnodvds  42032  fmtnoprmfac2lem1  42054  2pwp1prm  42079  flsqrt  42084  sfprmdvdsmersenne  42096  lighneallem2  42099  lighneallem4a  42101  proththdlem  42106  proththd  42107  nnoALTV  42182  bgoldbtbndlem4  42272  cznnring  42525  divge1b  42871  divgt1b  42872  m1modmmod  42885  difmodm1lt  42886  nn0eo  42891  regt1loggt0  42899  rege1logbrege0  42921  logblt1b  42927  fllog2  42931  nnolog2flm1  42953  dignn0flhalflem1  42978  reseccl  43066  recsccl  43067  amgmwlem  43120  amgmlemALT  43121
  Copyright terms: Public domain W3C validator