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

Theorem 0red 9643
Description:  0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
0red  |-  ( ph  ->  0  e.  RR )

Proof of Theorem 0red
StepHypRef Expression
1 0re 9642 . 2  |-  0  e.  RR
21a1i 11 1  |-  ( ph  ->  0  e.  RR )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870   RRcr 9537   0cc0 9538
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-addrcl 9599  ax-mulcl 9600  ax-mulrcl 9601  ax-i2m1 9606  ax-1ne0 9607  ax-rnegex 9609  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:  gt0ne0  10078  add20  10125  subge0  10126  lesub0  10130  mulge0  10131  msqgt0  10133  msqge0  10134  addgt0d  10187  sublt0d  10237  prodgt0  10449  prodge0  10451  lt2msq1  10489  supmul1  10576  supmul  10579  0mnnnnn0  10902  rpgecl  11328  ge0p1rp  11331  mul2lt0rlt0  11398  mul2lt0rgt0  11399  mul2lt0bi  11402  max0sub  11489  reltxrnmnf  11632  infmrp1  11634  iccf1o  11774  xov1plusxeqvd  11776  elfz1b  11862  elfz0fzfz0  11893  fz0fzelfz0  11894  fzo1fzo0n0  11955  elfzo0z  11956  fzofzim  11960  elfzodifsumelfzo  11977  ssfzoulel  12002  elfznelfzo  12011  muladdmodid  12134  modltm1p1mod  12139  expgt1  12307  ltexp2a  12321  expcan  12322  ltexp2  12323  leexp2  12324  leexp2a  12325  expnlbnd2  12400  discr  12406  brfi1uzind  12641  ccatsymb  12714  ccat2s1fvw  12756  swrdnd  12773  swrdswrdlem  12800  swrdswrd  12801  swrdccatin2  12828  swrdccatin12lem3  12831  repswswrd  12872  swrd2lsw  13006  2swrd2eqwrdeq  13007  leabs  13341  max0add  13352  absgt0  13366  rlimrege0  13621  iseraltlem2  13727  fsumrecl  13778  o1fsum  13851  cvgcmp  13854  cvgcmpce  13856  geomulcvg  13910  mertenslem2  13919  fprodle  14028  rpnnen2lem4  14248  moddvds  14290  bitsfzolem  14382  bitsinv1lem  14389  sadcaddlem  14405  lcmgcdlem  14542  qnumgt0  14670  modprm0  14719  qexpz  14809  prmreclem4  14826  4sqlem6  14850  prmgaplem7  14990  gzrngunit  18968  regsumsupp  19121  fvmptnn04ifd  19808  chfacffsupp  19811  chfacfscmul0  19813  chfacfscmulgsum  19815  chfacfpmmul0  19817  chfacfpmmulgsum  19819  prdsmet  21316  metustexhalf  21502  nlmvscnlem2  21619  nlmvscnlem1  21620  nmo0  21667  evth  21883  lebnumlem1  21885  lebnumii  21890  htpycc  21904  pcohtpylem  21943  pcoass  21948  pcorevlem  21950  nmoleub2lem3  22022  ipcnlem2  22108  ipcnlem1  22109  rrxcph  22244  rrxmetlem  22254  rrxmet  22255  rrxdstprj1  22256  ehlbase  22258  minveclem3b  22263  minveclem6  22269  pjthlem1  22272  ovolicopnf  22355  ioorcl2  22401  volivth  22442  mbfposr  22485  i1fmulc  22538  itg1mulc  22539  itg1ge0a  22546  mbfi1flim  22558  itg2split  22584  itg2monolem1  22585  itg2monolem3  22587  itg2mono  22588  itg2cnlem2  22597  itgge0  22645  dvlip  22822  dvlipcn  22823  dveq0  22829  dv11cn  22830  dvlt0  22834  dvfsumge  22851  dgradd2  23090  plydivlem3  23116  mtest  23224  radcnvlem1  23233  radcnv0  23236  radcnvlt1  23238  radcnvle  23240  pserulm  23242  pserdvlem1  23247  pserdv  23249  abelthlem2  23252  abelthlem7  23258  pilem2  23272  pilem2OLD  23273  coseq00topi  23322  tanabsge  23326  tanord1  23351  tanord  23352  rplogcl  23418  logdivle  23436  logcnlem3  23454  logcnlem4  23455  dvloglem  23458  logtayl  23470  abscxp2  23503  cxplt  23504  cxple  23505  cxple2a  23509  cxpcn3lem  23552  abscxpbnd  23558  chordthmlem5  23627  asinlem3  23662  atanre  23676  atanlogaddlem  23704  atanlogadd  23705  atanlogsublem  23706  atantan  23714  atans2  23722  efrlim  23760  cxp2limlem  23766  cxp2lim  23767  cxploglim2  23769  divsqrtsumlem  23770  jensenlem2  23778  harmonicubnd  23800  fsumharmonic  23802  dmlogdmgm  23814  lgamgulmlem1  23819  lgamgulmlem2  23820  ftalem1  23862  ftalem2  23863  ftalem5  23866  vmacl  23908  chtwordi  23946  ppiwordi  23952  chtrpcl  23965  fsumfldivdiaglem  23981  fsumvma2  24005  chpval2  24009  chpchtsum  24010  chpub  24011  logfacbnd3  24014  logexprlim  24016  mersenne  24018  lgslem4  24090  lgsdilem  24113  lgsne0  24124  lgseisen  24144  lgsquadlem1  24145  lgsquadlem2  24146  chebbnd1lem2  24171  chebbnd1lem3  24172  chebbnd1  24173  chtppilimlem1  24174  chtppilimlem2  24175  chtppilim  24176  chebbnd2  24178  chto1lb  24179  chpchtlim  24180  chpo1ub  24181  dchrisumlema  24189  dchrisumlem2  24191  dchrisumlem3  24192  dchrmusumlema  24194  dchrvmasumlem2  24199  dchrvmasumiflem1  24202  dchrisum0flblem1  24209  dchrisum0flblem2  24210  dchrisum0re  24214  dchrisum0lema  24215  dchrisum0  24221  dirith2  24229  mulog2sumlem1  24235  vmalogdivsum2  24239  log2sumbnd  24245  selberg2lem  24251  chpdifbndlem1  24254  chpdifbndlem2  24255  chpdifbnd  24256  selberg3lem1  24258  pntrmax  24265  pntrsumo1  24266  pntrlog2bndlem4  24281  pntrlog2bndlem5  24282  pntpbnd1a  24286  pntpbnd1  24287  pntpbnd2  24288  pntlemg  24299  pntlemj  24304  pntlemk  24307  pntlem3  24310  pntleml  24312  pnt2  24314  pnt  24315  ostth2lem1  24319  padicabv  24331  padicabvcxp  24333  ostth2lem3  24336  ostth2lem4  24337  ostth3  24339  trgcgrg  24422  axsegconlem7  24799  axsegconlem10  24802  axcontlem2  24841  axcontlem4  24843  axcontlem7  24846  axcontlem10  24849  nvnencycllem  25216  clwwlkn0  25347  clwlkisclwwlklem2a2  25353  clwlkisclwwlklem2a  25358  wwlksubclwwlk  25377  frgraogt3nreg  25693  friendshipgt3  25694  minvecolem5  26368  minvecolem6  26369  htthlem  26405  pjhthlem1  26879  nndiffz1  28202  bcm1n  28207  2sqmod  28247  regsumfsum  28383  pnfneige0  28596  nexple  28670  indf1o  28684  measinb  28882  eulerpartlems  29019  eulerpartlemgc  29021  ballotlemfc0  29151  ballotlemfcc  29152  ballotlemodife  29156  sgnneg  29199  sgnmul  29201  sgnsub  29203  signsply0  29228  signslema  29239  signsvtp  29260  signshf  29265  cvmliftlem2  29797  bj-pinftynminfty  31414  poimirlem10  31653  poimirlem11  31654  poimirlem24  31667  poimirlem29  31672  poimirlem31  31674  poimirlem32  31675  poimir  31676  bddiblnc  31715  ftc1anclem7  31726  ftc1anclem8  31727  ftc1anc  31728  areacirclem1  31735  areacirclem4  31738  areacirc  31740  geomcau  31791  isbnd3b  31820  prdsbnd  31828  bfp  31859  rrnequiv  31870  irrapxlem1  35375  irrapxlem2  35376  irrapxlem3  35377  irrapxlem4  35378  pellexlem6  35387  pell14qrgt0  35412  pell1qrgaplem  35426  pellfundex  35439  pellfundrp  35441  monotoddzzfi  35495  jm2.24  35518  jm2.23  35556  jm2.26lem3  35561  jm3.1lem3  35579  imo72b2lem1  36250  isprm7  36296  dvgrat  36297  hashnzfz2  36306  binomcxplemnn0  36334  binomcxplemnotnn0  36341  neglt  37102  divlt0gt0d  37104  upbdrech2  37134  fsumnncl  37224  sumnnodd  37281  lptre2pt  37291  dvmptconst  37356  dvdivbd  37366  dvcosax  37369  dvbdfbdioolem1  37371  dvbdfbdioolem2  37372  ioodvbdlimc1lem1  37374  ioodvbdlimc1lem2  37375  ioodvbdlimc2lem  37377  dvxpaek  37383  dvnxpaek  37385  volioc  37417  stoweidlem1  37429  stoweidlem7  37435  stoweidlem11  37439  stoweidlem25  37453  stoweidlem26  37454  stoweidlem34  37463  stoweidlem36  37465  stoweidlem41  37470  stoweidlem42  37471  stoweidlem44  37473  stoweidlem45  37474  wallispilem3  37497  wallispilem4  37498  wallispi  37500  stirlinglem3  37506  stirlinglem5  37508  stirlinglem6  37509  stirlinglem7  37510  stirlinglem10  37513  stirlinglem11  37514  stirlinglem12  37515  dirkeritg  37532  dirkercncflem2  37534  fourierdlem9  37546  fourierdlem11  37548  fourierdlem12  37549  fourierdlem14  37551  fourierdlem15  37552  fourierdlem19  37556  fourierdlem24  37561  fourierdlem28  37565  fourierdlem30  37567  fourierdlem40  37577  fourierdlem41  37578  fourierdlem43  37580  fourierdlem44  37581  fourierdlem47  37584  fourierdlem50  37587  fourierdlem51  37588  fourierdlem57  37594  fourierdlem60  37597  fourierdlem61  37598  fourierdlem66  37603  fourierdlem68  37605  fourierdlem73  37610  fourierdlem74  37611  fourierdlem75  37612  fourierdlem78  37615  fourierdlem79  37616  fourierdlem83  37620  fourierdlem88  37625  fourierdlem92  37629  fourierdlem93  37630  fourierdlem97  37634  fourierdlem103  37640  fourierdlem104  37641  fourierdlem109  37646  fourierdlem111  37648  sqwvfoura  37659  sqwvfourb  37660  fourierswlem  37661  fouriersw  37662  elaa2lem  37664  etransclem4  37669  etransclem18  37683  etransclem19  37684  etransclem23  37688  etransclem27  37692  etransclem31  37696  etransclem32  37697  etransclem35  37700  etransclem41  37706  etransclem46  37711  etransclem48  37713  sge0tsms  37755  sharhght  37873  iccpartigtl  38126  iccpartgt  38130  zm1nn  38397  eluzge0nn0  38401  elfz2z  38403  2ffzoeq  38412  expnegico01  39074  m1modmmod  39084  difmodm1lt  39085  regt1loggt0  39107  refdivmptf  39113  elbigolo1  39128  rege1logbrege0  39129  fllog2  39139  dignn0flhalflem1  39186
  Copyright terms: Public domain W3C validator