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

Theorem 0red 11159
Description: The number 0 is real, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.)
Assertion
Ref Expression
0red (𝜑 → 0 ∈ ℝ)

Proof of Theorem 0red
StepHypRef Expression
1 0re 11158 . 2 0 ∈ ℝ
21a1i 11 1 (𝜑 → 0 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  cr 11051  0cc0 11052
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-1cn 11110  ax-addrcl 11113  ax-rnegex 11123  ax-cnre 11125
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-clel 2815  df-rex 3075
This theorem is referenced by:  gt0ne0  11621  add20  11668  subge0  11669  lesub0  11673  mulge0  11674  msqgt0  11676  msqge0  11677  addgt0d  11731  sublt0d  11782  prodgt0  12003  lt2msq1  12040  fiminre2  12104  supmul1  12125  supmul  12128  nnne0  12188  0mnnnnn0  12446  nn0negleid  12466  rpgecl  12944  ge0p1rp  12947  ledivge1le  12987  mul2lt0rlt0  13018  mul2lt0rgt0  13019  mul2lt0bi  13022  prodge0rd  13023  max0sub  13116  reltxrnmnf  13262  infmrp1  13264  lincmb01cmp  13413  iccf1o  13414  xov1plusxeqvd  13416  elfz0fzfz0  13547  fz0fzelfz0  13548  elfzo0z  13615  fzofzim  13620  fzo1fzo0n0  13624  elfzodifsumelfzo  13639  ssfzoulel  13667  elfznelfzo  13678  muladdmodid  13817  modltm1p1mod  13829  addmodlteq  13852  expgt1  14007  ltexp2a  14072  expcan  14075  ltexp2  14076  leexp2  14077  leexp2a  14078  zzlesq  14111  expnlbnd2  14138  discr  14144  fi1uzind  14397  ccatsymb  14471  ccat2s1fvw  14527  swrdnd  14543  swrdnnn0nd  14545  swrdswrdlem  14593  swrdswrd  14594  repswswrd  14673  swrd2lsw  14842  2swrd2eqwrdeq  14843  leabs  15185  max0add  15196  absgt0  15210  rlimrege0  15462  iseraltlem2  15568  fsumrecl  15620  o1fsum  15699  cvgcmp  15702  cvgcmpce  15704  geomulcvg  15762  mertenslem2  15771  fprodle  15880  rpnnen2lem4  16100  p1modz1  16144  moddvds  16148  oddge22np1  16232  bitsfzolem  16315  bitsinv1lem  16322  sadcaddlem  16338  lcmgcdlem  16483  dvdsnprmd  16567  2mulprm  16570  isprm7  16585  qnumgt0  16626  modprm0  16678  qexpz  16774  prmreclem4  16792  4sqlem6  16816  prmgaplem7  16930  gzrngunit  20866  regsumfsum  20868  regsumsupp  21029  fvmptnn04ifd  22205  chfacffsupp  22208  chfacfscmul0  22210  chfacfscmulgsum  22212  chfacfpmmul0  22214  chfacfpmmulgsum  22216  prdsmet  23726  metustexhalf  23915  nlmvscnlem2  24052  nlmvscnlem1  24053  nmo0  24102  blcvx  24164  evth  24325  lebnumlem1  24327  lebnumii  24332  htpycc  24346  pcohtpylem  24385  pcoass  24390  pcorevlem  24392  nmoleub2lem3  24481  ipcnlem2  24611  ipcnlem1  24612  rrxcph  24759  rrxmetlem  24774  rrxmet  24775  rrxdstprj1  24776  ehlbase  24782  minveclem3b  24795  minveclem6  24801  pjthlem1  24804  ovolicopnf  24891  ioorcl2  24939  volivth  24974  mbfposr  25019  i1fmulc  25071  itg1mulc  25072  itg1ge0a  25079  mbfi1flim  25091  itg2split  25117  itg2monolem1  25118  itg2monolem3  25120  itg2mono  25121  itg2cnlem2  25130  itgge0  25178  bddiblnc  25209  dvlip  25360  dvlipcn  25361  dveq0  25367  dv11cn  25368  dvlt0  25372  dvfsumge  25389  dgradd2  25632  plydivlem3  25658  mtest  25766  radcnvlem1  25775  radcnv0  25778  radcnvlt1  25780  radcnvle  25782  pserulm  25784  pserdvlem1  25789  pserdv  25791  abelthlem2  25794  abelthlem7  25800  pilem2  25814  pilem3  25815  coseq00topi  25862  tanabsge  25866  cosq34lt1  25886  tanord1  25896  tanord  25897  rplogcl  25962  logdivle  25980  logcnlem3  26002  logcnlem4  26003  dvloglem  26006  logtayl  26018  abscxp2  26051  cxplt  26052  cxple  26053  cxple2a  26057  cxpcn3lem  26103  abscxpbnd  26109  chordthmlem4  26188  chordthmlem5  26189  asinlem3  26224  atanre  26238  atanlogaddlem  26266  atanlogadd  26267  atanlogsublem  26268  atantan  26276  atans2  26284  efrlim  26322  cxp2limlem  26328  cxp2lim  26329  cxploglim2  26331  divsqrtsumlem  26332  jensenlem2  26340  harmonicubnd  26362  fsumharmonic  26364  dmlogdmgm  26376  lgamgulmlem1  26381  lgamgulmlem2  26382  ftalem1  26425  ftalem2  26426  ftalem5  26429  vmacl  26470  chtwordi  26508  ppiwordi  26514  chtrpcl  26527  fsumfldivdiaglem  26541  fsumvma2  26565  chpval2  26569  chpchtsum  26570  chpub  26571  logfacbnd3  26574  logexprlim  26576  mersenne  26578  lgsdilem  26675  lgsne0  26686  gausslemma2dlem1a  26716  lgseisen  26730  lgsquadlem1  26731  lgsquadlem2  26732  2sqmod  26787  2sqnn0  26789  chebbnd1lem2  26821  chebbnd1lem3  26822  chebbnd1  26823  chtppilimlem1  26824  chtppilimlem2  26825  chtppilim  26826  chebbnd2  26828  chto1lb  26829  chpchtlim  26830  chpo1ub  26831  dchrisumlema  26839  dchrisumlem2  26841  dchrisumlem3  26842  dchrmusumlema  26844  dchrvmasumlem2  26849  dchrvmasumiflem1  26852  dchrisum0flblem1  26859  dchrisum0flblem2  26860  dchrisum0re  26864  dchrisum0lema  26865  dchrisum0  26871  dirith2  26879  mulog2sumlem1  26885  vmalogdivsum2  26889  log2sumbnd  26895  selberg2lem  26901  chpdifbndlem1  26904  chpdifbnd  26906  selberg3lem1  26908  pntrmax  26915  pntrsumo1  26916  pntrlog2bndlem4  26931  pntrlog2bndlem5  26932  pntpbnd1a  26936  pntpbnd1  26937  pntpbnd2  26938  pntlemg  26949  pntlemj  26954  pntlemk  26957  pntlem3  26960  pnt2  26964  pnt  26965  ostth2lem1  26969  padicabv  26981  padicabvcxp  26983  ostth2lem3  26986  ostth2lem4  26987  ostth3  26989  trgcgrg  27460  tgcgr4  27476  axsegconlem7  27875  axsegconlem10  27878  axcontlem2  27917  axcontlem4  27919  axcontlem7  27922  axcontlem10  27925  crctcshwlkn0lem3  28760  crctcshwlkn0  28769  clwlkclwwlklem2a2  28940  clwlkclwwlklem2a  28945  wwlksubclwwlk  29005  frgrogt3nreg  29344  friendshipgt3  29345  minvecolem5  29826  minvecolem6  29827  htthlem  29862  pjhthlem1  30336  nndiffz1  31692  bcm1n  31701  wrdt2ind  31810  cycpmrn  31995  cyc3conja  32009  ccfldextdgrr  32359  pnfneige0  32535  nexple  32611  indf1o  32626  measinb  32823  eulerpartlems  32963  eulerpartlemgc  32965  ballotlemfc0  33095  ballotlemfcc  33096  ballotlemodife  33100  sgnneg  33143  sgnmul  33145  sgnsub  33147  signsply0  33166  signslema  33177  signsvtp  33198  itgexpif  33222  breprexplemc  33248  circlemeth  33256  logdivsqrle  33266  0nn0m1nnn0  33706  cvmliftlem2  33883  dnibndlem9  34952  unbdqndv2lem2  34976  knoppndvlem1  34978  knoppndvlem2  34979  knoppndvlem7  34984  knoppndvlem11  34988  knoppndvlem14  34991  knoppndvlem15  34992  knoppndvlem17  34994  knoppndvlem19  34996  knoppndvlem20  34997  bj-pinftynminfty  35701  poimirlem10  36091  poimirlem11  36092  poimirlem24  36105  poimirlem29  36110  poimirlem31  36112  poimirlem32  36113  poimir  36114  mblfinlem2  36119  ftc1anclem7  36160  ftc1anclem8  36161  ftc1anc  36162  areacirclem1  36169  areacirclem4  36172  areacirc  36174  geomcau  36221  isbnd3b  36247  prdsbnd  36255  bfp  36286  rrnequiv  36297  resdvopclptsd  40488  lcmineqlem2  40490  lcmineqlem3  40491  lcmineqlem10  40498  lcmineqlem12  40500  lcmineqlem23  40511  3lexlogpow5ineq1  40514  3lexlogpow5ineq2  40515  3lexlogpow5ineq4  40516  3lexlogpow5ineq3  40517  3lexlogpow2ineq2  40519  3lexlogpow5ineq5  40520  aks4d1lem1  40522  dvrelog2  40524  dvrelog3  40525  dvrelog2b  40526  0nonelalab  40527  dvrelogpow2b  40528  aks4d1p1p3  40529  aks4d1p1p2  40530  aks4d1p1p4  40531  aks4d1p1p6  40533  aks4d1p1p7  40534  aks4d1p1p5  40535  aks4d1p1  40536  aks4d1p2  40537  aks4d1p3  40538  aks4d1p5  40540  aks4d1p6  40541  aks4d1p7d1  40542  aks4d1p7  40543  aks4d1p8d2  40545  aks4d1p8d3  40546  aks4d1p8  40547  aks4d1p9  40548  2np3bcnp1  40555  2ap1caineq  40556  sticksstones7  40563  sticksstones10  40566  sticksstones12a  40568  sticksstones12  40569  sticksstones22  40579  metakunt2  40581  metakunt29  40608  sn-1ne2  40784  oexpreposd  40810  nn0rppwr  40822  nn0expgcd  40824  posqsqznn  40832  rtprmirr  40836  re1m1e0m0  40869  re0m0e0  40874  remul01  40879  remulneg2d  40886  sn-addlt0d  40918  sn-addgt0d  40919  renegmulnnass  40925  zmulcomlem  40927  mulgt0con1dlem  40929  dffltz  40975  3cubeslem1  41010  irrapxlem1  41148  irrapxlem2  41149  irrapxlem3  41150  irrapxlem4  41151  pellexlem6  41160  pell14qrgt0  41185  pell1qrgaplem  41199  pellfundex  41212  pellfundrp  41214  monotoddzzfi  41269  jm2.24  41290  jm2.23  41323  jm2.26lem3  41328  jm3.1lem3  41346  sqrtcvallem1  41910  reabsifneg  41911  reabsifpos  41913  sqrtcval  41920  k0004ss2  42431  imo72b2lem1  42449  dvgrat  42599  hashnzfz2  42608  binomcxplemnn0  42636  binomcxplemnotnn0  42643  neglt  43525  divlt0gt0d  43527  upbdrech2  43549  xralrple2  43595  xralrple3  43615  reclt0d  43628  reclt0  43633  xrpnf  43728  fsumnncl  43820  fsumsupp0  43826  sumnnodd  43878  lptre2pt  43888  limsupubuz  43961  liminfresre  44027  liminf0  44041  dvmptconst  44163  dvdivbd  44171  dvcosax  44174  dvbdfbdioolem1  44176  dvbdfbdioolem2  44177  ioodvbdlimc1lem1  44179  ioodvbdlimc1lem2  44180  ioodvbdlimc2lem  44182  dvxpaek  44188  dvnxpaek  44190  volioc  44220  volico  44231  stoweidlem1  44249  stoweidlem7  44255  stoweidlem11  44259  stoweidlem25  44273  stoweidlem26  44274  stoweidlem34  44282  stoweidlem36  44284  stoweidlem41  44289  stoweidlem42  44290  stoweidlem44  44292  stoweidlem45  44293  wallispilem3  44315  wallispilem4  44316  wallispi  44318  stirlinglem3  44324  stirlinglem5  44326  stirlinglem6  44327  stirlinglem7  44328  stirlinglem10  44331  stirlinglem11  44332  stirlinglem12  44333  dirkeritg  44350  dirkercncflem2  44352  fourierdlem9  44364  fourierdlem11  44366  fourierdlem12  44367  fourierdlem14  44369  fourierdlem15  44370  fourierdlem19  44374  fourierdlem24  44379  fourierdlem28  44383  fourierdlem30  44385  fourierdlem40  44395  fourierdlem41  44396  fourierdlem43  44398  fourierdlem44  44399  fourierdlem47  44401  fourierdlem50  44404  fourierdlem51  44405  fourierdlem57  44411  fourierdlem60  44414  fourierdlem61  44415  fourierdlem66  44420  fourierdlem68  44422  fourierdlem73  44427  fourierdlem74  44428  fourierdlem75  44429  fourierdlem78  44432  fourierdlem79  44433  fourierdlem83  44437  fourierdlem88  44442  fourierdlem92  44446  fourierdlem93  44447  fourierdlem97  44451  fourierdlem103  44457  fourierdlem104  44458  fourierdlem109  44463  fourierdlem111  44465  sqwvfoura  44476  sqwvfourb  44477  fourierswlem  44478  fouriersw  44479  elaa2lem  44481  etransclem4  44486  etransclem18  44500  etransclem19  44501  etransclem23  44505  etransclem27  44509  etransclem31  44513  etransclem32  44514  etransclem35  44517  etransclem41  44523  etransclem46  44528  etransclem48  44530  rrxtopnfi  44535  qndenserrnbllem  44542  salgencntex  44591  sge0tsms  44628  sge0isum  44675  volicorecl  44794  hoiprodcl  44795  ovnlerp  44810  ovnsubaddlem1  44818  hoiprodcl3  44828  volicore  44829  hoidmvcl  44830  hoidmvlelem1  44843  hoidmvlelem2  44844  hoidmvlelem3  44845  ovnhoi  44851  hoiqssbllem2  44871  volicorege0  44885  vonhoire  44920  pimrecltpos  44956  pimrecltneg  44972  smfmbfcex  45008  nsssmfmbflem  45026  smfrec  45037  smfmullem3  45041  smfdivdmmbl  45086  sharhght  45113  et-sqrtnegnre  45121  natglobalincr  45123  upwordnul  45126  zm1nn  45541  eluzge0nn0  45551  elfz2z  45554  2ffzoeq  45567  iccpartigtl  45622  iccpartgt  45626  requad01  45820  requad1  45821  requad2  45822  expnegico01  46606  m1modmmod  46614  difmodm1lt  46615  regt1loggt0  46629  refdivmptf  46635  elbigolo1  46650  rege1logbrege0  46651  fllog2  46661  dignn0flhalflem1  46708  eenglngeehlnmlem2  46831  line2  46845  line2xlem  46846  line2x  46847  line2y  46848  itsclc0yqsol  46857  2itscp  46874  inlinecirc02plem  46879  amgmwlem  47256
  Copyright terms: Public domain W3C validator