MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0re Unicode version

Theorem 0re 9617
Description: is a real number. See also 0reALT 9940. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
Assertion
Ref Expression
0re

Proof of Theorem 0re
StepHypRef Expression
1 1re 9616 . 2
2 ax-rnegex 9584 . 2
3 readdcl 9596 . . . . 5
41, 3mpan 670 . . . 4
5 eleq1 2529 . . . 4
64, 5syl5ibcom 220 . . 3
76rexlimiv 2943 . 2
81, 2, 7mp2b 10 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  e.wcel 1818  E.wrex 2808  (class class class)co 6296   cr 9512  0cc0 9513  1c1 9514   caddc 9516
This theorem is referenced by:  0red  9618  0xr  9661  axmulgt0  9680  ne0gt0  9710  00id  9776  mul02lem1  9777  mul02lem2  9778  mul02  9779  addid1  9781  addgt0  10063  addgegt0  10064  addgtge0  10065  addge0  10066  ltaddpos  10067  ltneg  10077  leneg  10080  lt0neg1  10083  lt0neg2  10084  le0neg1  10085  le0neg2  10086  addge01  10087  suble0  10091  mulge0  10095  msqge0  10099  0le1  10101  relin01  10102  gt0ne0i  10113  gt0ne0d  10142  lt0ne0d  10143  elimge0  10404  ltm1  10407  recgt0  10411  prodgt0  10412  lemul1a  10421  ltmul12a  10423  lemul12a  10425  mulgt1  10426  gt0div  10433  ge0div  10434  mulge0b  10437  lediv12a  10463  recgt1i  10467  recreclt  10469  ledivp1  10472  squeeze0  10473  recgt0ii  10476  ledivp1i  10496  ltdivp1i  10497  fimaxre2  10516  inelr  10551  crne0  10554  nnge1  10587  nngt0  10590  nnrecgt0  10598  0le0  10650  neg1lt0  10667  nn0ssre  10824  nn0ge0  10846  nn0nlt0  10847  nn0le0eq0  10849  0mnnnnn0  10853  elnnnn0b  10865  elnnnn0c  10866  nn0sub  10871  elnnz  10899  0z  10900  elnn0z  10902  elnnz1  10915  nn0lt10bOLD  10951  recnz  10963  gtndiv  10965  uzindOLD  10982  fnn0ind  10988  rpge0  11261  rpneg  11278  0nrp  11279  0ltpnf  11361  mnflt0  11363  qsqueeze  11429  xneg0  11440  xaddid1  11467  xmulpnf1  11495  xlemul1a  11509  xadddi  11516  xrsupsslem  11527  xrinfmsslem  11528  elrege0  11656  0e0icopnf  11659  0elunit  11667  1elunit  11668  divelunit  11691  lincmb01cmp  11692  iccf1o  11693  unitssre  11696  fzpreddisj  11758  rpsup  11993  0mod  12027  1mod  12028  expubnd  12226  le2sq2  12243  sqlecan  12274  bernneq2  12293  expnbnd  12295  expnlbnd  12296  expmulnbnd  12298  discr1  12302  discr  12303  facdiv  12365  faclbnd  12368  faclbnd3  12370  faclbnd6  12377  bcval4  12385  bcval5  12396  bcpasc  12399  hasheq0  12433  hashneq0  12434  hashnn0n0nn  12458  hashgt12el  12481  hashgt12el2  12482  hashge2el2dif  12521  wrdsymb0  12575  reim0  12951  re0  12985  im0  12986  rei  12989  imi  12990  cj0  12991  sqeqd  12999  rennim  13072  cnpart  13073  sqr0lem  13074  sqrlem4  13079  resqrex  13084  sqrtgt0  13092  sqrt00  13097  sqrtneglem  13100  sqrt9  13107  sqrt2gt1lt2  13108  leabs  13132  absor  13133  max0add  13143  eqsqrt2d  13201  sqrtpclii  13215  rlimconst  13367  rlimrege0  13402  lo1mul  13450  iserge0  13483  fsum00  13612  isumless  13657  arisum2  13672  georeclim  13681  geo2sum  13682  geo2lim  13684  geoisumr  13687  0.999...  13690  cvgrat  13692  cos0  13885  ef01bndlem  13919  sin01bnd  13920  cos01bnd  13921  cos2bnd  13923  sin01gt0  13925  cos01gt0  13926  sincos2sgn  13929  sin4lt0  13930  absef  13932  absefib  13933  efieq1re  13934  epos  13940  znnenlem  13945  rpnnen2lem2  13949  rpnnen2lem3  13950  rpnnen2lem4  13951  rpnnen2lem9  13956  rpnnen2  13959  ruclem6  13968  dvdslelem  14030  divalglem1  14052  divalglem5  14055  divalglem6  14056  bitsp1o  14083  sadcadd  14108  gcdn0gt0  14160  nn0seqcvgd  14199  algcvgblem  14206  algcvga  14208  pythagtriplem12  14350  pythagtriplem13  14351  pythagtriplem14  14352  pythagtriplem16  14354  prmreclem4  14437  prmreclem5  14438  prmreclem6  14439  1arith  14445  vdwap0  14494  ramz  14543  mulgnegnn  16152  subgmulg  16215  srgbinomlem4  17194  isabvd  17469  abvtrivd  17489  psrbaglesupp  18017  psrbaglesuppOLD  18018  xrs1mnd  18456  xrs10  18457  rge0srg  18487  re0g  18648  mnfnei  19722  imasdsf1olem  20876  ssblps  20925  ssbl  20926  xmeter  20936  metustexhalfOLD  21066  dscmet  21093  dscopn  21094  nmoi  21235  nmoeq0  21243  0nghm  21248  idnghm  21250  cnbl0  21281  blcvx  21303  xrsxmet  21314  metdseq0  21358  iicmp  21390  iicon  21391  iirev  21429  iihalf1  21431  iihalf1cn  21432  iihalf2  21433  elii1  21435  elii2  21436  iimulcl  21437  icopnfcnv  21442  icopnfhmeo  21443  iccpnfcnv  21444  iccpnfhmeo  21445  xrhmeo  21446  xrhmph  21447  lebnumii  21466  htpycc  21480  reparphti  21497  pcoval1  21513  pco0  21514  pcoval2  21516  pcocn  21517  pcohtpylem  21519  pcopt  21522  pcopt2  21523  pcoass  21524  pcorevlem  21526  reust  21813  recusp  21814  minveclem4c  21840  minveclem2  21841  minveclem3b  21843  minveclem4  21847  minveclem7  21850  pjthlem1  21852  cniccbdd  21873  ovolunnul  21911  ovoliunnul  21918  ovolicc1  21927  ovolre  21936  iccvolcl  21977  ovolioo  21978  ioovolcl  21979  ioorcl  21986  vitalilem2  22018  vitalilem4  22020  vitalilem5  22021  vitali  22022  ismbf  22037  mbfmulc2lem  22054  mbfpos  22058  mbfposr  22059  i1f0  22094  i1f1  22097  itg1addlem2  22104  itg1addlem4  22106  itg1addlem5  22107  mbfi1fseqlem4  22125  mbfi1fseqlem5  22126  mbfi1fseqlem6  22127  mbfi1flimlem  22129  xrge0f  22138  itg2ge0  22142  itg2const  22147  itg2mulc  22154  itg2splitlem  22155  itg2gt0  22167  itg2cnlem1  22168  ibl0  22193  iblrelem  22197  iblposlem  22198  iblpos  22199  iblre  22200  itgreval  22203  itgneg  22210  iblss  22211  i1fibl  22214  itgitg1  22215  itgle  22216  itgeqa  22220  itgless  22223  iblconst  22224  itgconst  22225  ibladdlem  22226  itgaddlem2  22230  iblabslem  22234  iblabsr  22236  iblmulc2  22237  itgmulc2lem2  22239  itgabs  22241  itgsplit  22242  bddmulibl  22245  dvferm1  22386  dvferm2  22388  dvferm  22389  dvlip  22394  c1lip1  22398  dveq0  22401  dv11cn  22402  dvne0  22412  ftc1lem4  22440  ply1divex  22537  dgrco  22672  plyrecj  22676  vieta1lem2  22707  aalioulem2  22729  aalioulem3  22730  pserulm  22817  psercnlem2  22819  psercnlem1  22820  psercn  22821  abelthlem6  22831  abelth  22836  abelth2  22837  reeff1olem  22841  reeff1o  22842  pilem2  22847  pilem3  22848  pipos  22853  sinhalfpilem  22856  sincosq1sgn  22891  sincosq2sgn  22892  coseq00topi  22895  coseq0negpitopi  22896  tangtx  22898  tanabsge  22899  sinq12ge0  22901  sinq34lt0t  22902  cosq14ge0  22904  sincos4thpi  22906  sincos6thpi  22908  pige3  22910  sineq0  22914  cosordlem  22918  cosord  22919  cos11  22920  sinord  22921  recosf1o  22922  resinf1o  22923  tanord1  22924  tanord  22925  tanregt0  22926  efif1olem4  22932  efifo  22934  relogrn  22949  log1  22970  logneg  22972  argregt0  22995  argrege0  22996  argimgt0  22997  logneg2  23000  logdivlti  23005  logdivlt  23006  ellogdm  23020  logdmn0  23021  logdmnrp  23022  logcnlem3  23025  dvloglem  23029  logdmopn  23030  logf1o2  23031  dvlog2lem  23033  efopnlem1  23037  logtayl  23041  recxpcl  23056  cxpge0  23064  cxple2  23078  cxple2a  23080  cxpsqrtlem  23083  cxpcn3  23122  cxpaddlelem  23125  cxpaddle  23126  loglesqrt  23132  ang180lem3  23143  ang180lem4  23144  chordthmlem4  23166  heron  23169  asinneg  23217  asin1  23225  reasinsin  23227  acosbnd  23231  atan0  23239  atanrecl  23242  atanlogaddlem  23244  atanlogsublem  23246  atanlogsub  23247  atantan  23254  atanbnd  23257  atan1  23259  atans2  23262  ressatans  23265  leibpi  23273  log2cnv  23275  log2tlbnd  23276  log2ublem3  23279  log2ub  23280  rlimcnp  23295  rlimcnp2  23296  o1cxp  23304  jensenlem2  23317  jensen  23318  amgm  23320  emgt0  23336  harmonicbnd3  23337  harmoniclbnd  23338  harmonicbnd4  23340  basellem3  23356  basellem8  23361  efnnfsumcl  23376  ppisval  23377  vmage0  23395  chpge0  23400  efchtdvds  23433  ppiltx  23451  ppiub  23479  chpeq0  23483  chteq0  23484  chtleppi  23485  chpchtsum  23494  chpub  23495  dchr1re  23538  bcmono  23552  efexple  23556  bposlem1  23559  bposlem4  23562  bposlem5  23563  bposlem7  23565  bposlem8  23566  bposlem9  23567  lgsval2lem  23581  lgsval4a  23593  lgsneg  23594  lgsdilem  23597  lgsdir2lem1  23598  rplogsumlem2  23670  rpvmasumlem  23672  dchrisum0flblem1  23693  dchrisum0flblem2  23694  dchrisum0fno1  23696  rplogsum  23712  logdivsum  23718  mulog2sumlem2  23720  selberg2lem  23735  logdivbnd  23741  pntrsumo1  23750  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  pntpbnd1  23771  pntpbnd2  23772  pntlem3  23794  pntleml  23796  ostth2  23822  trgcgrg  23906  ttgcontlem1  24188  brbtwn2  24208  ax5seglem1  24231  ax5seglem2  24232  ax5seglem3  24234  ax5seglem5  24236  ax5seglem6  24237  ax5seglem9  24240  ax5seg  24241  axbtwnid  24242  axpaschlem  24243  axpasch  24244  axlowdimlem1  24245  axlowdimlem6  24250  axlowdimlem7  24251  axlowdimlem10  24254  axlowdim1  24262  axlowdim2  24263  axlowdim  24264  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  usgraexvlem  24395  usgraex0elv  24396  spthispth  24575  vdgr0  24900  rusgranumwlks  24956  konigsberg  24987  ex-po  25156  gxnval  25262  readdsubgo  25355  nvz0  25571  0blo  25707  nmlno0lem  25708  nmblolbii  25714  siilem2  25767  minvecolem2  25791  minvecolem3  25792  minvecolem4c  25795  minvecolem4  25796  minvecolem5  25797  minvecolem7  25799  htthlem  25834  hiidge0  26015  normlem6  26032  normgt0  26044  norm-i  26046  normpyc  26063  bcsiALT  26096  pjhthlem1  26309  pjneli  26641  nmlnop0iALT  26914  unopbd  26934  nmbdoplbi  26943  nmcoplbi  26947  nmbdfnlbi  26968  nmbdfnlb  26969  nmcfnlbi  26971  cnlnadjlem7  26992  nmopcoi  27014  branmfn  27024  leopmul  27053  nmopleid  27058  pjbdlni  27068  pjnormssi  27087  stge0  27143  stle1  27144  stle0i  27158  strlem3a  27171  cdj3lem1  27353  xaddeq0  27573  xdiv0  27625  xrge0slmod  27834  elunitrn  27879  elunitge0  27881  unitdivcld  27883  sqsscirc1  27890  xrge0iifcnv  27915  xrge0iifiso  27917  xrge0iifhom  27919  rezh  27952  rnlogblem  28015  logbrec  28021  log2le1  28023  indf  28029  indfval  28030  pr01ssre  28031  voliune  28201  volfiniune  28202  sibfinima  28281  0rrv  28390  coinfliprv  28421  ballotlem2  28427  ballotlem4  28437  ballotlemi1  28441  ballotlemic  28445  sgnclre  28478  sgnnbi  28484  sgnpbi  28485  plymulx0  28504  signsply0  28508  signswch  28518  signstf  28523  signstf0  28525  signstfveq0  28534  signlem0  28544  zetacvg  28557  eldmgm  28564  lgamgulmlem2  28572  rescon  28691  iiscon  28697  iillyscon  28698  cvmliftlem10  28739  snmlff  28774  fz0n  29110  logi  29121  bpoly4  29821  sin2h  30045  tan2h  30047  heicant  30049  mblfinlem2  30052  ismblfin  30055  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  mbfposadd  30062  dvtanlem  30064  itg2addnclem  30066  itg2addnclem2  30067  ibladdnclem  30071  itgaddnclem2  30074  iblabsnclem  30078  iblmulc2nc  30080  itgmulc2nclem2  30082  itgabsnc  30084  ftc1cnnclem  30088  ftc1anclem5  30094  ftc1anclem8  30097  asindmre  30102  dvasin  30103  areacirclem4  30110  areacirc  30112  nn0prpwlem  30140  isbnd3  30280  ssbnd  30284  prdsbnd  30289  bfplem2  30319  bfp  30320  modelico  30757  pellexlem6  30770  elpell14qr2  30798  oddcomabszz  30880  zindbi  30882  jm2.24  30901  acongeq  30921  arearect  31183  areaquad  31184  dvconstbi  31239  binomcxplemnn0  31254  binomcxplemdvbinom  31258  binomcxplemcvg  31259  binomcxplemnotnn0  31261  ltaddneg  31484  halffl  31493  dvnmptdivc  31735  dvnmul  31740  itgsin0pilem1  31748  itgsinexplem1  31752  itgsinexp  31753  iblempty  31764  stoweidlem17  31799  stoweidlem36  31818  stoweidlem55  31837  wallispilem1  31847  wallispilem2  31848  wallispilem4  31850  stirlinglem4  31859  stirlinglem13  31868  stirlinglem14  31869  stirlinglem15  31870  stirlingr  31872  dirker2re  31874  dirkerdenne0  31875  dirkerre  31877  dirkertrigeqlem1  31880  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem11  31900  fourierdlem16  31905  fourierdlem21  31910  fourierdlem22  31911  fourierdlem41  31930  fourierdlem42  31931  fourierdlem48  31937  fourierdlem62  31951  fourierdlem66  31955  fourierdlem79  31968  fourierdlem83  31972  fourierdlem94  31983  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fourierdlem112  32001  fourierdlem113  32002  fourierdlem114  32003  sqwvfoura  32011  sqwvfourb  32012  fourierswlem  32013  fouriersw  32014  etransclem23  32040  etransclem44  32061  etransclem46  32063  etransc  32066  zm1nn  32325  altgsumbcALT  32942  ex-gt  33122  sineq0ALT  33737  bj-flbi3  34608  bj-pinftyccb  34624  bj-minftyccb  34628  bj-pinftynminfty  34630  renegclALT  34694  taupilemrplb  37695  imo72b2lem0  37982  imo72b2lem2  37984  imo72b2lem1  37988  imo72b2  37993
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299
  Copyright terms: Public domain W3C validator