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

Theorem 1red 9600
Description: 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
1red  |-  ( ph  ->  1  e.  RR )

Proof of Theorem 1red
StepHypRef Expression
1 1re 9584 . 2  |-  1  e.  RR
21a1i 11 1  |-  ( ph  ->  1  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1762   RRcr 9480   1c1 9482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-mulcl 9543  ax-mulrcl 9544  ax-i2m1 9549  ax-1ne0 9550  ax-rrecex 9553  ax-cnre 9554
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-iota 5542  df-fv 5587  df-ov 6278
This theorem is referenced by:  recgt0  10375  ltrec  10415  nn0p1gt0  10814  nn0ge2m1nn  10850  suprzcl  10929  qbtwnre  11387  xov1plusxeqvd  11655  elfz1b  11737  elfznelfzo  11872  elfznelfzob  11873  fladdz  11914  flhalf  11918  ltdifltdiv  11922  modltm1p1mod  11995  ltexp2a  12172  expcan  12173  ltexp2  12174  leexp2  12175  leexp2a  12176  leexp2r  12178  nnlesq  12226  bernneq3  12249  expnbnd  12250  expnlbnd2  12252  fzsdom2  12438  brfi1uzind  12485  wrdlenge2n0  12529  lswccatn0lsw  12558  ccatws1n0  12586  swrdn0  12605  swrd2lsw  12840  2swrd2eqwrdeq  12841  rddif  13122  rlimo1  13388  o1fsum  13576  abscvgcvg  13582  climcndslem1  13613  flo1  13618  harmonic  13622  geomulcvg  13637  efcllem  13664  efgt1  13701  tanhlt1  13745  sinltx  13774  eirrlem  13787  bitsfzo  13933  bitscmp  13936  smuval2  13980  prmind2  14076  isprm5  14101  divdenle  14130  zsqrelqelz  14139  fermltl  14162  odzdvds  14170  modprm0  14178  iserodd  14207  pcfaclem  14265  prmreclem1  14282  4sqlem11  14321  4sqlem12  14322  ramub1lem1  14392  2expltfac  14424  pgpfaclem2  16916  znidomb  18360  chfacfisf  19115  chfacfisfcpmat  19116  chfacfscmulgsum  19121  chfacfpmmulgsum  19125  nrginvrcnlem  20927  nmoid  20977  xrsmopn  21045  metnrmlem1a  21090  iccpnfhmeo  21173  htpycc  21208  pcohtpylem  21247  pcoass  21252  pcorevlem  21254  nmhmcn  21331  cncmet  21489  ovoliunlem1  21641  dyadmaxlem  21734  vitalilem2  21746  mbfi1fseqlem6  21855  itg2mulc  21882  itg2monolem1  21885  itg2monolem3  21887  dveflem  22108  mvth  22121  dvlipcn  22123  lhop1lem  22142  dvfsumlem1  22155  dvfsumlem2  22156  dvfsumlem3  22157  dvfsumlem4  22158  dvfsum2  22163  fta1glem2  22295  plyeq0lem  22335  fta1lem  22430  vieta1lem2  22434  aalioulem3  22457  aalioulem4  22458  radcnvlem1  22535  radcnvlem2  22536  dvradcnv  22543  abelthlem5  22557  abelthlem7  22560  abelth2  22564  cosne0  22643  rplogcl  22710  logdivlti  22726  logno1  22738  advlog  22756  logtayllem  22761  cxplt  22796  cxple  22797  cxpaddlelem  22846  cxpaddle  22847  isosctrlem1  22873  isosctrlem2  22874  heron  22890  atanlogaddlem  22965  bndatandm  22981  leibpi  22994  log2tlbnd  22997  birthdaylem3  23004  rlimcnp  23016  rlimcnp2  23017  efrlim  23020  cxp2limlem  23026  divsqrsumo1  23034  jensenlem2  23038  logdiflbnd  23045  fsumharmonic  23062  wilthlem2  23064  ftalem2  23068  basellem9  23083  vma1  23161  ppieq0  23171  mumullem2  23175  fsumfldivdiaglem  23186  chpeq0  23204  chtub  23208  chpval2  23214  chpchtsum  23215  chpub  23216  logfacrlim  23220  logexprlim  23221  mersenne  23223  dchrelbas4  23239  bposlem1  23280  bposlem2  23281  lgslem3  23294  lgslem4  23295  lgsmod  23317  lgsdir2lem4  23322  lgsdirprm  23325  lgsquadlem2  23351  2sqlem8  23368  chebbnd1lem1  23375  chebbnd1lem2  23376  chtppilimlem1  23379  chebbnd2  23383  chto1lb  23384  chpchtlim  23385  chpo1ubb  23387  vmadivsum  23388  rplogsumlem1  23390  rpvmasumlem  23393  dchrisumlem3  23397  dchrmusumlema  23399  dchrmusum2  23400  dchrvmasumlem2  23404  dchrvmasumlem3  23405  dchrvmasumiflem1  23407  dchrvmasumiflem2  23408  dchrisum0flblem1  23414  dchrisum0fno1  23417  dchrisum0re  23419  dchrisum0lema  23420  dchrisum0lem2a  23423  dchrisum0lem2  23424  dchrisum0lem3  23425  rplogsum  23433  dirith2  23434  mudivsum  23436  mulogsumlem  23437  mulogsum  23438  mulog2sumlem1  23440  mulog2sumlem2  23441  vmalogdivsum2  23444  vmalogdivsum  23445  2vmadivsumlem  23446  log2sumbnd  23450  selberglem2  23452  selberg2lem  23456  chpdifbnd  23461  selberg3lem1  23463  selberg3  23465  selberg4lem1  23466  selberg4  23467  pntrmax  23470  pntrsumo1  23471  pntrsumbnd  23472  selberg3r  23475  selberg4r  23476  selberg34r  23477  pntrlog2bndlem1  23483  pntrlog2bndlem2  23484  pntrlog2bndlem3  23485  pntrlog2bndlem4  23486  pntrlog2bndlem5  23487  pntrlog2bndlem6  23489  pntrlog2bnd  23490  pntpbnd1  23492  pntibndlem2a  23496  pntibndlem2  23497  pntibnd  23499  pntlemc  23501  pntlemg  23504  pntlemr  23508  pntlemk  23512  qabvle  23531  ostth2lem3  23541  ostth2  23543  ttgcontlem1  23857  wwlkm1edg  24397  clwlkisclwwlklem1  24449  usg2cwwkdifex  24483  frgrareggt1  24779  frgraregord013  24781  frgraogt3nreg  24783  smcnlem  25269  nmoub3i  25350  blocnilem  25381  ubthlem2  25449  minvecolem4  25458  htthlem  25496  nmcexi  26607  nmopcoi  26676  cdj1i  27014  fibp1  27966  areaquad  30778  sumnnodd  31127  dvcosax  31211  ioodvbdlimc1lem1  31216  ioodvbdlimc1lem2  31217  ioodvbdlimc2lem  31219  stoweidlem5  31260  stoweidlem7  31262  stoweidlem10  31265  stoweidlem11  31266  stoweidlem12  31267  stoweidlem13  31268  stoweidlem14  31269  stoweidlem16  31271  stoweidlem18  31273  stoweidlem20  31275  stoweidlem24  31279  stoweidlem25  31280  stoweidlem34  31289  stoweidlem36  31291  stoweidlem38  31293  stoweidlem40  31295  stoweidlem41  31296  stoweidlem42  31297  stoweidlem45  31300  stoweidlem51  31306  stoweidlem60  31315  fourierdlem6  31368  fourierdlem19  31381  fourierdlem41  31403  fourierdlem45  31407  fourierdlem48  31410  sqwvfoura  31484  nn0le2is012  31896
  Copyright terms: Public domain W3C validator