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

Theorem 1red 11157
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 11156 . 2 1 ∈ ℝ
21a1i 11 1 (𝜑 → 1 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cr 11051  1c1 11053
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-1cn 11110  ax-icn 11111  ax-addcl 11112  ax-mulcl 11114  ax-mulrcl 11115  ax-i2m1 11120  ax-1ne0 11121  ax-rrecex 11124  ax-cnre 11125
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2945  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361
This theorem is referenced by:  recgt0  12002  ltrec  12038  nnne0  12188  nn0p1gt0  12443  nn0ge2m1nn  12483  nn0le2is012  12568  suprzcl  12584  ledivge1le  12987  qbtwnre  13119  lincmb01cmp  13413  iccf1o  13414  xov1plusxeqvd  13416  zltaddlt1le  13423  fznatpl1  13496  elfz1b  13511  fzonn0p1p1  13652  elfznelfzo  13678  elfznelfzob  13679  fladdz  13731  2tnp1ge0ge0  13735  flhalf  13736  ltdifltdiv  13740  fldiv4lem1div2uz2  13742  mulp1mod1  13818  m1modge3gt1  13824  modltm1p1mod  13829  addmodlteq  13852  ltexp2a  14072  expcan  14075  ltexp2  14076  leexp2  14077  leexp2a  14078  leexp2r  14080  nnlesq  14110  bernneq3  14135  expnbnd  14136  expnlbnd2  14138  expnngt1  14145  fzsdom2  14329  wrdlenge2n0  14441  swrd2lsw  14842  2swrd2eqwrdeq  14843  01sqrexlem7  15134  rddif  15226  reccn2  15480  rlimo1  15500  o1fsum  15699  abscvgcvg  15705  climcndslem1  15735  flo1  15740  harmonic  15745  geomulcvg  15762  fprodrecl  15837  fprodreclf  15843  fprodle  15880  bpoly4  15943  efcllem  15961  efgt1  15999  tanhlt1  16043  sinltx  16072  eirrlem  16087  p1modz1  16144  mod2eq1n2dvds  16230  oddge22np1  16232  ltoddhalfle  16244  nn0o1gt2  16264  nno  16265  nn0oddm1d2  16268  nnoddm1d2  16269  bitsfzolem  16315  bitsfzo  16316  bitsmod  16317  bitscmp  16319  bitsinv1lem  16322  smuval2  16363  coprmgcdb  16526  prmind2  16562  dvdsnprmd  16567  2mulprm  16570  isprm5  16584  isprm7  16585  divdenle  16625  zsqrtelqelz  16634  fermltl  16657  odzdvds  16668  modprm0  16678  iserodd  16708  difsqpwdvds  16760  pcfaclem  16771  prmreclem1  16789  4sqlem11  16828  4sqlem12  16829  ramub1lem1  16899  prmgaplem8  16931  2expltfac  16966  pgpfaclem2  19862  znidomb  20971  chfacfisf  22206  chfacfisfcpmat  22207  chfacfscmulgsum  22212  chfacfpmmulgsum  22216  nrginvrcnlem  24058  nmoid  24109  xrsmopn  24178  metnrmlem1a  24224  iccpnfhmeo  24311  lebnumii  24332  htpycc  24346  pcohtpylem  24385  pcoass  24390  pcorevlem  24392  nmhmcn  24486  cncmet  24689  ovoliunlem1  24869  dyadmaxlem  24964  vitalilem2  24976  mbfi1fseqlem6  25088  itg2mulc  25115  itg2monolem1  25118  itg2monolem3  25120  dveflem  25346  mvth  25359  dvlipcn  25361  lhop1lem  25380  dvfsumlem1  25393  dvfsumlem2  25394  dvfsumlem3  25395  dvfsumlem4  25396  dvfsum2  25401  fta1glem2  25534  plyeq0lem  25574  fta1lem  25670  vieta1lem2  25674  aalioulem3  25697  aalioulem4  25698  radcnvlem1  25775  radcnvlem2  25776  dvradcnv  25783  abelthlem2  25794  abelthlem5  25797  abelthlem7  25800  abelth2  25804  cos02pilt1  25885  cosne0  25888  rplogcl  25962  logdivlti  25978  logno1  25994  dvlog2lem  26010  advlog  26012  logtayllem  26017  cxplt  26052  cxple  26053  cxpaddlelem  26107  cxpaddle  26108  relogbf  26144  logbgt0b  26146  isosctrlem1  26171  isosctrlem2  26172  chordthmlem4  26188  heron  26191  atanlogaddlem  26266  bndatandm  26282  leibpi  26295  log2tlbnd  26298  birthdaylem3  26306  rlimcnp  26318  rlimcnp2  26319  efrlim  26322  cxp2limlem  26328  cxp2lim  26329  divsqrtsumo1  26336  jensenlem2  26340  logdiflbnd  26347  fsumharmonic  26364  lgamgulmlem2  26382  lgamgulmlem3  26383  lgamgulmlem4  26384  lgamgulmlem5  26385  lgamgulmlem6  26386  lgamcvg2  26407  regamcl  26413  wilthlem2  26421  ftalem2  26426  basellem9  26441  vma1  26518  ppieq0  26528  mumullem2  26532  fsumfldivdiaglem  26541  chpeq0  26559  chtub  26563  chpval2  26569  chpchtsum  26570  chpub  26571  logfacrlim  26575  logexprlim  26576  mersenne  26578  perfectlem2  26581  dchrelbas4  26594  bcmono  26628  bposlem1  26635  bposlem2  26636  zabsle1  26647  lgslem3  26650  lgsmod  26674  lgsdir2lem4  26679  lgsdirprm  26682  gausslemma2dlem1a  26716  gausslemma2d  26725  lgsquadlem2  26732  2sqlem8  26777  chebbnd1lem1  26820  chebbnd1lem2  26821  chtppilimlem1  26824  chebbnd2  26828  chto1lb  26829  chpchtlim  26830  chpo1ubb  26832  vmadivsum  26833  rplogsumlem1  26835  rpvmasumlem  26838  dchrisumlem3  26842  dchrmusumlema  26844  dchrmusum2  26845  dchrvmasumlem2  26849  dchrvmasumlem3  26850  dchrvmasumiflem1  26852  dchrvmasumiflem2  26853  dchrisum0flblem1  26859  dchrisum0flblem2  26860  dchrisum0fno1  26862  dchrisum0re  26864  dchrisum0lema  26865  dchrisum0lem1b  26866  dchrisum0lem2a  26868  dchrisum0lem2  26869  dchrisum0lem3  26870  rplogsum  26878  dirith2  26879  mudivsum  26881  mulogsumlem  26882  mulogsum  26883  mulog2sumlem1  26885  mulog2sumlem2  26886  vmalogdivsum2  26889  vmalogdivsum  26890  2vmadivsumlem  26891  log2sumbnd  26895  selberglem2  26897  selberg2lem  26901  chpdifbnd  26906  selberg3lem1  26908  selberg3  26910  selberg4lem1  26911  selberg4  26912  pntrmax  26915  pntrsumo1  26916  pntrsumbnd  26917  selberg3r  26920  selberg4r  26921  selberg34r  26922  pntrlog2bndlem1  26928  pntrlog2bndlem2  26929  pntrlog2bndlem3  26930  pntrlog2bndlem4  26931  pntrlog2bndlem5  26932  pntrlog2bndlem6  26934  pntrlog2bnd  26935  pntpbnd1a  26936  pntpbnd1  26937  pntibndlem2a  26941  pntibndlem2  26942  pntibnd  26944  pntlemc  26946  pntlemg  26949  pntlemr  26953  pntlemk  26957  pnt  26965  qabvle  26976  ostth2lem3  26986  ostth2  26988  trgcgrg  27460  tgcgr4  27476  ttgcontlem1  27836  axpaschlem  27892  axlowdimlem16  27909  axcontlem2  27917  axcontlem7  27922  nbusgrvtxm1  28330  upgrewlkle2  28557  pthdlem1  28717  crctcshwlkn0lem3  28760  crctcshwlkn0lem5  28762  wwlksm1edg  28829  wwlksnextproplem2  28858  clwlkclwwlklem2fv1  28942  clwlkclwwlklem2fv2  28943  clwlkclwwlklem2  28947  clwlkclwwlk2  28950  clwwisshclwwslem  28961  clwwlkf1  28996  clwwlkext2edg  29003  clwlknf1oclwwlknlem1  29028  clwwlknonex2lem2  29055  numclwwlk7  29338  frgrreggt1  29340  frgrogt3nreg  29344  smcnlem  29642  nmoub3i  29718  blocnilem  29749  ubthlem2  29816  minvecolem4  29825  htthlem  29862  nmcexi  30971  nmopcoi  31040  stadd3i  31193  cdj1i  31378  nnmulge  31658  nndiffz1  31692  fzsplit3  31700  wrdt2ind  31810  pmtrto1cl  31951  fzto1st1  31954  fzto1st  31955  psgnfzto1st  31957  cycpmco2lem6  31983  cycpmco2lem7  31984  cycpmrn  31995  qsidomlem1  32228  krull  32243  1smat1  32388  submateqlem1  32391  madjusmdetlem2  32412  unitdivcld  32485  sqsscirc1  32492  nexple  32611  indf1o  32626  esumdivc  32685  dya2ub  32873  dya2iocress  32877  dya2iocbrsiga  32878  dya2icobrsiga  32879  dya2icoseg  32880  dya2iocucvr  32887  sxbrsigalem2  32889  fibp1  33004  probmeasb  33033  dstrvprob  33074  dstfrvunirn  33077  ballotlemfc0  33095  ballotlemfcc  33096  ballotlemsgt1  33113  ballotlemsel1i  33115  ballotlemfrcn0  33132  signsply0  33166  itgexpif  33222  reprlt  33235  chtvalz  33245  breprexplemc  33248  breprexp  33249  circlemeth  33256  tgoldbachgnn  33275  acycgr1v  33746  subfaclim  33785  cvmliftlem2  33883  cvmliftlem13  33893  snmlff  33926  bccolsum  34315  faclim  34322  nn0prpwlem  34797  dnibndlem10  34953  dnibndlem12  34955  knoppcnlem4  34962  unblimceq0  34973  knoppndvlem1  34978  knoppndvlem2  34979  knoppndvlem3  34980  knoppndvlem7  34984  knoppndvlem11  34988  knoppndvlem12  34989  knoppndvlem14  34991  knoppndvlem15  34992  knoppndvlem17  34994  knoppndvlem18  34995  knoppndvlem20  34997  irrdiff  35800  poimirlem6  36087  poimirlem7  36088  poimirlem15  36096  poimirlem19  36100  poimirlem29  36110  poimirlem30  36111  poimirlem31  36112  poimirlem32  36113  broucube  36115  itg2addnclem2  36133  itg2addnclem3  36134  areacirclem1  36169  areacirclem4  36172  incsequz  36210  totbndbnd  36251  bfplem2  36285  resdvopclptsd  40488  lcmineqlem2  40490  lcmineqlem3  40491  lcmineqlem10  40498  lcmineqlem12  40500  lcmineqlem15  40503  lcmineqlem18  40506  lcmineqlem19  40507  lcmineqlem20  40508  lcmineqlem22  40510  lcmineqlem23  40511  3lexlogpow5ineq2  40515  3lexlogpow5ineq4  40516  3lexlogpow5ineq3  40517  3lexlogpow2ineq1  40518  3lexlogpow2ineq2  40519  3lexlogpow5ineq5  40520  aks4d1lem1  40522  dvrelog2  40524  dvrelog3  40525  dvrelog2b  40526  dvrelogpow2b  40528  aks4d1p1p3  40529  aks4d1p1p2  40530  aks4d1p1p4  40531  aks4d1p1p6  40533  aks4d1p1p7  40534  aks4d1p1p5  40535  aks4d1p1  40536  aks4d1p2  40537  aks4d1p3  40538  aks4d1p5  40540  aks4d1p6  40541  aks4d1p7d1  40542  aks4d1p7  40543  aks4d1p8d2  40545  aks4d1p8d3  40546  aks4d1p8  40547  aks4d1p9  40548  aks6d1c2p2  40552  2np3bcnp1  40555  2ap1caineq  40556  sticksstones6  40562  sticksstones7  40563  sticksstones10  40566  sticksstones12a  40568  sticksstones12  40569  sticksstones22  40579  metakunt1  40580  metakunt2  40581  metakunt7  40586  metakunt15  40594  metakunt16  40595  metakunt24  40603  metakunt28  40607  metakunt29  40608  2xp3dxp2ge1d  40617  factwoffsmonot  40618  sn-1ne2  40784  rtprmirr  40836  sn-00idlem2  40871  sn-0ne2  40878  rei4  40895  sn-0tie0  40911  sn-nnne0  40920  mulgt0b2d  40932  sn-0lt1  40934  flt4lem7  41000  fltnlta  41004  3cubeslem1  41010  3cubeslem3r  41013  3cubeslem4  41015  lzenom  41096  irrapxlem1  41148  irrapxlem2  41149  irrapxlem4  41151  irrapxlem5  41152  pellexlem2  41156  pell1qrge1  41196  pell1qr1  41197  elpell1qr2  41198  pell14qrgapw  41202  pellfundgt1  41209  pellfundglb  41211  pellfundex  41212  pellfundrp  41214  pellfundne1  41215  rmspecsqrtnq  41232  rmspecnonsq  41233  rmspecfund  41235  rmspecpos  41243  monotoddzzfi  41269  rmygeid  41291  areaquad  41553  imo72b2lem0  42445  imo72b2lem1  42449  imo72b2  42452  cvgdvgrat  42600  radcnvrat  42601  hashnzfzclim  42609  lhe4.4ex1a  42616  binomcxplemnn0  42636  binomcxplemdvbinom  42640  binomcxplemnotnn0  42643  oddfl  43518  abscosbd  43519  zltlesub  43526  abssinbd  43536  monoords  43538  fzisoeu  43541  fzdifsuc2  43551  suplesup  43580  xralrple2  43595  infxr  43608  infleinflem2  43612  reclt0d  43628  xrralrecnnge  43632  sqrlearg  43798  iooiinioc  43801  fmul01  43828  fmul01lt1lem1  43832  fmul01lt1lem2  43833  climsuselem1  43855  sumnnodd  43878  0ellimcdiv  43897  dvmptidg  44165  dvcosax  44174  ioodvbdlimc1lem1  44179  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  dvxpaek  44188  dvnmul  44191  iblspltprt  44221  itgspltprt  44227  stoweidlem5  44253  stoweidlem7  44255  stoweidlem10  44258  stoweidlem11  44259  stoweidlem12  44260  stoweidlem13  44261  stoweidlem14  44262  stoweidlem16  44264  stoweidlem18  44266  stoweidlem20  44268  stoweidlem24  44272  stoweidlem25  44273  stoweidlem34  44282  stoweidlem36  44284  stoweidlem38  44286  stoweidlem40  44288  stoweidlem41  44289  stoweidlem42  44290  stoweidlem45  44293  stoweidlem51  44299  stoweidlem60  44308  wallispilem3  44315  wallispilem4  44316  wallispilem5  44317  wallispi  44318  wallispi2lem1  44319  wallispi2lem2  44320  wallispi2  44321  stirlinglem1  44322  stirlinglem3  44324  stirlinglem5  44326  stirlinglem6  44327  stirlinglem7  44328  stirlinglem8  44329  stirlinglem10  44331  stirlinglem11  44332  stirlinglem12  44333  stirlinglem13  44334  stirlinglem15  44336  dirker2re  44340  dirkerval2  44342  dirkerre  44343  dirkertrigeqlem1  44346  dirkertrigeqlem3  44348  dirkeritg  44350  dirkercncflem1  44351  dirkercncflem2  44352  dirkercncflem4  44354  fourierdlem5  44360  fourierdlem6  44361  fourierdlem11  44366  fourierdlem15  44370  fourierdlem19  44374  fourierdlem20  44375  fourierdlem24  44379  fourierdlem26  44381  fourierdlem28  44383  fourierdlem30  44385  fourierdlem39  44394  fourierdlem41  44396  fourierdlem43  44398  fourierdlem47  44401  fourierdlem48  44402  fourierdlem56  44410  fourierdlem60  44414  fourierdlem61  44415  fourierdlem62  44416  fourierdlem64  44418  fourierdlem65  44419  fourierdlem66  44420  fourierdlem68  44422  fourierdlem73  44427  fourierdlem78  44432  fourierdlem79  44433  fourierdlem87  44441  fourierdlem103  44457  fourierdlem104  44458  sqwvfoura  44476  fouriersw  44479  etransclem4  44486  etransclem23  44505  etransclem24  44506  etransclem31  44513  etransclem32  44514  etransclem35  44517  etransclem41  44523  etransclem46  44528  etransclem48  44530  etransc  44531  ioorrnopnxrlem  44554  nnfoctbdjlem  44703  iundjiun  44708  hoidmvlelem1  44843  hoidmvlelem2  44844  hoidmvlelem3  44845  hoidmvlelem4  44846  ovnhoilem1  44849  vonioolem2  44929  vonicclem2  44932  pimrecltneg  44972  smfrec  45037  smfmullem1  45039  smfmullem2  45040  smfdiv  45045  sigaradd  45114  p1lep2  45539  zm1nn  45541  m1mod0mod1  45568  iccpartiltu  45621  iccpartlt  45623  iccpartgt  45626  fmtnoge3  45729  fmtnodvds  45743  fmtnoprmfac2lem1  45765  2pwp1prm  45788  flsqrt  45792  sfprmdvdsmersenne  45802  lighneallem2  45805  lighneallem4a  45807  proththdlem  45812  proththd  45813  nnoALTV  45894  bgoldbtbndlem4  46007  cznnring  46261  divge1b  46600  divgt1b  46601  m1modmmod  46614  difmodm1lt  46615  nn0eo  46621  regt1loggt0  46629  rege1logbrege0  46651  logblt1b  46657  fllog2  46661  nnolog2flm1  46683  dignn0flhalflem1  46708  rrxlinesc  46828  rrxlinec  46829  eenglngeehlnmlem1  46830  eenglngeehlnmlem2  46831  line2ylem  46844  line2  46845  line2xlem  46846  reseccl  47205  recsccl  47206  amgmwlem  47256  amgmlemALT  47257
  Copyright terms: Public domain W3C validator