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

Theorem 1red 9657
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 9641 . 2  |-  1  e.  RR
21a1i 11 1  |-  ( ph  ->  1  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   RRcr 9537   1c1 9539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-1cn 9596  ax-icn 9597  ax-addcl 9598  ax-mulcl 9600  ax-mulrcl 9601  ax-i2m1 9606  ax-1ne0 9607  ax-rrecex 9610  ax-cnre 9611
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-iota 5565  df-fv 5609  df-ov 6308
This theorem is referenced by:  recgt0  10448  ltrec  10487  nn0p1gt0  10899  nn0ge2m1nn  10934  suprzcl  11015  qbtwnre  11492  iccf1o  11774  xov1plusxeqvd  11776  fznatpl1  11848  elfz1b  11862  fzonn0p1p1  11989  elfzom1p1elfzo  11990  elfznelfzo  12011  elfznelfzob  12012  fladdz  12055  flhalf  12059  ltdifltdiv  12063  modltm1p1mod  12139  ltexp2a  12321  expcan  12322  ltexp2  12323  leexp2  12324  leexp2a  12325  leexp2r  12327  nnlesq  12375  bernneq3  12397  expnbnd  12398  expnlbnd2  12400  fzsdom2  12595  wrdlenge2n0  12690  swrd2lsw  13006  2swrd2eqwrdeq  13007  rddif  13382  reccn2  13638  rlimo1  13658  o1fsum  13851  abscvgcvg  13857  climcndslem1  13885  flo1  13890  harmonic  13895  geomulcvg  13910  fprodrecl  13985  fprodle  14028  bpoly4  14090  efcllem  14110  efgt1  14148  tanhlt1  14192  sinltx  14221  eirrlem  14234  bitsfzolem  14382  bitsfzo  14383  bitsmod  14384  bitscmp  14386  bitsinv1lem  14389  smuval2  14430  prmind2  14597  isprm5  14613  coprmgcdb  14616  divdenle  14660  zsqrtelqelz  14669  fermltl  14692  odzdvds  14700  modprm0  14710  iserodd  14739  pcfaclem  14797  prmreclem1  14814  4sqlem11  14853  4sqlem12  14854  ramub1lem1  14938  prmgaplem8  14982  2expltfac  15017  pgpfaclem2  17641  znidomb  19054  chfacfisf  19800  chfacfisfcpmat  19801  chfacfscmulgsum  19806  chfacfpmmulgsum  19810  nrginvrcnlem  21615  nmoid  21665  xrsmopn  21732  metnrmlem1a  21777  iccpnfhmeo  21860  htpycc  21895  pcohtpylem  21934  pcoass  21939  pcorevlem  21941  nmhmcn  22018  cncmet  22174  ovoliunlem1  22324  dyadmaxlem  22423  vitalilem2  22435  mbfi1fseqlem6  22546  itg2mulc  22573  itg2monolem1  22576  itg2monolem3  22578  dveflem  22799  mvth  22812  dvlipcn  22814  lhop1lem  22833  dvfsumlem1  22846  dvfsumlem2  22847  dvfsumlem3  22848  dvfsumlem4  22849  dvfsum2  22854  fta1glem2  22983  plyeq0lem  23023  fta1lem  23119  vieta1lem2  23123  aalioulem3  23146  aalioulem4  23147  radcnvlem1  23224  radcnvlem2  23225  dvradcnv  23232  abelthlem2  23243  abelthlem5  23246  abelthlem7  23249  abelth2  23253  cosne0  23335  rplogcl  23409  logdivlti  23425  logno1  23437  advlog  23455  logtayllem  23460  cxplt  23495  cxple  23496  cxpaddlelem  23547  cxpaddle  23548  relogbf  23584  isosctrlem1  23603  isosctrlem2  23604  heron  23620  atanlogaddlem  23695  bndatandm  23711  leibpi  23724  log2tlbnd  23727  birthdaylem3  23735  rlimcnp  23747  rlimcnp2  23748  efrlim  23751  cxp2limlem  23757  divsqrtsumo1  23765  jensenlem2  23769  logdiflbnd  23776  fsumharmonic  23793  lgamgulmlem2  23811  lgamgulmlem3  23812  lgamgulmlem4  23813  lgamgulmlem5  23814  lgamgulmlem6  23815  lgamcvg2  23836  regamcl  23842  wilthlem2  23850  ftalem2  23854  basellem9  23869  vma1  23947  ppieq0  23957  mumullem2  23961  fsumfldivdiaglem  23972  chpeq0  23990  chtub  23994  chpval2  24000  chpchtsum  24001  chpub  24002  logfacrlim  24006  logexprlim  24007  mersenne  24009  dchrelbas4  24025  bcmono  24059  bposlem1  24066  bposlem2  24067  lgslem3  24080  lgslem4  24081  lgsmod  24103  lgsdir2lem4  24108  lgsdirprm  24111  lgsquadlem2  24137  2sqlem8  24154  chebbnd1lem1  24161  chebbnd1lem2  24162  chtppilimlem1  24165  chebbnd2  24169  chto1lb  24170  chpchtlim  24171  chpo1ubb  24173  vmadivsum  24174  rplogsumlem1  24176  rpvmasumlem  24179  dchrisumlem3  24183  dchrmusumlema  24185  dchrmusum2  24186  dchrvmasumlem2  24190  dchrvmasumlem3  24191  dchrvmasumiflem1  24193  dchrvmasumiflem2  24194  dchrisum0flblem1  24200  dchrisum0flblem2  24201  dchrisum0fno1  24203  dchrisum0re  24205  dchrisum0lema  24206  dchrisum0lem1b  24207  dchrisum0lem2a  24209  dchrisum0lem2  24210  dchrisum0lem3  24211  rplogsum  24219  dirith2  24220  mudivsum  24222  mulogsumlem  24223  mulogsum  24224  mulog2sumlem1  24226  mulog2sumlem2  24227  vmalogdivsum2  24230  vmalogdivsum  24231  2vmadivsumlem  24232  log2sumbnd  24236  selberglem2  24238  selberg2lem  24242  chpdifbnd  24247  selberg3lem1  24249  selberg3  24251  selberg4lem1  24252  selberg4  24253  pntrmax  24256  pntrsumo1  24257  pntrsumbnd  24258  selberg3r  24261  selberg4r  24262  selberg34r  24263  pntrlog2bndlem1  24269  pntrlog2bndlem2  24270  pntrlog2bndlem3  24271  pntrlog2bndlem4  24272  pntrlog2bndlem5  24273  pntrlog2bndlem6  24275  pntrlog2bnd  24276  pntpbnd1a  24277  pntpbnd1  24278  pntibndlem2a  24282  pntibndlem2  24283  pntibnd  24285  pntlemc  24287  pntlemg  24290  pntlemr  24294  pntlemk  24298  qabvle  24317  ostth2lem3  24327  ostth2  24329  trgcgrg  24413  ttgcontlem1  24752  axpaschlem  24807  axlowdimlem16  24824  axcontlem2  24832  axcontlem7  24837  wwlkm1edg  25299  wwlkextproplem1  25305  wwlkextproplem2  25306  clwlkisclwwlklem2fv1  25346  clwlkisclwwlklem2fv2  25347  clwlkisclwwlklem1  25351  clwlkisclwwlk2  25354  clwwlkf1  25360  clwwlkext2edg  25366  clwwisshclwwlem  25370  usg2cwwkdifex  25385  extwwlkfablem2  25642  numclwwlkovf2ex  25650  numclwlk1lem2f1  25658  numclwwlk7  25678  frgrareggt1  25680  frgraregord013  25682  frgraogt3nreg  25684  smcnlem  26169  nmoub3i  26250  blocnilem  26281  ubthlem2  26349  minvecolem4  26358  htthlem  26396  nmcexi  27505  nmopcoi  27574  cdj1i  27912  nn0sqeq1  28158  nndiffz1  28193  fzsplit3  28197  pmtrto1cl  28442  fzto1st1  28445  fzto1st  28446  psgnfzto1st  28448  1smat1  28460  submateqlem1  28463  madjusmdetlem2  28484  unitdivcld  28537  sqsscirc1  28544  nexple  28661  indf1o  28675  esumdivc  28734  dya2ub  28922  dya2iocress  28926  dya2iocbrsiga  28927  dya2icobrsiga  28928  dya2icoseg  28929  dya2iocucvr  28936  sxbrsigalem2  28938  fibp1  29051  probmeasb  29080  dstrvprob  29121  dstfrvunirn  29124  ballotlemfc0  29142  ballotlemfcc  29143  ballotlemsgt1  29160  ballotlemsel1i  29162  ballotlemfrcn0  29179  signsply0  29219  subfaclim  29690  cvmliftlem2  29788  cvmliftlem13  29798  snmlff  29831  bccolsum  30153  faclim  30160  nn0prpwlem  30754  poimirlem6  31640  poimirlem7  31641  poimirlem15  31649  poimirlem19  31653  poimirlem29  31663  poimirlem30  31664  poimirlem31  31665  poimirlem32  31666  broucube  31668  itg2addnclem2  31688  itg2addnclem3  31689  areacirclem1  31726  areacirclem4  31729  incsequz  31771  totbndbnd  31815  bfplem2  31849  lzenom  35311  irrapxlem1  35366  irrapxlem2  35367  irrapxlem4  35369  irrapxlem5  35370  pellexlem2  35374  pell1qrge1  35414  pell1qr1  35415  elpell1qr2  35416  pell14qrgapw  35420  pellfundgt1  35427  pellfundglb  35429  pellfundex  35430  pellfundrp  35432  pellfundne1  35433  rmspecnonsq  35451  rmspecfund  35453  rmspecpos  35460  monotoddzzfi  35486  rmygeid  35510  areaquad  35790  imo72b2lem0  36235  imo72b2lem1  36241  imo72b2  36246  isprm7  36287  cvgdvgrat  36289  radcnvrat  36290  hashnzfzclim  36298  lhe4.4ex1a  36305  binomcxplemnn0  36325  binomcxplemdvbinom  36329  binomcxplemnotnn0  36332  oddfl  37086  abscosbd  37087  zltlesub  37094  abssinbd  37111  monoords  37113  fzisoeu  37117  fzdifsuc2  37129  suplesup  37161  fmul01  37220  fmul01lt1lem1  37224  fmul01lt1lem2  37225  climsuselem1  37248  sumnnodd  37272  0ellimcdiv  37292  dvmptidg  37349  dvcosax  37360  ioodvbdlimc1lem1  37365  ioodvbdlimc1lem2  37366  ioodvbdlimc2lem  37368  dvxpaek  37374  dvnmul  37377  iblspltprt  37409  itgspltprt  37415  stoweidlem5  37424  stoweidlem7  37426  stoweidlem10  37429  stoweidlem11  37430  stoweidlem12  37431  stoweidlem13  37432  stoweidlem14  37433  stoweidlem16  37435  stoweidlem18  37437  stoweidlem20  37439  stoweidlem24  37443  stoweidlem25  37444  stoweidlem34  37454  stoweidlem36  37456  stoweidlem38  37458  stoweidlem40  37460  stoweidlem41  37461  stoweidlem42  37462  stoweidlem45  37465  stoweidlem51  37471  stoweidlem60  37480  wallispilem3  37488  wallispilem4  37489  wallispilem5  37490  wallispi  37491  wallispi2lem1  37492  wallispi2lem2  37493  wallispi2  37494  stirlinglem1  37495  stirlinglem3  37497  stirlinglem5  37499  stirlinglem6  37500  stirlinglem7  37501  stirlinglem8  37502  stirlinglem10  37504  stirlinglem11  37505  stirlinglem12  37506  stirlinglem13  37507  stirlinglem15  37509  dirker2re  37513  dirkerval2  37515  dirkerre  37516  dirkertrigeqlem1  37519  dirkertrigeqlem3  37521  dirkeritg  37523  dirkercncflem1  37524  dirkercncflem2  37525  dirkercncflem4  37527  fourierdlem5  37533  fourierdlem6  37534  fourierdlem11  37539  fourierdlem15  37543  fourierdlem19  37547  fourierdlem20  37548  fourierdlem24  37552  fourierdlem26  37554  fourierdlem28  37556  fourierdlem30  37558  fourierdlem39  37567  fourierdlem41  37569  fourierdlem43  37571  fourierdlem47  37575  fourierdlem48  37576  fourierdlem56  37584  fourierdlem60  37588  fourierdlem61  37589  fourierdlem62  37590  fourierdlem64  37592  fourierdlem65  37593  fourierdlem66  37594  fourierdlem68  37596  fourierdlem73  37601  fourierdlem78  37606  fourierdlem79  37607  fourierdlem87  37615  fourierdlem103  37631  fourierdlem104  37632  sqwvfoura  37650  fouriersw  37653  etransclem4  37660  etransclem23  37679  etransclem24  37680  etransclem31  37687  etransclem32  37688  etransclem35  37691  etransclem41  37697  etransclem46  37702  etransclem48  37704  etransc  37705  nnfoctbdjlem  37792  iundjiun  37797  sigaradd  37865  m1mod0mod1  38103  mod2eq1n2dvds  38105  iccpartiltu  38116  iccpartlt  38118  iccpartgt  38121  nnoALTV  38204  bgoldbtbndlem4  38283  proththdlem  38293  proththd  38294  pfx2  38333  p1lep2  38385  zm1nn  38388  cznnring  38706  nn0le2is012  38898  divge1b  39058  divgt1b  39059  m1modmmod  39075  difmodm1lt  39076  nn0o1gt2  39078  nno  39079  nn0eo  39086  regt1loggt0  39098  rege1logbrege0  39120  logblt1b  39126  fllog2  39130  nnolog2flm1  39152  dignn0flhalflem1  39177  reseccl  39224  recsccl  39225
  Copyright terms: Public domain W3C validator