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

Theorem 1red 9404
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 9388 . 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 9284   1c1 9286
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 2423  ax-1cn 9343  ax-icn 9344  ax-addcl 9345  ax-mulcl 9347  ax-mulrcl 9348  ax-i2m1 9353  ax-1ne0 9354  ax-rrecex 9357  ax-cnre 9358
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 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-ral 2723  df-rex 2724  df-rab 2727  df-v 2977  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-iota 5384  df-fv 5429  df-ov 6097
This theorem is referenced by:  recgt0  10176  ltrec  10216  nn0p1gt0  10612  suprzcl  10724  qbtwnre  11172  xov1plusxeqvd  11434  elfz1b  11530  elfznelfzo  11633  elfznelfzob  11634  fladdz  11673  flhalf  11677  ltdifltdiv  11681  modltm1p1mod  11754  ltexp2a  11918  expcan  11919  ltexp2  11920  leexp2  11921  leexp2a  11922  leexp2r  11924  nnlesq  11972  bernneq3  11995  expnbnd  11996  expnlbnd2  11998  fzsdom2  12192  brfi1uzind  12222  wrdlenge2n0  12264  lswccatn0lsw  12290  ccatws1n0  12313  swrdn0  12327  swrd2lsw  12555  2swrd2eqwrdeq  12556  rddif  12831  rlimo1  13097  o1fsum  13279  abscvgcvg  13285  climcndslem1  13315  flo1  13320  harmonic  13324  geomulcvg  13339  efcllem  13366  efgt1  13403  tanhlt1  13447  sinltx  13476  eirrlem  13489  bitsfzo  13634  bitscmp  13637  smuval2  13681  prmind2  13777  isprm5  13801  divdenle  13830  zsqrelqelz  13839  fermltl  13862  odzdvds  13870  modprm0  13876  iserodd  13905  pcfaclem  13963  prmreclem1  13980  4sqlem11  14019  4sqlem12  14020  ramub1lem1  14090  2expltfac  14122  pgpfaclem2  16586  znidomb  17997  nrginvrcnlem  20274  nmoid  20324  xrsmopn  20392  metnrmlem1a  20437  iccpnfhmeo  20520  htpycc  20555  pcohtpylem  20594  pcoass  20599  pcorevlem  20601  nmhmcn  20678  cncmet  20836  ovoliunlem1  20988  dyadmaxlem  21080  vitalilem2  21092  mbfi1fseqlem6  21201  itg2mulc  21228  itg2monolem1  21231  itg2monolem3  21233  dveflem  21454  mvth  21467  dvlipcn  21469  lhop1lem  21488  dvfsumlem1  21501  dvfsumlem2  21502  dvfsumlem3  21503  dvfsumlem4  21504  dvfsum2  21509  fta1glem2  21641  plyeq0lem  21681  fta1lem  21776  vieta1lem2  21780  aalioulem3  21803  aalioulem4  21804  radcnvlem1  21881  radcnvlem2  21882  dvradcnv  21889  abelthlem5  21903  abelthlem7  21906  abelth2  21910  cosne0  21989  rplogcl  22056  logdivlti  22072  logno1  22084  advlog  22102  logtayllem  22107  cxplt  22142  cxple  22143  cxpaddlelem  22192  cxpaddle  22193  isosctrlem1  22219  isosctrlem2  22220  heron  22236  atanlogaddlem  22311  bndatandm  22327  leibpi  22340  log2tlbnd  22343  birthdaylem3  22350  rlimcnp  22362  rlimcnp2  22363  efrlim  22366  cxp2limlem  22372  divsqrsumo1  22380  jensenlem2  22384  logdiflbnd  22391  fsumharmonic  22408  wilthlem2  22410  ftalem2  22414  basellem9  22429  vma1  22507  ppieq0  22517  mumullem2  22521  fsumfldivdiaglem  22532  chpeq0  22550  chtub  22554  chpval2  22560  chpchtsum  22561  chpub  22562  logfacrlim  22566  logexprlim  22567  mersenne  22569  dchrelbas4  22585  bposlem1  22626  bposlem2  22627  lgslem3  22640  lgslem4  22641  lgsmod  22663  lgsdir2lem4  22668  lgsdirprm  22671  lgsquadlem2  22697  2sqlem8  22714  chebbnd1lem1  22721  chebbnd1lem2  22722  chtppilimlem1  22725  chebbnd2  22729  chto1lb  22730  chpchtlim  22731  chpo1ubb  22733  vmadivsum  22734  rplogsumlem1  22736  rpvmasumlem  22739  dchrisumlem3  22743  dchrmusumlema  22745  dchrmusum2  22746  dchrvmasumlem2  22750  dchrvmasumlem3  22751  dchrvmasumiflem1  22753  dchrvmasumiflem2  22754  dchrisum0flblem1  22760  dchrisum0fno1  22763  dchrisum0re  22765  dchrisum0lema  22766  dchrisum0lem2a  22769  dchrisum0lem2  22770  dchrisum0lem3  22771  rplogsum  22779  dirith2  22780  mudivsum  22782  mulogsumlem  22783  mulogsum  22784  mulog2sumlem1  22786  mulog2sumlem2  22787  vmalogdivsum2  22790  vmalogdivsum  22791  2vmadivsumlem  22792  log2sumbnd  22796  selberglem2  22798  selberg2lem  22802  chpdifbnd  22807  selberg3lem1  22809  selberg3  22811  selberg4lem1  22812  selberg4  22813  pntrmax  22816  pntrsumo1  22817  pntrsumbnd  22818  selberg3r  22821  selberg4r  22822  selberg34r  22823  pntrlog2bndlem1  22829  pntrlog2bndlem2  22830  pntrlog2bndlem3  22831  pntrlog2bndlem4  22832  pntrlog2bndlem5  22833  pntrlog2bndlem6  22835  pntrlog2bnd  22836  pntpbnd1  22838  pntibndlem2a  22842  pntibndlem2  22843  pntibnd  22845  pntlemc  22847  pntlemg  22850  pntlemr  22854  pntlemk  22858  qabvle  22877  ostth2lem3  22887  ostth2  22889  ttgcontlem1  23134  smcnlem  24095  nmoub3i  24176  blocnilem  24207  ubthlem2  24275  minvecolem4  24284  htthlem  24322  nmcexi  25433  nmopcoi  25502  cdj1i  25840  fibp1  26787  areaquad  29595  stoweidlem5  29803  stoweidlem7  29805  stoweidlem10  29808  stoweidlem11  29809  stoweidlem12  29810  stoweidlem13  29811  stoweidlem14  29812  stoweidlem16  29814  stoweidlem18  29816  stoweidlem20  29818  stoweidlem24  29822  stoweidlem25  29823  stoweidlem34  29832  stoweidlem36  29834  stoweidlem38  29836  stoweidlem40  29838  stoweidlem41  29839  stoweidlem42  29840  stoweidlem45  29843  stoweidlem51  29849  stoweidlem60  29858  frgrareggt1  30712  frgraregord013  30714  frgraogt3nreg  30716  nn0le2is012  30769
  Copyright terms: Public domain W3C validator