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

Theorem 1red 9393
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 9377 . 2  |-  1  e.  RR
21a1i 11 1  |-  ( ph  ->  1  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756   RRcr 9273   1c1 9275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-mulcl 9336  ax-mulrcl 9337  ax-i2m1 9342  ax-1ne0 9343  ax-rrecex 9346  ax-cnre 9347
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-rab 2718  df-v 2968  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-br 4286  df-iota 5374  df-fv 5419  df-ov 6089
This theorem is referenced by:  recgt0  10165  ltrec  10205  nn0p1gt0  10601  suprzcl  10713  qbtwnre  11161  xov1plusxeqvd  11423  elfz1b  11519  elfznelfzo  11622  elfznelfzob  11623  fladdz  11662  flhalf  11666  ltdifltdiv  11670  modltm1p1mod  11743  ltexp2a  11907  expcan  11908  ltexp2  11909  leexp2  11910  leexp2a  11911  leexp2r  11913  nnlesq  11961  bernneq3  11984  expnbnd  11985  expnlbnd2  11987  fzsdom2  12181  brfi1uzind  12211  wrdlenge2n0  12253  lswccatn0lsw  12279  ccatws1n0  12302  swrdn0  12316  swrd2lsw  12544  2swrd2eqwrdeq  12545  rddif  12820  rlimo1  13086  o1fsum  13268  abscvgcvg  13274  climcndslem1  13304  flo1  13309  harmonic  13313  geomulcvg  13328  efcllem  13355  efgt1  13392  tanhlt1  13436  sinltx  13465  eirrlem  13478  bitsfzo  13623  bitscmp  13626  smuval2  13670  prmind2  13766  isprm5  13790  divdenle  13819  zsqrelqelz  13828  fermltl  13851  odzdvds  13859  modprm0  13865  iserodd  13894  pcfaclem  13952  prmreclem1  13969  4sqlem11  14008  4sqlem12  14009  ramub1lem1  14079  2expltfac  14111  pgpfaclem2  16569  znidomb  17963  nrginvrcnlem  20240  nmoid  20290  xrsmopn  20358  metnrmlem1a  20403  iccpnfhmeo  20486  htpycc  20521  pcohtpylem  20560  pcoass  20565  pcorevlem  20567  nmhmcn  20644  cncmet  20802  ovoliunlem1  20954  dyadmaxlem  21046  vitalilem2  21058  mbfi1fseqlem6  21167  itg2mulc  21194  itg2monolem1  21197  itg2monolem3  21199  dveflem  21420  mvth  21433  dvlipcn  21435  lhop1lem  21454  dvfsumlem1  21467  dvfsumlem2  21468  dvfsumlem3  21469  dvfsumlem4  21470  dvfsum2  21475  fta1glem2  21607  plyeq0lem  21647  fta1lem  21742  vieta1lem2  21746  aalioulem3  21769  aalioulem4  21770  radcnvlem1  21847  radcnvlem2  21848  dvradcnv  21855  abelthlem5  21869  abelthlem7  21872  abelth2  21876  cosne0  21955  rplogcl  22022  logdivlti  22038  logno1  22050  advlog  22068  logtayllem  22073  cxplt  22108  cxple  22109  cxpaddlelem  22158  cxpaddle  22159  isosctrlem1  22185  isosctrlem2  22186  heron  22202  atanlogaddlem  22277  bndatandm  22293  leibpi  22306  log2tlbnd  22309  birthdaylem3  22316  rlimcnp  22328  rlimcnp2  22329  efrlim  22332  cxp2limlem  22338  divsqrsumo1  22346  jensenlem2  22350  logdiflbnd  22357  fsumharmonic  22374  wilthlem2  22376  ftalem2  22380  basellem9  22395  vma1  22473  ppieq0  22483  mumullem2  22487  fsumfldivdiaglem  22498  chpeq0  22516  chtub  22520  chpval2  22526  chpchtsum  22527  chpub  22528  logfacrlim  22532  logexprlim  22533  mersenne  22535  dchrelbas4  22551  bposlem1  22592  bposlem2  22593  lgslem3  22606  lgslem4  22607  lgsmod  22629  lgsdir2lem4  22634  lgsdirprm  22637  lgsquadlem2  22663  2sqlem8  22680  chebbnd1lem1  22687  chebbnd1lem2  22688  chtppilimlem1  22691  chebbnd2  22695  chto1lb  22696  chpchtlim  22697  chpo1ubb  22699  vmadivsum  22700  rplogsumlem1  22702  rpvmasumlem  22705  dchrisumlem3  22709  dchrmusumlema  22711  dchrmusum2  22712  dchrvmasumlem2  22716  dchrvmasumlem3  22717  dchrvmasumiflem1  22719  dchrvmasumiflem2  22720  dchrisum0flblem1  22726  dchrisum0fno1  22729  dchrisum0re  22731  dchrisum0lema  22732  dchrisum0lem2a  22735  dchrisum0lem2  22736  dchrisum0lem3  22737  rplogsum  22745  dirith2  22746  mudivsum  22748  mulogsumlem  22749  mulogsum  22750  mulog2sumlem1  22752  mulog2sumlem2  22753  vmalogdivsum2  22756  vmalogdivsum  22757  2vmadivsumlem  22758  log2sumbnd  22762  selberglem2  22764  selberg2lem  22768  chpdifbnd  22773  selberg3lem1  22775  selberg3  22777  selberg4lem1  22778  selberg4  22779  pntrmax  22782  pntrsumo1  22783  pntrsumbnd  22784  selberg3r  22787  selberg4r  22788  selberg34r  22789  pntrlog2bndlem1  22795  pntrlog2bndlem2  22796  pntrlog2bndlem3  22797  pntrlog2bndlem4  22798  pntrlog2bndlem5  22799  pntrlog2bndlem6  22801  pntrlog2bnd  22802  pntpbnd1  22804  pntibndlem2a  22808  pntibndlem2  22809  pntibnd  22811  pntlemc  22813  pntlemg  22816  pntlemr  22820  pntlemk  22824  qabvle  22843  ostth2lem3  22853  ostth2  22855  ttgcontlem1  23076  smcnlem  24037  nmoub3i  24118  blocnilem  24149  ubthlem2  24217  minvecolem4  24226  htthlem  24264  nmcexi  25375  nmopcoi  25444  cdj1i  25782  fibp1  26732  areaquad  29535  stoweidlem5  29743  stoweidlem7  29745  stoweidlem10  29748  stoweidlem11  29749  stoweidlem12  29750  stoweidlem13  29751  stoweidlem14  29752  stoweidlem16  29754  stoweidlem18  29756  stoweidlem20  29758  stoweidlem24  29762  stoweidlem25  29763  stoweidlem34  29772  stoweidlem36  29774  stoweidlem38  29776  stoweidlem40  29778  stoweidlem41  29779  stoweidlem42  29780  stoweidlem45  29783  stoweidlem51  29789  stoweidlem60  29798  frgrareggt1  30652  frgraregord013  30654  frgraogt3nreg  30656  nn0le2is012  30701
  Copyright terms: Public domain W3C validator