Theorem 0red 9920

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

Step	Hyp	Ref	Expression
1		0re 9919	. 2 ⊢ 0 ∈ ℝ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1977  ℝcr 9814  0cc0 9815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  gt0ne0  10372  add20  10419  subge0  10420  lesub0  10424  mulge0  10425  msqgt0  10427  msqge0  10428  addgt0d  10481  sublt0d  10532  prodgt0  10747  prodge0  10749  lt2msq1  10786  supmul1  10869  supmul  10872  0mnnnnn0  11202  nn0negleid  11222  rpgecl  11735  ge0p1rp  11738  ledivge1le  11777  mul2lt0rlt0  11808  mul2lt0rgt0  11809  mul2lt0bi  11812  max0sub  11901  reltxrnmnf  12043  infmrp1  12045  iccf1o  12187  xov1plusxeqvd  12189  elfz1b  12279  elfz0fzfz0  12313  fz0fzelfz0  12314  elfzo0z  12377  fzofzim  12382  fzo1fzo0n0  12386  elfzodifsumelfzo  12401  ssfzoulel  12428  elfznelfzo  12439  muladdmodid  12572  modltm1p1mod  12584  addmodlteq  12607  expgt1  12760  ltexp2a  12774  expcan  12775  ltexp2  12776  leexp2  12777  leexp2a  12778  expnlbnd2  12857  discr  12863  fi1uzind  13134  fi1uzindOLD  13140  ccatsymb  13219  ccat2s1fvw  13267  swrdnd  13284  swrdswrdlem  13311  swrdswrd  13312  swrdccatin2  13338  swrdccatin12lem3  13341  repswswrd  13382  swrd2lsw  13543  2swrd2eqwrdeq  13544  leabs  13887  max0add  13898  absgt0  13912  rlimrege0  14158  iseraltlem2  14261  fsumrecl  14312  o1fsum  14386  cvgcmp  14389  cvgcmpce  14391  geomulcvg  14446  mertenslem2  14456  fprodle  14566  rpnnen2lem4  14785  moddvds  14829  oddge22np1  14911  bitsfzolem  14994  bitsinv1lem  15001  sadcaddlem  15017  lcmgcdlem  15157  dvdsnprmd  15241  isprm7  15258  qnumgt0  15296  modprm0  15348  qexpz  15443  prmreclem4  15461  4sqlem6  15485  prmgaplem7  15599  gzrngunit  19631  regsumfsum  19633  regsumsupp  19787  fvmptnn04ifd  20477  chfacffsupp  20480  chfacfscmul0  20482  chfacfscmulgsum  20484  chfacfpmmul0  20486  chfacfpmmulgsum  20488  prdsmet  21985  metustexhalf  22171  nlmvscnlem2  22299  nlmvscnlem1  22300  nmo0  22349  evth  22566  lebnumlem1  22568  lebnumii  22573  htpycc  22587  pcohtpylem  22627  pcoass  22632  pcorevlem  22634  nmoleub2lem3  22723  ipcnlem2  22851  ipcnlem1  22852  rrxcph  22988  rrxmetlem  22998  rrxmet  22999  rrxdstprj1  23000  ehlbase  23002  minveclem3b  23007  minveclem6  23013  pjthlem1  23016  ovolicopnf  23099  ioorcl2  23146  volivth  23181  mbfposr  23225  i1fmulc  23276  itg1mulc  23277  itg1ge0a  23284  mbfi1flim  23296  itg2split  23322  itg2monolem1  23323  itg2monolem3  23325  itg2mono  23326  itg2cnlem2  23335  itgge0  23383  dvlip  23560  dvlipcn  23561  dveq0  23567  dv11cn  23568  dvlt0  23572  dvfsumge  23589  dgradd2  23828  plydivlem3  23854  mtest  23962  radcnvlem1  23971  radcnv0  23974  radcnvlt1  23976  radcnvle  23978  pserulm  23980  pserdvlem1  23985  pserdv  23987  abelthlem2  23990  abelthlem7  23996  pilem2  24010  coseq00topi  24058  tanabsge  24062  tanord1  24087  tanord  24088  rplogcl  24154  logdivle  24172  logcnlem3  24190  logcnlem4  24191  dvloglem  24194  logtayl  24206  abscxp2  24239  cxplt  24240  cxple  24241  cxple2a  24245  cxpcn3lem  24288  abscxpbnd  24294  chordthmlem5  24363  asinlem3  24398  atanre  24412  atanlogaddlem  24440  atanlogadd  24441  atanlogsublem  24442  atantan  24450  atans2  24458  efrlim  24496  cxp2limlem  24502  cxp2lim  24503  cxploglim2  24505  divsqrtsumlem  24506  jensenlem2  24514  harmonicubnd  24536  fsumharmonic  24538  dmlogdmgm  24550  lgamgulmlem1  24555  lgamgulmlem2  24556  ftalem1  24599  ftalem2  24600  ftalem5  24603  vmacl  24644  chtwordi  24682  ppiwordi  24688  chtrpcl  24701  fsumfldivdiaglem  24715  fsumvma2  24739  chpval2  24743  chpchtsum  24744  chpub  24745  logfacbnd3  24748  logexprlim  24750  mersenne  24752  lgslem4  24825  lgsdilem  24849  lgsne0  24860  gausslemma2dlem1a  24890  lgseisen  24904  lgsquadlem1  24905  lgsquadlem2  24906  chebbnd1lem2  24959  chebbnd1lem3  24960  chebbnd1  24961  chtppilimlem1  24962  chtppilimlem2  24963  chtppilim  24964  chebbnd2  24966  chto1lb  24967  chpchtlim  24968  chpo1ub  24969  dchrisumlema  24977  dchrisumlem2  24979  dchrisumlem3  24980  dchrmusumlema  24982  dchrvmasumlem2  24987  dchrvmasumiflem1  24990  dchrisum0flblem1  24997  dchrisum0flblem2  24998  dchrisum0re  25002  dchrisum0lema  25003  dchrisum0  25009  dirith2  25017  mulog2sumlem1  25023  vmalogdivsum2  25027  log2sumbnd  25033  selberg2lem  25039  chpdifbndlem1  25042  chpdifbndlem2  25043  chpdifbnd  25044  selberg3lem1  25046  pntrmax  25053  pntrsumo1  25054  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntlemg  25087  pntlemj  25092  pntlemk  25095  pntlem3  25098  pntleml  25100  pnt2  25102  pnt  25103  ostth2lem1  25107  padicabv  25119  padicabvcxp  25121  ostth2lem3  25124  ostth2lem4  25125  ostth3  25127  trgcgrg  25210  tgcgr4  25226  axsegconlem7  25603  axsegconlem10  25606  axcontlem2  25645  axcontlem4  25647  axcontlem7  25650  axcontlem10  25653  nvnencycllem  26171  clwwlkn0  26302  clwlkisclwwlklem2a2  26308  clwlkisclwwlklem2a  26313  wwlksubclwwlk  26332  frgraogt3nreg  26647  friendshipgt3  26648  minvecolem5  27121  minvecolem6  27122  htthlem  27158  pjhthlem1  27634  nndiffz1  28936  bcm1n  28941  2sqmod  28979  pnfneige0  29325  nexple  29399  indf1o  29413  measinb  29611  eulerpartlems  29749  eulerpartlemgc  29751  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemodife  29886  sgnneg  29929  sgnmul  29931  sgnsub  29933  signsply0  29954  signslema  29965  signsvtp  29986  signshf  29991  cvmliftlem2  30522  dnibndlem9  31646  unbdqndv2lem2  31671  knoppndvlem1  31673  knoppndvlem2  31674  knoppndvlem7  31679  knoppndvlem11  31683  knoppndvlem14  31686  knoppndvlem15  31687  knoppndvlem17  31689  knoppndvlem19  31691  knoppndvlem20  31692  bj-pinftynminfty  32291  poimirlem10  32589  poimirlem11  32590  poimirlem24  32603  poimirlem29  32608  poimirlem31  32610  poimirlem32  32611  poimir  32612  mblfinlem2  32617  bddiblnc  32650  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  areacirclem1  32670  areacirclem4  32673  areacirc  32675  geomcau  32725  isbnd3b  32754  prdsbnd  32762  bfp  32793  rrnequiv  32804  irrapxlem1  36404  irrapxlem2  36405  irrapxlem3  36406  irrapxlem4  36407  pellexlem6  36416  pell14qrgt0  36441  pell1qrgaplem  36455  pellfundex  36468  pellfundrp  36470  monotoddzzfi  36525  jm2.24  36548  jm2.23  36581  jm2.26lem3  36586  jm3.1lem3  36604  k0004ss2  37470  imo72b2lem1  37493  dvgrat  37533  hashnzfz2  37542  binomcxplemnn0  37570  binomcxplemnotnn0  37577  neglt  38437  divlt0gt0d  38439  upbdrech2  38463  xralrple2  38511  xralrple3  38531  fiminre2  38535  reclt0d  38548  reclt0  38555  fsumnncl  38638  fsumsupp0  38645  sumnnodd  38697  lptre2pt  38707  dvmptconst  38803  dvdivbd  38813  dvcosax  38816  dvbdfbdioolem1  38818  dvbdfbdioolem2  38819  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvxpaek  38830  dvnxpaek  38832  volioc  38864  volico  38876  stoweidlem1  38894  stoweidlem7  38900  stoweidlem11  38904  stoweidlem25  38918  stoweidlem26  38919  stoweidlem34  38927  stoweidlem36  38929  stoweidlem41  38934  stoweidlem42  38935  stoweidlem44  38937  stoweidlem45  38938  wallispilem3  38960  wallispilem4  38961  wallispi  38963  stirlinglem3  38969  stirlinglem5  38971  stirlinglem6  38972  stirlinglem7  38973  stirlinglem10  38976  stirlinglem11  38977  stirlinglem12  38978  dirkeritg  38995  dirkercncflem2  38997  fourierdlem9  39009  fourierdlem11  39011  fourierdlem12  39012  fourierdlem14  39014  fourierdlem15  39015  fourierdlem19  39019  fourierdlem24  39024  fourierdlem28  39028  fourierdlem30  39030  fourierdlem40  39040  fourierdlem41  39041  fourierdlem43  39043  fourierdlem44  39044  fourierdlem47  39046  fourierdlem50  39049  fourierdlem51  39050  fourierdlem57  39056  fourierdlem60  39059  fourierdlem61  39060  fourierdlem66  39065  fourierdlem68  39067  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem78  39077  fourierdlem79  39078  fourierdlem83  39082  fourierdlem88  39087  fourierdlem92  39091  fourierdlem93  39092  fourierdlem97  39096  fourierdlem103  39102  fourierdlem104  39103  fourierdlem109  39108  fourierdlem111  39110  sqwvfoura  39121  sqwvfourb  39122  fourierswlem  39123  fouriersw  39124  elaa2lem  39126  etransclem4  39131  etransclem18  39145  etransclem19  39146  etransclem23  39150  etransclem27  39154  etransclem31  39158  etransclem32  39159  etransclem35  39162  etransclem41  39168  etransclem46  39173  etransclem48  39175  rrxtopnfi  39182  qndenserrnbllem  39190  salgencntex  39237  sge0tsms  39273  sge0isum  39320  volicorecl  39436  hoiprodcl  39437  ovnlerp  39452  ovnsubaddlem1  39460  hoiprodcl3  39470  volicore  39471  hoidmvcl  39472  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  ovnhoi  39493  hoiqssbllem2  39513  volicorege0  39527  vonhoire  39563  pimrecltpos  39596  pimrecltneg  39610  smfmbfcex  39646  nsssmfmbflem  39664  smfrec  39674  smfmullem3  39678  sharhght  39703  iccpartigtl  39961  iccpartgt  39965  zm1nn  40348  eluzge0nn0  40350  elfz2z  40352  2ffzoeq  40361  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0  41024  clwlkclwwlklem2a2  41202  clwlkclwwlklem2a  41207  wwlksubclwwlks  41232  av-frgraogt3nreg  41551  av-friendshipgt3  41552  expnegico01  42102  m1modmmod  42110  difmodm1lt  42111  regt1loggt0  42128  refdivmptf  42134  elbigolo1  42149  rege1logbrege0  42150  fllog2  42160  dignn0flhalflem1  42207  amgmwlem  42357