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

Theorem 1red 10631
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 10630 . 2 1 ∈ ℝ
21a1i 11 1 (𝜑 → 1 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cr 10525  1c1 10527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rrecex 10598  ax-cnre 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-iota 6308  df-fv 6357  df-ov 7148
This theorem is referenced by:  recgt0  11475  ltrec  11511  nnne0  11660  nn0p1gt0  11915  nn0ge2m1nn  11953  nn0le2is012  12035  suprzcl  12051  ledivge1le  12450  qbtwnre  12582  lincmb01cmp  12871  iccf1o  12872  xov1plusxeqvd  12874  zltaddlt1le  12880  fznatpl1  12951  elfz1b  12966  fzonn0p1p1  13106  elfznelfzo  13132  elfznelfzob  13133  fladdz  13185  2tnp1ge0ge0  13189  flhalf  13190  ltdifltdiv  13194  fldiv4lem1div2uz2  13196  mulp1mod1  13270  m1modge3gt1  13276  modltm1p1mod  13281  addmodlteq  13304  ltexp2a  13520  expcan  13523  ltexp2  13524  leexp2  13525  leexp2a  13526  leexp2r  13528  nnlesq  13558  bernneq3  13582  expnbnd  13583  expnlbnd2  13585  expnngt1  13592  fzsdom2  13779  wrdlenge2n0  13894  swrd2lsw  14304  2swrd2eqwrdeq  14305  sqrlem7  14598  rddif  14690  reccn2  14943  rlimo1  14963  o1fsum  15158  abscvgcvg  15164  climcndslem1  15194  flo1  15199  harmonic  15204  geomulcvg  15222  fprodrecl  15297  fprodreclf  15303  fprodle  15340  bpoly4  15403  efcllem  15421  efgt1  15459  tanhlt1  15503  sinltx  15532  eirrlem  15547  p1modz1  15604  mod2eq1n2dvds  15686  oddge22np1  15688  ltoddhalfle  15700  nn0o1gt2  15722  nno  15723  nn0oddm1d2  15726  nnoddm1d2  15727  bitsfzolem  15773  bitsfzo  15774  bitsmod  15775  bitscmp  15777  bitsinv1lem  15780  smuval2  15821  coprmgcdb  15983  prmind2  16019  dvdsnprmd  16024  2mulprm  16027  isprm5  16041  isprm7  16042  divdenle  16079  zsqrtelqelz  16088  fermltl  16111  odzdvds  16122  modprm0  16132  iserodd  16162  difsqpwdvds  16213  pcfaclem  16224  prmreclem1  16242  4sqlem11  16281  4sqlem12  16282  ramub1lem1  16352  prmgaplem8  16384  2expltfac  16416  pgpfaclem2  19135  znidomb  20638  chfacfisf  21392  chfacfisfcpmat  21393  chfacfscmulgsum  21398  chfacfpmmulgsum  21402  nrginvrcnlem  23229  nmoid  23280  xrsmopn  23349  metnrmlem1a  23395  iccpnfhmeo  23478  lebnumii  23499  htpycc  23513  pcohtpylem  23552  pcoass  23557  pcorevlem  23559  nmhmcn  23653  cncmet  23854  ovoliunlem1  24032  dyadmaxlem  24127  vitalilem2  24139  mbfi1fseqlem6  24250  itg2mulc  24277  itg2monolem1  24280  itg2monolem3  24282  dveflem  24505  mvth  24518  dvlipcn  24520  lhop1lem  24539  dvfsumlem1  24552  dvfsumlem2  24553  dvfsumlem3  24554  dvfsumlem4  24555  dvfsum2  24560  fta1glem2  24689  plyeq0lem  24729  fta1lem  24825  vieta1lem2  24829  aalioulem3  24852  aalioulem4  24853  radcnvlem1  24930  radcnvlem2  24931  dvradcnv  24938  abelthlem2  24949  abelthlem5  24952  abelthlem7  24955  abelth2  24959  cosne0  25041  rplogcl  25114  logdivlti  25130  logno1  25146  dvlog2lem  25162  advlog  25164  logtayllem  25169  cxplt  25204  cxple  25205  cxpaddlelem  25259  cxpaddle  25260  relogbf  25296  logbgt0b  25298  isosctrlem1  25323  isosctrlem2  25324  chordthmlem4  25340  heron  25343  atanlogaddlem  25418  bndatandm  25434  leibpi  25448  log2tlbnd  25451  birthdaylem3  25459  rlimcnp  25471  rlimcnp2  25472  efrlim  25475  cxp2limlem  25481  cxp2lim  25482  divsqrtsumo1  25489  jensenlem2  25493  logdiflbnd  25500  fsumharmonic  25517  lgamgulmlem2  25535  lgamgulmlem3  25536  lgamgulmlem4  25537  lgamgulmlem5  25538  lgamgulmlem6  25539  lgamcvg2  25560  regamcl  25566  wilthlem2  25574  ftalem2  25579  basellem9  25594  vma1  25671  ppieq0  25681  mumullem2  25685  fsumfldivdiaglem  25694  chpeq0  25712  chtub  25716  chpval2  25722  chpchtsum  25723  chpub  25724  logfacrlim  25728  logexprlim  25729  mersenne  25731  perfectlem2  25734  dchrelbas4  25747  bcmono  25781  bposlem1  25788  bposlem2  25789  zabsle1  25800  lgslem3  25803  lgsmod  25827  lgsdir2lem4  25832  lgsdirprm  25835  gausslemma2dlem1a  25869  gausslemma2d  25878  lgsquadlem2  25885  2sqlem8  25930  chebbnd1lem1  25973  chebbnd1lem2  25974  chtppilimlem1  25977  chebbnd2  25981  chto1lb  25982  chpchtlim  25983  chpo1ubb  25985  vmadivsum  25986  rplogsumlem1  25988  rpvmasumlem  25991  dchrisumlem3  25995  dchrmusumlema  25997  dchrmusum2  25998  dchrvmasumlem2  26002  dchrvmasumlem3  26003  dchrvmasumiflem1  26005  dchrvmasumiflem2  26006  dchrisum0flblem1  26012  dchrisum0flblem2  26013  dchrisum0fno1  26015  dchrisum0re  26017  dchrisum0lema  26018  dchrisum0lem1b  26019  dchrisum0lem2a  26021  dchrisum0lem2  26022  dchrisum0lem3  26023  rplogsum  26031  dirith2  26032  mudivsum  26034  mulogsumlem  26035  mulogsum  26036  mulog2sumlem1  26038  mulog2sumlem2  26039  vmalogdivsum2  26042  vmalogdivsum  26043  2vmadivsumlem  26044  log2sumbnd  26048  selberglem2  26050  selberg2lem  26054  chpdifbnd  26059  selberg3lem1  26061  selberg3  26063  selberg4lem1  26064  selberg4  26065  pntrmax  26068  pntrsumo1  26069  pntrsumbnd  26070  selberg3r  26073  selberg4r  26074  selberg34r  26075  pntrlog2bndlem1  26081  pntrlog2bndlem2  26082  pntrlog2bndlem3  26083  pntrlog2bndlem4  26084  pntrlog2bndlem5  26085  pntrlog2bndlem6  26087  pntrlog2bnd  26088  pntpbnd1a  26089  pntpbnd1  26090  pntibndlem2a  26094  pntibndlem2  26095  pntibnd  26097  pntlemc  26099  pntlemg  26102  pntlemr  26106  pntlemk  26110  pnt  26118  qabvle  26129  ostth2lem3  26139  ostth2  26141  trgcgrg  26229  tgcgr4  26245  ttgcontlem1  26599  axpaschlem  26654  axlowdimlem16  26671  axcontlem2  26679  axcontlem7  26684  nbusgrvtxm1  27089  upgrewlkle2  27316  pthdlem1  27475  crctcshwlkn0lem3  27518  crctcshwlkn0lem5  27520  wwlksm1edg  27587  wwlksnextproplem2  27617  clwlkclwwlklem2fv1  27701  clwlkclwwlklem2fv2  27702  clwlkclwwlklem2  27706  clwlkclwwlk2  27709  clwwisshclwwslem  27720  clwwlkf1  27756  clwwlkext2edg  27763  clwlknf1oclwwlknlem1  27788  clwwlknonex2lem2  27815  numclwwlk7  28098  frgrreggt1  28100  frgrogt3nreg  28104  smcnlem  28402  nmoub3i  28478  blocnilem  28509  ubthlem2  28576  minvecolem4  28585  htthlem  28622  nmcexi  29731  nmopcoi  29800  stadd3i  29953  cdj1i  30138  nnmulge  30401  nndiffz1  30436  fzsplit3  30444  wrdt2ind  30555  pmtrto1cl  30669  fzto1st1  30672  fzto1st  30673  psgnfzto1st  30675  cycpmco2lem6  30701  cycpmco2lem7  30702  cycpmrn  30713  qsidomlem1  30883  1smat1  30969  submateqlem1  30972  madjusmdetlem2  30993  unitdivcld  31044  sqsscirc1  31051  nexple  31168  indf1o  31183  esumdivc  31242  dya2ub  31428  dya2iocress  31432  dya2iocbrsiga  31433  dya2icobrsiga  31434  dya2icoseg  31435  dya2iocucvr  31442  sxbrsigalem2  31444  fibp1  31559  probmeasb  31588  dstrvprob  31629  dstfrvunirn  31632  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemsgt1  31668  ballotlemsel1i  31670  ballotlemfrcn0  31687  signsply0  31721  itgexpif  31777  reprlt  31790  chtvalz  31800  breprexplemc  31803  breprexp  31804  circlemeth  31811  tgoldbachgnn  31830  acycgr1v  32294  subfaclim  32333  cvmliftlem2  32431  cvmliftlem13  32441  snmlff  32474  bccolsum  32869  faclim  32876  nn0prpwlem  33568  dnibndlem10  33724  dnibndlem12  33726  knoppcnlem4  33733  unblimceq0  33744  knoppndvlem1  33749  knoppndvlem2  33750  knoppndvlem3  33751  knoppndvlem7  33755  knoppndvlem11  33759  knoppndvlem12  33760  knoppndvlem14  33762  knoppndvlem15  33763  knoppndvlem17  33765  knoppndvlem18  33766  knoppndvlem20  33768  poimirlem6  34780  poimirlem7  34781  poimirlem15  34789  poimirlem19  34793  poimirlem29  34803  poimirlem30  34804  poimirlem31  34805  poimirlem32  34806  broucube  34808  itg2addnclem2  34826  itg2addnclem3  34827  areacirclem1  34864  areacirclem4  34867  incsequz  34906  totbndbnd  34950  bfplem2  34984  sn-1ne2  39038  rtprmirr  39074  sn-00idlem2  39109  sn-0ne2  39116  fltnlta  39155  3cubeslem1  39161  3cubeslem3r  39164  3cubeslem4  39166  lzenom  39247  irrapxlem1  39299  irrapxlem2  39300  irrapxlem4  39302  irrapxlem5  39303  pellexlem2  39307  pell1qrge1  39347  pell1qr1  39348  elpell1qr2  39349  pell14qrgapw  39353  pellfundgt1  39360  pellfundglb  39362  pellfundex  39363  pellfundrp  39365  pellfundne1  39366  rmspecsqrtnq  39383  rmspecnonsq  39384  rmspecfund  39386  rmspecpos  39393  monotoddzzfi  39419  rmygeid  39441  areaquad  39703  imo72b2lem0  40396  imo72b2lem1  40402  imo72b2  40406  cvgdvgrat  40525  radcnvrat  40526  hashnzfzclim  40534  lhe4.4ex1a  40541  binomcxplemnn0  40561  binomcxplemdvbinom  40565  binomcxplemnotnn0  40568  oddfl  41423  abscosbd  41424  zltlesub  41431  abssinbd  41442  monoords  41444  fzisoeu  41447  fzdifsuc2  41457  suplesup  41487  xralrple2  41502  infxr  41515  infleinflem2  41519  reclt0d  41538  xrralrecnnge  41542  sqrlearg  41709  iooiinioc  41712  fmul01  41741  fmul01lt1lem1  41745  fmul01lt1lem2  41746  climsuselem1  41768  sumnnodd  41791  0ellimcdiv  41810  dvmptidg  42081  dvcosax  42091  ioodvbdlimc1lem1  42096  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvxpaek  42105  dvnmul  42108  iblspltprt  42138  itgspltprt  42144  stoweidlem5  42171  stoweidlem7  42173  stoweidlem10  42176  stoweidlem11  42177  stoweidlem12  42178  stoweidlem13  42179  stoweidlem14  42180  stoweidlem16  42182  stoweidlem18  42184  stoweidlem20  42186  stoweidlem24  42190  stoweidlem25  42191  stoweidlem34  42200  stoweidlem36  42202  stoweidlem38  42204  stoweidlem40  42206  stoweidlem41  42207  stoweidlem42  42208  stoweidlem45  42211  stoweidlem51  42217  stoweidlem60  42226  wallispilem3  42233  wallispilem4  42234  wallispilem5  42235  wallispi  42236  wallispi2lem1  42237  wallispi2lem2  42238  wallispi2  42239  stirlinglem1  42240  stirlinglem3  42242  stirlinglem5  42244  stirlinglem6  42245  stirlinglem7  42246  stirlinglem8  42247  stirlinglem10  42249  stirlinglem11  42250  stirlinglem12  42251  stirlinglem13  42252  stirlinglem15  42254  dirker2re  42258  dirkerval2  42260  dirkerre  42261  dirkertrigeqlem1  42264  dirkertrigeqlem3  42266  dirkeritg  42268  dirkercncflem1  42269  dirkercncflem2  42270  dirkercncflem4  42272  fourierdlem5  42278  fourierdlem6  42279  fourierdlem11  42284  fourierdlem15  42288  fourierdlem19  42292  fourierdlem20  42293  fourierdlem24  42297  fourierdlem26  42299  fourierdlem28  42301  fourierdlem30  42303  fourierdlem39  42312  fourierdlem41  42314  fourierdlem43  42316  fourierdlem47  42319  fourierdlem48  42320  fourierdlem56  42328  fourierdlem60  42332  fourierdlem61  42333  fourierdlem62  42334  fourierdlem64  42336  fourierdlem65  42337  fourierdlem66  42338  fourierdlem68  42340  fourierdlem73  42345  fourierdlem78  42350  fourierdlem79  42351  fourierdlem87  42359  fourierdlem103  42375  fourierdlem104  42376  sqwvfoura  42394  fouriersw  42397  etransclem4  42404  etransclem23  42423  etransclem24  42424  etransclem31  42431  etransclem32  42432  etransclem35  42435  etransclem41  42441  etransclem46  42446  etransclem48  42448  etransc  42449  ioorrnopnxrlem  42472  nnfoctbdjlem  42618  iundjiun  42623  hoidmvlelem1  42758  hoidmvlelem2  42759  hoidmvlelem3  42760  hoidmvlelem4  42761  ovnhoilem1  42764  vonioolem2  42844  vonicclem2  42847  pimrecltneg  42882  smfrec  42945  smfmullem1  42947  smfmullem2  42948  smfdiv  42953  sigaradd  43004  p1lep2  43381  zm1nn  43383  m1mod0mod1  43410  iccpartiltu  43429  iccpartlt  43431  iccpartgt  43434  fmtnoge3  43539  fmtnodvds  43553  fmtnoprmfac2lem1  43575  2pwp1prm  43598  flsqrt  43603  sfprmdvdsmersenne  43615  lighneallem2  43618  lighneallem4a  43620  proththdlem  43625  proththd  43626  nnoALTV  43707  bgoldbtbndlem4  43820  cznnring  44125  divge1b  44465  divgt1b  44466  m1modmmod  44479  difmodm1lt  44480  nn0eo  44486  regt1loggt0  44494  rege1logbrege0  44516  logblt1b  44522  fllog2  44526  nnolog2flm1  44548  dignn0flhalflem1  44573  rrxlinesc  44620  rrxlinec  44621  eenglngeehlnmlem1  44622  eenglngeehlnmlem2  44623  line2ylem  44636  line2  44637  line2xlem  44638  reseccl  44750  recsccl  44751  amgmwlem  44801  amgmlemALT  44802
  Copyright terms: Public domain W3C validator