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

Theorem 1red 9911
Description: 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
1red (𝜑 → 1 ∈ ℝ)

Proof of Theorem 1red
StepHypRef Expression
1 1re 9895 . 2 1 ∈ ℝ
21a1i 11 1 (𝜑 → 1 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cr 9791  1c1 9793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-mulcl 9854  ax-mulrcl 9855  ax-i2m1 9860  ax-1ne0 9861  ax-rrecex 9864  ax-cnre 9865
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5753  df-fv 5797  df-ov 6529
This theorem is referenced by:  recgt0  10718  ltrec  10756  nn0p1gt0  11171  nn0ge2m1nn  11209  suprzcl  11291  ledivge1le  11735  qbtwnre  11865  iccf1o  12145  xov1plusxeqvd  12147  zltaddlt1le  12153  fznatpl1  12222  elfz1b  12236  fzonn0p1p1  12370  elfzom1p1elfzo  12371  elfznelfzo  12396  elfznelfzob  12397  fladdz  12445  2tnp1ge0ge0  12449  flhalf  12450  ltdifltdiv  12454  fldiv4lem1div2uz2  12456  mulp1mod1  12530  m1modge3gt1  12536  modltm1p1mod  12541  addmodlteq  12564  ltexp2a  12731  expcan  12732  ltexp2  12733  leexp2  12734  leexp2a  12735  leexp2r  12737  nnlesq  12787  bernneq3  12811  expnbnd  12812  expnlbnd2  12814  fzsdom2  13029  wrdlenge2n0  13144  swrd2lsw  13491  2swrd2eqwrdeq  13492  rddif  13876  reccn2  14123  rlimo1  14143  o1fsum  14334  abscvgcvg  14340  climcndslem1  14368  flo1  14373  harmonic  14378  geomulcvg  14394  fprodrecl  14470  fprodle  14514  bpoly4  14577  efcllem  14595  efgt1  14633  tanhlt1  14677  sinltx  14706  eirrlem  14719  mod2eq1n2dvds  14857  oddge22np1  14859  ltoddhalfle  14871  nn0o1gt2  14883  nno  14884  nn0oddm1d2  14887  nnoddm1d2  14888  bitsfzolem  14942  bitsfzo  14943  bitsmod  14944  bitscmp  14946  bitsinv1lem  14949  smuval2  14990  coprmgcdb  15148  prmind2  15184  dvdsnprmd  15189  isprm5  15205  isprm7  15206  divdenle  15243  zsqrtelqelz  15252  fermltl  15275  odzdvds  15286  modprm0  15296  iserodd  15326  difsqpwdvds  15377  pcfaclem  15388  prmreclem1  15406  4sqlem11  15445  4sqlem12  15446  ramub1lem1  15516  prmgaplem8  15548  2expltfac  15585  pgpfaclem2  18252  znidomb  19676  chfacfisf  20425  chfacfisfcpmat  20426  chfacfscmulgsum  20431  chfacfpmmulgsum  20435  nrginvrcnlem  22252  nmoid  22303  xrsmopn  22370  metnrmlem1a  22416  iccpnfhmeo  22499  htpycc  22534  pcohtpylem  22574  pcoass  22579  pcorevlem  22581  nmhmcn  22675  cncmet  22871  ovoliunlem1  23021  dyadmaxlem  23115  vitalilem2  23128  mbfi1fseqlem6  23237  itg2mulc  23264  itg2monolem1  23267  itg2monolem3  23269  dveflem  23490  mvth  23503  dvlipcn  23505  lhop1lem  23524  dvfsumlem1  23537  dvfsumlem2  23538  dvfsumlem3  23539  dvfsumlem4  23540  dvfsum2  23545  fta1glem2  23674  plyeq0lem  23714  fta1lem  23810  vieta1lem2  23814  aalioulem3  23837  aalioulem4  23838  radcnvlem1  23915  radcnvlem2  23916  dvradcnv  23923  abelthlem2  23934  abelthlem5  23937  abelthlem7  23940  abelth2  23944  cosne0  24024  rplogcl  24098  logdivlti  24114  logno1  24126  advlog  24144  logtayllem  24149  cxplt  24184  cxple  24185  cxpaddlelem  24236  cxpaddle  24237  relogbf  24273  isosctrlem1  24292  isosctrlem2  24293  heron  24309  atanlogaddlem  24384  bndatandm  24400  leibpi  24413  log2tlbnd  24416  birthdaylem3  24424  rlimcnp  24436  rlimcnp2  24437  efrlim  24440  cxp2limlem  24446  divsqrtsumo1  24454  jensenlem2  24458  logdiflbnd  24465  fsumharmonic  24482  lgamgulmlem2  24500  lgamgulmlem3  24501  lgamgulmlem4  24502  lgamgulmlem5  24503  lgamgulmlem6  24504  lgamcvg2  24525  regamcl  24531  wilthlem2  24539  ftalem2  24544  basellem9  24559  vma1  24636  ppieq0  24646  mumullem2  24650  fsumfldivdiaglem  24659  chpeq0  24677  chtub  24681  chpval2  24687  chpchtsum  24688  chpub  24689  logfacrlim  24693  logexprlim  24694  mersenne  24696  perfectlem2  24699  dchrelbas4  24712  bcmono  24746  bposlem1  24753  bposlem2  24754  zabsle1  24765  lgslem3  24768  lgslem4  24769  lgsmod  24792  lgsdir2lem4  24797  lgsdirprm  24800  gausslemma2dlem1a  24834  gausslemma2d  24843  lgsquadlem2  24850  2sqlem8  24895  chebbnd1lem1  24902  chebbnd1lem2  24903  chtppilimlem1  24906  chebbnd2  24910  chto1lb  24911  chpchtlim  24912  chpo1ubb  24914  vmadivsum  24915  rplogsumlem1  24917  rpvmasumlem  24920  dchrisumlem3  24924  dchrmusumlema  24926  dchrmusum2  24927  dchrvmasumlem2  24931  dchrvmasumlem3  24932  dchrvmasumiflem1  24934  dchrvmasumiflem2  24935  dchrisum0flblem1  24941  dchrisum0flblem2  24942  dchrisum0fno1  24944  dchrisum0re  24946  dchrisum0lema  24947  dchrisum0lem1b  24948  dchrisum0lem2a  24950  dchrisum0lem2  24951  dchrisum0lem3  24952  rplogsum  24960  dirith2  24961  mudivsum  24963  mulogsumlem  24964  mulogsum  24965  mulog2sumlem1  24967  mulog2sumlem2  24968  vmalogdivsum2  24971  vmalogdivsum  24972  2vmadivsumlem  24973  log2sumbnd  24977  selberglem2  24979  selberg2lem  24983  chpdifbnd  24988  selberg3lem1  24990  selberg3  24992  selberg4lem1  24993  selberg4  24994  pntrmax  24997  pntrsumo1  24998  pntrsumbnd  24999  selberg3r  25002  selberg4r  25003  selberg34r  25004  pntrlog2bndlem1  25010  pntrlog2bndlem2  25011  pntrlog2bndlem3  25012  pntrlog2bndlem4  25013  pntrlog2bndlem5  25014  pntrlog2bndlem6  25016  pntrlog2bnd  25017  pntpbnd1a  25018  pntpbnd1  25019  pntibndlem2a  25023  pntibndlem2  25024  pntibnd  25026  pntlemc  25028  pntlemg  25031  pntlemr  25035  pntlemk  25039  qabvle  25058  ostth2lem3  25068  ostth2  25070  trgcgrg  25155  tgcgr4  25171  ttgcontlem1  25510  axpaschlem  25565  axlowdimlem16  25582  axcontlem2  25590  axcontlem7  25595  wwlkm1edg  26056  wwlkextproplem1  26062  wwlkextproplem2  26063  clwlkisclwwlklem2fv1  26103  clwlkisclwwlklem2fv2  26104  clwlkisclwwlklem1  26108  clwlkisclwwlk2  26111  clwwlkf1  26117  clwwlkext2edg  26123  clwwisshclwwlem  26127  usg2cwwkdifex  26142  extwwlkfablem2  26398  numclwwlkovf2ex  26406  numclwlk1lem2f1  26414  numclwwlk7  26434  frgrareggt1  26436  frgraregord013  26438  frgraogt3nreg  26440  smcnlem  26729  nmoub3i  26805  blocnilem  26836  ubthlem2  26904  minvecolem4  26913  htthlem  26951  nmcexi  28062  nmopcoi  28131  stadd3i  28284  cdj1i  28469  nn0sqeq1  28694  nndiffz1  28729  fzsplit3  28733  pmtrto1cl  28973  fzto1st1  28976  fzto1st  28977  psgnfzto1st  28979  1smat1  28991  submateqlem1  28994  madjusmdetlem2  29015  unitdivcld  29068  sqsscirc1  29075  nexple  29192  indf1o  29206  esumdivc  29265  dya2ub  29452  dya2iocress  29456  dya2iocbrsiga  29457  dya2icobrsiga  29458  dya2icoseg  29459  dya2iocucvr  29466  sxbrsigalem2  29468  fibp1  29583  probmeasb  29612  dstrvprob  29653  dstfrvunirn  29656  ballotlemfc0  29674  ballotlemfcc  29675  ballotlemsgt1  29692  ballotlemsel1i  29694  ballotlemfrcn0  29711  signsply0  29747  subfaclim  30217  cvmliftlem2  30315  cvmliftlem13  30325  snmlff  30358  bccolsum  30671  faclim  30678  nn0prpwlem  31280  dnibndlem10  31440  dnibndlem12  31442  knoppcnlem4  31449  unblimceq0  31461  knoppndvlem1  31466  knoppndvlem2  31467  knoppndvlem3  31468  knoppndvlem7  31472  knoppndvlem11  31476  knoppndvlem12  31477  knoppndvlem14  31479  knoppndvlem15  31480  knoppndvlem17  31482  knoppndvlem18  31483  knoppndvlem20  31485  poimirlem6  32368  poimirlem7  32369  poimirlem15  32377  poimirlem19  32381  poimirlem29  32391  poimirlem30  32392  poimirlem31  32393  poimirlem32  32394  broucube  32396  itg2addnclem2  32415  itg2addnclem3  32416  areacirclem1  32453  areacirclem4  32456  incsequz  32497  totbndbnd  32541  bfplem2  32575  lzenom  36134  irrapxlem1  36187  irrapxlem2  36188  irrapxlem4  36190  irrapxlem5  36191  pellexlem2  36195  pell1qrge1  36235  pell1qr1  36236  elpell1qr2  36237  pell14qrgapw  36241  pellfundgt1  36248  pellfundglb  36250  pellfundex  36251  pellfundrp  36253  pellfundne1  36254  rmspecsqrtnq  36271  rmspecnonsq  36273  rmspecfund  36275  rmspecpos  36282  monotoddzzfi  36308  rmygeid  36332  areaquad  36604  imo72b2lem0  37270  imo72b2lem1  37276  imo72b2  37280  cvgdvgrat  37317  radcnvrat  37318  hashnzfzclim  37326  lhe4.4ex1a  37333  binomcxplemnn0  37353  binomcxplemdvbinom  37357  binomcxplemnotnn0  37360  oddfl  38213  abscosbd  38214  zltlesub  38221  abssinbd  38233  monoords  38235  fzisoeu  38238  fzdifsuc2  38249  suplesup  38279  xralrple2  38294  infxr  38307  infleinflem2  38311  reclt0d  38331  xrralrecnnge  38337  sqrlearg  38410  iooiinioc  38413  fmul01  38430  fmul01lt1lem1  38434  fmul01lt1lem2  38435  climsuselem1  38457  sumnnodd  38480  0ellimcdiv  38499  dvmptidg  38588  dvcosax  38599  ioodvbdlimc1lem1  38604  ioodvbdlimc1lem2  38605  ioodvbdlimc2lem  38607  dvxpaek  38613  dvnmul  38616  iblspltprt  38648  itgspltprt  38654  stoweidlem5  38681  stoweidlem7  38683  stoweidlem10  38686  stoweidlem11  38687  stoweidlem12  38688  stoweidlem13  38689  stoweidlem14  38690  stoweidlem16  38692  stoweidlem18  38694  stoweidlem20  38696  stoweidlem24  38700  stoweidlem25  38701  stoweidlem34  38710  stoweidlem36  38712  stoweidlem38  38714  stoweidlem40  38716  stoweidlem41  38717  stoweidlem42  38718  stoweidlem45  38721  stoweidlem51  38727  stoweidlem60  38736  wallispilem3  38743  wallispilem4  38744  wallispilem5  38745  wallispi  38746  wallispi2lem1  38747  wallispi2lem2  38748  wallispi2  38749  stirlinglem1  38750  stirlinglem3  38752  stirlinglem5  38754  stirlinglem6  38755  stirlinglem7  38756  stirlinglem8  38757  stirlinglem10  38759  stirlinglem11  38760  stirlinglem12  38761  stirlinglem13  38762  stirlinglem15  38764  dirker2re  38768  dirkerval2  38770  dirkerre  38771  dirkertrigeqlem1  38774  dirkertrigeqlem3  38776  dirkeritg  38778  dirkercncflem1  38779  dirkercncflem2  38780  dirkercncflem4  38782  fourierdlem5  38788  fourierdlem6  38789  fourierdlem11  38794  fourierdlem15  38798  fourierdlem19  38802  fourierdlem20  38803  fourierdlem24  38807  fourierdlem26  38809  fourierdlem28  38811  fourierdlem30  38813  fourierdlem39  38822  fourierdlem41  38824  fourierdlem43  38826  fourierdlem47  38829  fourierdlem48  38830  fourierdlem56  38838  fourierdlem60  38842  fourierdlem61  38843  fourierdlem62  38844  fourierdlem64  38846  fourierdlem65  38847  fourierdlem66  38848  fourierdlem68  38850  fourierdlem73  38855  fourierdlem78  38860  fourierdlem79  38861  fourierdlem87  38869  fourierdlem103  38885  fourierdlem104  38886  sqwvfoura  38904  fouriersw  38907  etransclem4  38914  etransclem23  38933  etransclem24  38934  etransclem31  38941  etransclem32  38942  etransclem35  38945  etransclem41  38951  etransclem46  38956  etransclem48  38958  etransc  38959  ioorrnopnxrlem  38985  nnfoctbdjlem  39131  iundjiun  39136  hoidmvlelem1  39268  hoidmvlelem2  39269  hoidmvlelem3  39270  hoidmvlelem4  39271  ovnhoilem1  39274  vonioolem2  39355  vonicclem2  39358  pimrecltneg  39393  smfrec  39457  smfmullem1  39459  smfmullem2  39460  smfdiv  39465  sigaradd  39487  m1mod0mod1  39733  iccpartiltu  39744  iccpartlt  39746  iccpartgt  39749  fmtnoge3  39764  fmtnodvds  39778  fmtnoprmfac2lem1  39800  2pwp1prm  39825  flsqrt  39830  sfprmdvdsmersenne  39842  lighneallem2  39845  lighneallem4a  39847  proththdlem  39852  proththd  39853  nnoALTV  39928  bgoldbtbndlem4  40008  pfx2  40059  p1lep2  40152  zm1nn  40154  nbusgrvtxm1  40588  upgrewlkle2  40789  pthdlem1  40953  crctcsh1wlkn0lem3  40996  crctcsh1wlkn0lem5  40998  wwlksm1edg  41059  wwlksnextproplem2  41097  clwlkclwwlklem2fv1  41185  clwlkclwwlklem2fv2  41186  clwlkclwwlklem2  41190  clwlkclwwlk2  41193  clwwlksf1  41205  clwwlksext2edg  41211  clwwisshclwwslem  41215  av-extwwlkfablem2  41491  av-numclwwlkovf2ex  41498  av-numclwlk1lem2f1  41505  av-numclwwlk7  41526  av-frgrareggt1  41528  av-frgraogt3nreg  41532  cznnring  41729  nn0le2is012  41919  divge1b  42077  divgt1b  42078  m1modmmod  42091  difmodm1lt  42092  nn0eo  42097  regt1loggt0  42109  rege1logbrege0  42131  logblt1b  42137  fllog2  42141  nnolog2flm1  42163  dignn0flhalflem1  42188  reseccl  42235  recsccl  42236  amgmwlem  42299  amgmlemALT  42300
  Copyright terms: Public domain W3C validator