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

Theorem 0red 10337
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 10336 . 2 0 ∈ ℝ
21a1i 11 1 (𝜑 → 0 ∈ ℝ)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  cr 10229  0cc0 10230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-1cn 10288  ax-icn 10289  ax-addcl 10290  ax-addrcl 10291  ax-mulcl 10292  ax-mulrcl 10293  ax-i2m1 10298  ax-1ne0 10299  ax-rnegex 10301  ax-rrecex 10302  ax-cnre 10303
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-iota 6073  df-fv 6118  df-ov 6886
This theorem is referenced by:  gt0ne0  10787  add20  10834  subge0  10835  lesub0  10839  mulge0  10840  msqgt0  10842  msqge0  10843  addgt0d  10896  sublt0d  10947  prodgt0  11162  prodge0OLD  11164  lt2msq1  11201  supmul1  11286  supmul  11289  0mnnnnn0  11610  nn0negleid  11630  rpgecl  12092  ge0p1rp  12095  ledivge1le  12134  mul2lt0rlt0  12165  mul2lt0rgt0  12166  mul2lt0bi  12169  prodge0rd  12170  max0sub  12264  reltxrnmnf  12409  infmrp1  12411  iccf1o  12558  xov1plusxeqvd  12560  elfz0fzfz0  12687  fz0fzelfz0  12688  elfzo0z  12753  fzofzim  12758  fzo1fzo0n0  12762  elfzodifsumelfzo  12777  ssfzoulel  12805  elfznelfzo  12816  muladdmodid  12953  modltm1p1mod  12965  addmodlteq  12988  expgt1  13140  ltexp2a  13154  expcan  13155  ltexp2  13156  leexp2  13157  leexp2a  13158  expnlbnd2  13237  discr  13243  fi1uzind  13515  ccatsymb  13598  ccat2s1fvw  13657  swrdnd  13675  swrdswrdlem  13702  swrdswrd  13703  swrdccatin2  13730  swrdccatin12lem3  13733  repswswrd  13774  swrd2lsw  13939  2swrd2eqwrdeq  13940  leabs  14281  max0add  14292  absgt0  14306  rlimrege0  14552  iseraltlem2  14655  fsumrecl  14707  o1fsum  14786  cvgcmp  14789  cvgcmpce  14791  geomulcvg  14848  mertenslem2  14857  fprodle  14966  rpnnen2lem4  15185  p1modz1  15229  moddvds  15233  oddge22np1  15312  bitsfzolem  15394  bitsinv1lem  15401  sadcaddlem  15417  lcmgcdlem  15557  dvdsnprmd  15640  isprm7  15656  qnumgt0  15694  modprm0  15746  qexpz  15841  prmreclem4  15859  4sqlem6  15883  prmgaplem7  15997  gzrngunit  20039  regsumfsum  20041  regsumsupp  20196  fvmptnn04ifd  20891  chfacffsupp  20894  chfacfscmul0  20896  chfacfscmulgsum  20898  chfacfpmmul0  20900  chfacfpmmulgsum  20902  prdsmet  22408  metustexhalf  22594  nlmvscnlem2  22722  nlmvscnlem1  22723  nmo0  22772  evth  22991  lebnumlem1  22993  lebnumii  22998  htpycc  23012  pcohtpylem  23051  pcoass  23056  pcorevlem  23058  nmoleub2lem3  23147  ipcnlem2  23275  ipcnlem1  23276  rrxcph  23414  rrxmetlem  23424  rrxmet  23425  rrxdstprj1  23426  ehlbase  23428  minveclem3b  23433  minveclem6  23439  pjthlem1  23442  ovolicopnf  23527  ioorcl2  23575  volivth  23610  mbfposr  23655  i1fmulc  23706  itg1mulc  23707  itg1ge0a  23714  mbfi1flim  23726  itg2split  23752  itg2monolem1  23753  itg2monolem3  23755  itg2mono  23756  itg2cnlem2  23765  itgge0  23813  dvlip  23992  dvlipcn  23993  dveq0  23999  dv11cn  24000  dvlt0  24004  dvfsumge  24021  dgradd2  24260  plydivlem3  24286  mtest  24394  radcnvlem1  24403  radcnv0  24406  radcnvlt1  24408  radcnvle  24410  pserulm  24412  pserdvlem1  24417  pserdv  24419  abelthlem2  24422  abelthlem7  24428  pilem2  24442  pilem3  24443  coseq00topi  24491  tanabsge  24495  tanord1  24520  tanord  24521  rplogcl  24586  logdivle  24604  logcnlem3  24626  logcnlem4  24627  dvloglem  24630  logtayl  24642  abscxp2  24675  cxplt  24676  cxple  24677  cxple2a  24681  cxpcn3lem  24724  abscxpbnd  24730  chordthmlem5  24799  asinlem3  24834  atanre  24848  atanlogaddlem  24876  atanlogadd  24877  atanlogsublem  24878  atantan  24886  atans2  24894  efrlim  24932  cxp2limlem  24938  cxp2lim  24939  cxploglim2  24941  divsqrtsumlem  24942  jensenlem2  24950  harmonicubnd  24972  fsumharmonic  24974  dmlogdmgm  24986  lgamgulmlem1  24991  lgamgulmlem2  24992  ftalem1  25035  ftalem2  25036  ftalem5  25039  vmacl  25080  chtwordi  25118  ppiwordi  25124  chtrpcl  25137  fsumfldivdiaglem  25151  fsumvma2  25175  chpval2  25179  chpchtsum  25180  chpub  25181  logfacbnd3  25184  logexprlim  25186  mersenne  25188  lgsdilem  25285  lgsne0  25296  gausslemma2dlem1a  25326  lgseisen  25340  lgsquadlem1  25341  lgsquadlem2  25342  chebbnd1lem2  25395  chebbnd1lem3  25396  chebbnd1  25397  chtppilimlem1  25398  chtppilimlem2  25399  chtppilim  25400  chebbnd2  25402  chto1lb  25403  chpchtlim  25404  chpo1ub  25405  dchrisumlema  25413  dchrisumlem2  25415  dchrisumlem3  25416  dchrmusumlema  25418  dchrvmasumlem2  25423  dchrvmasumiflem1  25426  dchrisum0flblem1  25433  dchrisum0flblem2  25434  dchrisum0re  25438  dchrisum0lema  25439  dchrisum0  25445  dirith2  25453  mulog2sumlem1  25459  vmalogdivsum2  25463  log2sumbnd  25469  selberg2lem  25475  chpdifbndlem1  25478  chpdifbndlem2  25479  chpdifbnd  25480  selberg3lem1  25482  pntrmax  25489  pntrsumo1  25490  pntrlog2bndlem4  25505  pntrlog2bndlem5  25506  pntpbnd1a  25510  pntpbnd1  25511  pntpbnd2  25512  pntlemg  25523  pntlemj  25528  pntlemk  25531  pntlem3  25534  pntleml  25536  pnt2  25538  pnt  25539  ostth2lem1  25543  padicabv  25555  padicabvcxp  25557  ostth2lem3  25560  ostth2lem4  25561  ostth3  25563  trgcgrg  25646  tgcgr4  25662  axsegconlem7  26039  axsegconlem10  26042  axcontlem2  26081  axcontlem4  26083  axcontlem7  26086  axcontlem10  26089  crctcshwlkn0lem3  26955  crctcshwlkn0  26964  clwlkclwwlklem2a2  27158  clwlkclwwlklem2a  27163  wwlksubclwwlk  27231  frgrogt3nreg  27607  friendshipgt3  27608  minvecolem5  28087  minvecolem6  28088  htthlem  28124  pjhthlem1  28600  nndiffz1  29897  bcm1n  29903  2sqmod  29995  pnfneige0  30344  nexple  30418  indf1o  30433  measinb  30631  eulerpartlems  30769  eulerpartlemgc  30771  ballotlemfc0  30901  ballotlemfcc  30902  ballotlemodife  30906  sgnneg  30949  sgnmul  30951  sgnsub  30953  signsply0  30975  signslema  30986  signsvtp  31007  signshf  31012  itgexpif  31031  breprexplemc  31057  circlemeth  31065  logdivsqrle  31075  cvmliftlem2  31612  dnibndlem9  32814  unbdqndv2lem2  32839  knoppndvlem1  32841  knoppndvlem2  32842  knoppndvlem7  32847  knoppndvlem11  32851  knoppndvlem14  32854  knoppndvlem15  32855  knoppndvlem17  32857  knoppndvlem19  32859  knoppndvlem20  32860  bj-pinftynminfty  33449  poimirlem10  33750  poimirlem11  33751  poimirlem24  33764  poimirlem29  33769  poimirlem31  33771  poimirlem32  33772  poimir  33773  mblfinlem2  33778  bddiblnc  33810  ftc1anclem7  33821  ftc1anclem8  33822  ftc1anc  33823  areacirclem1  33830  areacirclem4  33833  areacirc  33835  geomcau  33884  isbnd3b  33913  prdsbnd  33921  bfp  33952  rrnequiv  33963  irrapxlem1  37905  irrapxlem2  37906  irrapxlem3  37907  irrapxlem4  37908  pellexlem6  37917  pell14qrgt0  37942  pell1qrgaplem  37956  pellfundex  37969  pellfundrp  37971  monotoddzzfi  38025  jm2.24  38048  jm2.23  38081  jm2.26lem3  38086  jm3.1lem3  38104  k0004ss2  38967  imo72b2lem1  38988  dvgrat  39028  hashnzfz2  39037  binomcxplemnn0  39065  binomcxplemnotnn0  39072  neglt  39995  divlt0gt0d  39997  upbdrech2  40020  xralrple2  40067  xralrple3  40087  fiminre2  40091  reclt0d  40104  reclt0  40110  xrpnf  40212  fsumnncl  40300  fsumsupp0  40307  sumnnodd  40359  lptre2pt  40369  limsupubuz  40442  liminfresre  40508  liminf0  40522  dvmptconst  40626  dvdivbd  40635  dvcosax  40638  dvbdfbdioolem1  40640  dvbdfbdioolem2  40641  ioodvbdlimc1lem1  40643  ioodvbdlimc1lem2  40644  ioodvbdlimc2lem  40646  dvxpaek  40652  dvnxpaek  40654  volioc  40684  volico  40696  stoweidlem1  40714  stoweidlem7  40720  stoweidlem11  40724  stoweidlem25  40738  stoweidlem26  40739  stoweidlem34  40747  stoweidlem36  40749  stoweidlem41  40754  stoweidlem42  40755  stoweidlem44  40757  stoweidlem45  40758  wallispilem3  40780  wallispilem4  40781  wallispi  40783  stirlinglem3  40789  stirlinglem5  40791  stirlinglem6  40792  stirlinglem7  40793  stirlinglem10  40796  stirlinglem11  40797  stirlinglem12  40798  dirkeritg  40815  dirkercncflem2  40817  fourierdlem9  40829  fourierdlem11  40831  fourierdlem12  40832  fourierdlem14  40834  fourierdlem15  40835  fourierdlem19  40839  fourierdlem24  40844  fourierdlem28  40848  fourierdlem30  40850  fourierdlem40  40860  fourierdlem41  40861  fourierdlem43  40863  fourierdlem44  40864  fourierdlem47  40866  fourierdlem50  40869  fourierdlem51  40870  fourierdlem57  40876  fourierdlem60  40879  fourierdlem61  40880  fourierdlem66  40885  fourierdlem68  40887  fourierdlem73  40892  fourierdlem74  40893  fourierdlem75  40894  fourierdlem78  40897  fourierdlem79  40898  fourierdlem83  40902  fourierdlem88  40907  fourierdlem92  40911  fourierdlem93  40912  fourierdlem97  40916  fourierdlem103  40922  fourierdlem104  40923  fourierdlem109  40928  fourierdlem111  40930  sqwvfoura  40941  sqwvfourb  40942  fourierswlem  40943  fouriersw  40944  elaa2lem  40946  etransclem4  40951  etransclem18  40965  etransclem19  40966  etransclem23  40970  etransclem27  40974  etransclem31  40978  etransclem32  40979  etransclem35  40982  etransclem41  40988  etransclem46  40993  etransclem48  40995  rrxtopnfi  41002  qndenserrnbllem  41010  salgencntex  41057  sge0tsms  41093  sge0isum  41140  volicorecl  41259  hoiprodcl  41260  ovnlerp  41275  ovnsubaddlem1  41283  hoiprodcl3  41293  volicore  41294  hoidmvcl  41295  hoidmvlelem1  41308  hoidmvlelem2  41309  hoidmvlelem3  41310  ovnhoi  41316  hoiqssbllem2  41336  volicorege0  41350  vonhoire  41385  pimrecltpos  41418  pimrecltneg  41432  smfmbfcex  41467  nsssmfmbflem  41485  smfrec  41495  smfmullem3  41499  sharhght  41553  zm1nn  41909  eluzge0nn0  41914  elfz2z  41917  2ffzoeq  41930  iccpartigtl  41951  iccpartgt  41955  expnegico01  42893  m1modmmod  42901  difmodm1lt  42902  regt1loggt0  42915  refdivmptf  42921  elbigolo1  42936  rege1logbrege0  42937  fllog2  42947  dignn0flhalflem1  42994  amgmwlem  43136
  Copyright terms: Public domain W3C validator