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

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

Proof of Theorem 0red
StepHypRef Expression
1 0re 10203 . 2 0 ∈ ℝ
21a1i 11 1 (𝜑 → 0 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2127  cr 10098  0cc0 10099
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-1cn 10157  ax-icn 10158  ax-addcl 10159  ax-addrcl 10160  ax-mulcl 10161  ax-mulrcl 10162  ax-i2m1 10167  ax-1ne0 10168  ax-rnegex 10170  ax-rrecex 10171  ax-cnre 10172
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-iota 6000  df-fv 6045  df-ov 6804
This theorem is referenced by:  gt0ne0  10656  add20  10703  subge0  10704  lesub0  10708  mulge0  10709  msqgt0  10711  msqge0  10712  addgt0d  10765  sublt0d  10816  prodgt0  11031  prodge0  11033  lt2msq1  11070  supmul1  11155  supmul  11158  0mnnnnn0  11488  nn0negleid  11508  rpgecl  12023  ge0p1rp  12026  ledivge1le  12065  mul2lt0rlt0  12096  mul2lt0rgt0  12097  mul2lt0bi  12100  max0sub  12191  reltxrnmnf  12336  infmrp1  12338  iccf1o  12480  xov1plusxeqvd  12482  elfz0fzfz0  12609  fz0fzelfz0  12610  elfzo0z  12675  fzofzim  12680  fzo1fzo0n0  12684  elfzodifsumelfzo  12699  ssfzoulel  12727  elfznelfzo  12738  muladdmodid  12875  modltm1p1mod  12887  addmodlteq  12910  expgt1  13063  ltexp2a  13077  expcan  13078  ltexp2  13079  leexp2  13080  leexp2a  13081  expnlbnd2  13160  discr  13166  fi1uzind  13442  ccatsymb  13525  ccat2s1fvw  13585  swrdnd  13603  swrdswrdlem  13630  swrdswrd  13631  swrdccatin2  13658  swrdccatin12lem3  13661  repswswrd  13702  swrd2lsw  13867  2swrd2eqwrdeq  13868  leabs  14209  max0add  14220  absgt0  14234  rlimrege0  14480  iseraltlem2  14583  fsumrecl  14635  o1fsum  14715  cvgcmp  14718  cvgcmpce  14720  geomulcvg  14777  mertenslem2  14787  fprodle  14897  rpnnen2lem4  15116  p1modz1  15160  moddvds  15164  oddge22np1  15246  bitsfzolem  15329  bitsinv1lem  15336  sadcaddlem  15352  lcmgcdlem  15492  dvdsnprmd  15576  isprm7  15593  qnumgt0  15631  modprm0  15683  qexpz  15778  prmreclem4  15796  4sqlem6  15820  prmgaplem7  15934  gzrngunit  19985  regsumfsum  19987  regsumsupp  20141  fvmptnn04ifd  20831  chfacffsupp  20834  chfacfscmul0  20836  chfacfscmulgsum  20838  chfacfpmmul0  20840  chfacfpmmulgsum  20842  prdsmet  22347  metustexhalf  22533  nlmvscnlem2  22661  nlmvscnlem1  22662  nmo0  22711  evth  22930  lebnumlem1  22932  lebnumii  22937  htpycc  22951  pcohtpylem  22990  pcoass  22995  pcorevlem  22997  nmoleub2lem3  23086  ipcnlem2  23214  ipcnlem1  23215  rrxcph  23351  rrxmetlem  23361  rrxmet  23362  rrxdstprj1  23363  ehlbase  23365  minveclem3b  23370  minveclem6  23376  pjthlem1  23379  ovolicopnf  23463  ioorcl2  23511  volivth  23546  mbfposr  23589  i1fmulc  23640  itg1mulc  23641  itg1ge0a  23648  mbfi1flim  23660  itg2split  23686  itg2monolem1  23687  itg2monolem3  23689  itg2mono  23690  itg2cnlem2  23699  itgge0  23747  dvlip  23926  dvlipcn  23927  dveq0  23933  dv11cn  23934  dvlt0  23938  dvfsumge  23955  dgradd2  24194  plydivlem3  24220  mtest  24328  radcnvlem1  24337  radcnv0  24340  radcnvlt1  24342  radcnvle  24344  pserulm  24346  pserdvlem1  24351  pserdv  24353  abelthlem2  24356  abelthlem7  24362  pilem2  24376  coseq00topi  24424  tanabsge  24428  tanord1  24453  tanord  24454  rplogcl  24520  logdivle  24538  logcnlem3  24560  logcnlem4  24561  dvloglem  24564  logtayl  24576  abscxp2  24609  cxplt  24610  cxple  24611  cxple2a  24615  cxpcn3lem  24658  abscxpbnd  24664  chordthmlem5  24733  asinlem3  24768  atanre  24782  atanlogaddlem  24810  atanlogadd  24811  atanlogsublem  24812  atantan  24820  atans2  24828  efrlim  24866  cxp2limlem  24872  cxp2lim  24873  cxploglim2  24875  divsqrtsumlem  24876  jensenlem2  24884  harmonicubnd  24906  fsumharmonic  24908  dmlogdmgm  24920  lgamgulmlem1  24925  lgamgulmlem2  24926  ftalem1  24969  ftalem2  24970  ftalem5  24973  vmacl  25014  chtwordi  25052  ppiwordi  25058  chtrpcl  25071  fsumfldivdiaglem  25085  fsumvma2  25109  chpval2  25113  chpchtsum  25114  chpub  25115  logfacbnd3  25118  logexprlim  25120  mersenne  25122  lgsdilem  25219  lgsne0  25230  gausslemma2dlem1a  25260  lgseisen  25274  lgsquadlem1  25275  lgsquadlem2  25276  chebbnd1lem2  25329  chebbnd1lem3  25330  chebbnd1  25331  chtppilimlem1  25332  chtppilimlem2  25333  chtppilim  25334  chebbnd2  25336  chto1lb  25337  chpchtlim  25338  chpo1ub  25339  dchrisumlema  25347  dchrisumlem2  25349  dchrisumlem3  25350  dchrmusumlema  25352  dchrvmasumlem2  25357  dchrvmasumiflem1  25360  dchrisum0flblem1  25367  dchrisum0flblem2  25368  dchrisum0re  25372  dchrisum0lema  25373  dchrisum0  25379  dirith2  25387  mulog2sumlem1  25393  vmalogdivsum2  25397  log2sumbnd  25403  selberg2lem  25409  chpdifbndlem1  25412  chpdifbndlem2  25413  chpdifbnd  25414  selberg3lem1  25416  pntrmax  25423  pntrsumo1  25424  pntrlog2bndlem4  25439  pntrlog2bndlem5  25440  pntpbnd1a  25444  pntpbnd1  25445  pntpbnd2  25446  pntlemg  25457  pntlemj  25462  pntlemk  25465  pntlem3  25468  pntleml  25470  pnt2  25472  pnt  25473  ostth2lem1  25477  padicabv  25489  padicabvcxp  25491  ostth2lem3  25494  ostth2lem4  25495  ostth3  25497  trgcgrg  25580  tgcgr4  25596  axsegconlem7  25973  axsegconlem10  25976  axcontlem2  26015  axcontlem4  26017  axcontlem7  26020  axcontlem10  26023  crctcshwlkn0lem3  26886  crctcshwlkn0  26895  clwlkclwwlklem2a2  27087  clwlkclwwlklem2a  27092  wwlksubclwwlk  27160  frgrogt3nreg  27536  friendshipgt3  27537  minvecolem5  28017  minvecolem6  28018  htthlem  28054  pjhthlem1  28530  nndiffz1  29828  bcm1n  29834  2sqmod  29928  pnfneige0  30277  nexple  30351  indf1o  30366  measinb  30564  eulerpartlems  30702  eulerpartlemgc  30704  ballotlemfc0  30834  ballotlemfcc  30835  ballotlemodife  30839  sgnneg  30882  sgnmul  30884  sgnsub  30886  signsply0  30908  signslema  30919  signsvtp  30940  signshf  30945  itgexpif  30964  breprexplemc  30990  circlemeth  30998  logdivsqrle  31008  cvmliftlem2  31546  dnibndlem9  32753  unbdqndv2lem2  32778  knoppndvlem1  32780  knoppndvlem2  32781  knoppndvlem7  32786  knoppndvlem11  32790  knoppndvlem14  32793  knoppndvlem15  32794  knoppndvlem17  32796  knoppndvlem19  32798  knoppndvlem20  32799  bj-pinftynminfty  33396  poimirlem10  33701  poimirlem11  33702  poimirlem24  33715  poimirlem29  33720  poimirlem31  33722  poimirlem32  33723  poimir  33724  mblfinlem2  33729  bddiblnc  33762  ftc1anclem7  33773  ftc1anclem8  33774  ftc1anc  33775  areacirclem1  33782  areacirclem4  33785  areacirc  33787  geomcau  33837  isbnd3b  33866  prdsbnd  33874  bfp  33905  rrnequiv  33916  irrapxlem1  37857  irrapxlem2  37858  irrapxlem3  37859  irrapxlem4  37860  pellexlem6  37869  pell14qrgt0  37894  pell1qrgaplem  37908  pellfundex  37921  pellfundrp  37923  monotoddzzfi  37978  jm2.24  38001  jm2.23  38034  jm2.26lem3  38039  jm3.1lem3  38057  k0004ss2  38921  imo72b2lem1  38942  dvgrat  38982  hashnzfz2  38991  binomcxplemnn0  39019  binomcxplemnotnn0  39026  neglt  39964  divlt0gt0d  39966  upbdrech2  39990  xralrple2  40037  xralrple3  40057  fiminre2  40061  reclt0d  40074  reclt0  40081  xrpnf  40183  fsumnncl  40275  fsumsupp0  40282  sumnnodd  40334  lptre2pt  40344  limsupubuz  40417  liminfresre  40483  liminf0  40497  dvmptconst  40601  dvdivbd  40610  dvcosax  40613  dvbdfbdioolem1  40615  dvbdfbdioolem2  40616  ioodvbdlimc1lem1  40618  ioodvbdlimc1lem2  40619  ioodvbdlimc2lem  40621  dvxpaek  40627  dvnxpaek  40629  volioc  40660  volico  40672  stoweidlem1  40690  stoweidlem7  40696  stoweidlem11  40700  stoweidlem25  40714  stoweidlem26  40715  stoweidlem34  40723  stoweidlem36  40725  stoweidlem41  40730  stoweidlem42  40731  stoweidlem44  40733  stoweidlem45  40734  wallispilem3  40756  wallispilem4  40757  wallispi  40759  stirlinglem3  40765  stirlinglem5  40767  stirlinglem6  40768  stirlinglem7  40769  stirlinglem10  40772  stirlinglem11  40773  stirlinglem12  40774  dirkeritg  40791  dirkercncflem2  40793  fourierdlem9  40805  fourierdlem11  40807  fourierdlem12  40808  fourierdlem14  40810  fourierdlem15  40811  fourierdlem19  40815  fourierdlem24  40820  fourierdlem28  40824  fourierdlem30  40826  fourierdlem40  40836  fourierdlem41  40837  fourierdlem43  40839  fourierdlem44  40840  fourierdlem47  40842  fourierdlem50  40845  fourierdlem51  40846  fourierdlem57  40852  fourierdlem60  40855  fourierdlem61  40856  fourierdlem66  40861  fourierdlem68  40863  fourierdlem73  40868  fourierdlem74  40869  fourierdlem75  40870  fourierdlem78  40873  fourierdlem79  40874  fourierdlem83  40878  fourierdlem88  40883  fourierdlem92  40887  fourierdlem93  40888  fourierdlem97  40892  fourierdlem103  40898  fourierdlem104  40899  fourierdlem109  40904  fourierdlem111  40906  sqwvfoura  40917  sqwvfourb  40918  fourierswlem  40919  fouriersw  40920  elaa2lem  40922  etransclem4  40927  etransclem18  40941  etransclem19  40942  etransclem23  40946  etransclem27  40950  etransclem31  40954  etransclem32  40955  etransclem35  40958  etransclem41  40964  etransclem46  40969  etransclem48  40971  rrxtopnfi  40978  qndenserrnbllem  40986  salgencntex  41033  sge0tsms  41069  sge0isum  41116  volicorecl  41235  hoiprodcl  41236  ovnlerp  41251  ovnsubaddlem1  41259  hoiprodcl3  41269  volicore  41270  hoidmvcl  41271  hoidmvlelem1  41284  hoidmvlelem2  41285  hoidmvlelem3  41286  ovnhoi  41292  hoiqssbllem2  41312  volicorege0  41326  vonhoire  41361  pimrecltpos  41394  pimrecltneg  41408  smfmbfcex  41443  nsssmfmbflem  41461  smfrec  41471  smfmullem3  41475  sharhght  41529  zm1nn  41795  eluzge0nn0  41801  elfz2z  41804  2ffzoeq  41817  iccpartigtl  41838  iccpartgt  41842  expnegico01  42787  m1modmmod  42795  difmodm1lt  42796  regt1loggt0  42809  refdivmptf  42815  elbigolo1  42830  rege1logbrege0  42831  fllog2  42841  dignn0flhalflem1  42888  amgmwlem  43030
  Copyright terms: Public domain W3C validator