Theorem 0red 10987

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

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 10879  0cc0 10880

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 2710  ax-1cn 10938  ax-addrcl 10941  ax-rnegex 10951  ax-cnre 10953

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071

This theorem is referenced by:  gt0ne0  11449  add20  11496  subge0  11497  lesub0  11501  mulge0  11502  msqgt0  11504  msqge0  11505  addgt0d  11559  sublt0d  11610  prodgt0  11831  lt2msq1  11868  fiminre2  11932  supmul1  11953  supmul  11956  nnne0  12016  0mnnnnn0  12274  nn0negleid  12294  rpgecl  12767  ge0p1rp  12770  ledivge1le  12810  mul2lt0rlt0  12841  mul2lt0rgt0  12842  mul2lt0bi  12845  prodge0rd  12846  max0sub  12939  reltxrnmnf  13085  infmrp1  13087  lincmb01cmp  13236  iccf1o  13237  xov1plusxeqvd  13239  elfz0fzfz0  13370  fz0fzelfz0  13371  elfzo0z  13438  fzofzim  13443  fzo1fzo0n0  13447  elfzodifsumelfzo  13462  ssfzoulel  13490  elfznelfzo  13501  muladdmodid  13640  modltm1p1mod  13652  addmodlteq  13675  expgt1  13830  ltexp2a  13893  expcan  13896  ltexp2  13897  leexp2  13898  leexp2a  13899  expnlbnd2  13958  discr  13964  fi1uzind  14220  ccatsymb  14296  ccat2s1fvw  14358  ccat2s1fvwOLD  14359  swrdnd  14376  swrdnnn0nd  14378  swrdswrdlem  14426  swrdswrd  14427  repswswrd  14506  swrd2lsw  14674  2swrd2eqwrdeq  14675  leabs  15020  max0add  15031  absgt0  15045  rlimrege0  15297  iseraltlem2  15403  fsumrecl  15455  o1fsum  15534  cvgcmp  15537  cvgcmpce  15539  geomulcvg  15597  mertenslem2  15606  fprodle  15715  rpnnen2lem4  15935  p1modz1  15979  moddvds  15983  oddge22np1  16067  bitsfzolem  16150  bitsinv1lem  16157  sadcaddlem  16173  lcmgcdlem  16320  dvdsnprmd  16404  2mulprm  16407  isprm7  16422  qnumgt0  16463  modprm0  16515  qexpz  16611  prmreclem4  16629  4sqlem6  16653  prmgaplem7  16767  gzrngunit  20673  regsumfsum  20675  regsumsupp  20836  fvmptnn04ifd  22011  chfacffsupp  22014  chfacfscmul0  22016  chfacfscmulgsum  22018  chfacfpmmul0  22020  chfacfpmmulgsum  22022  prdsmet  23532  metustexhalf  23721  nlmvscnlem2  23858  nlmvscnlem1  23859  nmo0  23908  blcvx  23970  evth  24131  lebnumlem1  24133  lebnumii  24138  htpycc  24152  pcohtpylem  24191  pcoass  24196  pcorevlem  24198  nmoleub2lem3  24287  ipcnlem2  24417  ipcnlem1  24418  rrxcph  24565  rrxmetlem  24580  rrxmet  24581  rrxdstprj1  24582  ehlbase  24588  minveclem3b  24601  minveclem6  24607  pjthlem1  24610  ovolicopnf  24697  ioorcl2  24745  volivth  24780  mbfposr  24825  i1fmulc  24877  itg1mulc  24878  itg1ge0a  24885  mbfi1flim  24897  itg2split  24923  itg2monolem1  24924  itg2monolem3  24926  itg2mono  24927  itg2cnlem2  24936  itgge0  24984  bddiblnc  25015  dvlip  25166  dvlipcn  25167  dveq0  25173  dv11cn  25174  dvlt0  25178  dvfsumge  25195  dgradd2  25438  plydivlem3  25464  mtest  25572  radcnvlem1  25581  radcnv0  25584  radcnvlt1  25586  radcnvle  25588  pserulm  25590  pserdvlem1  25595  pserdv  25597  abelthlem2  25600  abelthlem7  25606  pilem2  25620  pilem3  25621  coseq00topi  25668  tanabsge  25672  cosq34lt1  25692  tanord1  25702  tanord  25703  rplogcl  25768  logdivle  25786  logcnlem3  25808  logcnlem4  25809  dvloglem  25812  logtayl  25824  abscxp2  25857  cxplt  25858  cxple  25859  cxple2a  25863  cxpcn3lem  25909  abscxpbnd  25915  chordthmlem4  25994  chordthmlem5  25995  asinlem3  26030  atanre  26044  atanlogaddlem  26072  atanlogadd  26073  atanlogsublem  26074  atantan  26082  atans2  26090  efrlim  26128  cxp2limlem  26134  cxp2lim  26135  cxploglim2  26137  divsqrtsumlem  26138  jensenlem2  26146  harmonicubnd  26168  fsumharmonic  26170  dmlogdmgm  26182  lgamgulmlem1  26187  lgamgulmlem2  26188  ftalem1  26231  ftalem2  26232  ftalem5  26235  vmacl  26276  chtwordi  26314  ppiwordi  26320  chtrpcl  26333  fsumfldivdiaglem  26347  fsumvma2  26371  chpval2  26375  chpchtsum  26376  chpub  26377  logfacbnd3  26380  logexprlim  26382  mersenne  26384  lgsdilem  26481  lgsne0  26492  gausslemma2dlem1a  26522  lgseisen  26536  lgsquadlem1  26537  lgsquadlem2  26538  2sqmod  26593  2sqnn0  26595  chebbnd1lem2  26627  chebbnd1lem3  26628  chebbnd1  26629  chtppilimlem1  26630  chtppilimlem2  26631  chtppilim  26632  chebbnd2  26634  chto1lb  26635  chpchtlim  26636  chpo1ub  26637  dchrisumlema  26645  dchrisumlem2  26647  dchrisumlem3  26648  dchrmusumlema  26650  dchrvmasumlem2  26655  dchrvmasumiflem1  26658  dchrisum0flblem1  26665  dchrisum0flblem2  26666  dchrisum0re  26670  dchrisum0lema  26671  dchrisum0  26677  dirith2  26685  mulog2sumlem1  26691  vmalogdivsum2  26695  log2sumbnd  26701  selberg2lem  26707  chpdifbndlem1  26710  chpdifbnd  26712  selberg3lem1  26714  pntrmax  26721  pntrsumo1  26722  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntpbnd1a  26742  pntpbnd1  26743  pntpbnd2  26744  pntlemg  26755  pntlemj  26760  pntlemk  26763  pntlem3  26766  pnt2  26770  pnt  26771  ostth2lem1  26775  padicabv  26787  padicabvcxp  26789  ostth2lem3  26792  ostth2lem4  26793  ostth3  26795  trgcgrg  26885  tgcgr4  26901  axsegconlem7  27300  axsegconlem10  27303  axcontlem2  27342  axcontlem4  27344  axcontlem7  27347  axcontlem10  27350  crctcshwlkn0lem3  28186  crctcshwlkn0  28195  clwlkclwwlklem2a2  28366  clwlkclwwlklem2a  28371  wwlksubclwwlk  28431  frgrogt3nreg  28770  friendshipgt3  28771  minvecolem5  29252  minvecolem6  29253  htthlem  29288  pjhthlem1  29762  nndiffz1  31116  bcm1n  31125  wrdt2ind  31234  cycpmrn  31419  cyc3conja  31433  ccfldextdgrr  31751  pnfneige0  31910  nexple  31986  indf1o  32001  measinb  32198  eulerpartlems  32336  eulerpartlemgc  32338  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemodife  32473  sgnneg  32516  sgnmul  32518  sgnsub  32520  signsply0  32539  signslema  32550  signsvtp  32571  itgexpif  32595  breprexplemc  32621  circlemeth  32629  logdivsqrle  32639  0nn0m1nnn0  33080  cvmliftlem2  33257  dnibndlem9  34675  unbdqndv2lem2  34699  knoppndvlem1  34701  knoppndvlem2  34702  knoppndvlem7  34707  knoppndvlem11  34711  knoppndvlem14  34714  knoppndvlem15  34715  knoppndvlem17  34717  knoppndvlem19  34719  knoppndvlem20  34720  bj-pinftynminfty  35407  poimirlem10  35796  poimirlem11  35797  poimirlem24  35810  poimirlem29  35815  poimirlem31  35817  poimirlem32  35818  poimir  35819  mblfinlem2  35824  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  areacirclem1  35874  areacirclem4  35877  areacirc  35879  geomcau  35926  isbnd3b  35952  prdsbnd  35960  bfp  35991  rrnequiv  36002  resdvopclptsd  40043  lcmineqlem2  40045  lcmineqlem3  40046  lcmineqlem10  40053  lcmineqlem12  40055  lcmineqlem23  40066  3lexlogpow5ineq1  40069  3lexlogpow5ineq2  40070  3lexlogpow5ineq4  40071  3lexlogpow5ineq3  40072  3lexlogpow2ineq2  40074  3lexlogpow5ineq5  40075  aks4d1lem1  40077  dvrelog2  40079  dvrelog3  40080  dvrelog2b  40081  0nonelalab  40082  dvrelogpow2b  40083  aks4d1p1p3  40084  aks4d1p1p2  40085  aks4d1p1p4  40086  aks4d1p1p6  40088  aks4d1p1p7  40089  aks4d1p1p5  40090  aks4d1p1  40091  aks4d1p2  40092  aks4d1p3  40093  aks4d1p5  40095  aks4d1p6  40096  aks4d1p7d1  40097  aks4d1p7  40098  aks4d1p8d2  40100  aks4d1p8d3  40101  aks4d1p8  40102  aks4d1p9  40103  2np3bcnp1  40107  2ap1caineq  40108  sticksstones7  40115  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  sticksstones22  40131  metakunt2  40133  metakunt29  40160  sn-1ne2  40302  oexpreposd  40328  nn0rppwr  40340  nn0expgcd  40342  posqsqznn  40350  rtprmirr  40354  re1m1e0m0  40387  re0m0e0  40392  remul01  40397  mulgt0con1dlem  40434  mulgt0b2d  40437  dffltz  40478  3cubeslem1  40513  irrapxlem1  40651  irrapxlem2  40652  irrapxlem3  40653  irrapxlem4  40654  pellexlem6  40663  pell14qrgt0  40688  pell1qrgaplem  40702  pellfundex  40715  pellfundrp  40717  monotoddzzfi  40771  jm2.24  40792  jm2.23  40825  jm2.26lem3  40830  jm3.1lem3  40848  sqrtcvallem1  41246  reabsifneg  41247  reabsifpos  41249  sqrtcval  41256  k0004ss2  41769  imo72b2lem1  41787  dvgrat  41937  hashnzfz2  41946  binomcxplemnn0  41974  binomcxplemnotnn0  41981  neglt  42830  divlt0gt0d  42832  upbdrech2  42854  xralrple2  42900  xralrple3  42920  reclt0d  42933  reclt0  42938  xrpnf  43033  fsumnncl  43120  fsumsupp0  43126  sumnnodd  43178  lptre2pt  43188  limsupubuz  43261  liminfresre  43327  liminf0  43341  dvmptconst  43463  dvdivbd  43471  dvcosax  43474  dvbdfbdioolem1  43476  dvbdfbdioolem2  43477  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvxpaek  43488  dvnxpaek  43490  volioc  43520  volico  43531  stoweidlem1  43549  stoweidlem7  43555  stoweidlem11  43559  stoweidlem25  43573  stoweidlem26  43574  stoweidlem34  43582  stoweidlem36  43584  stoweidlem41  43589  stoweidlem42  43590  stoweidlem44  43592  stoweidlem45  43593  wallispilem3  43615  wallispilem4  43616  wallispi  43618  stirlinglem3  43624  stirlinglem5  43626  stirlinglem6  43627  stirlinglem7  43628  stirlinglem10  43631  stirlinglem11  43632  stirlinglem12  43633  dirkeritg  43650  dirkercncflem2  43652  fourierdlem9  43664  fourierdlem11  43666  fourierdlem12  43667  fourierdlem14  43669  fourierdlem15  43670  fourierdlem19  43674  fourierdlem24  43679  fourierdlem28  43683  fourierdlem30  43685  fourierdlem40  43695  fourierdlem41  43696  fourierdlem43  43698  fourierdlem44  43699  fourierdlem47  43701  fourierdlem50  43704  fourierdlem51  43705  fourierdlem57  43711  fourierdlem60  43714  fourierdlem61  43715  fourierdlem66  43720  fourierdlem68  43722  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem78  43732  fourierdlem79  43733  fourierdlem83  43737  fourierdlem88  43742  fourierdlem92  43746  fourierdlem93  43747  fourierdlem97  43751  fourierdlem103  43757  fourierdlem104  43758  fourierdlem109  43763  fourierdlem111  43765  sqwvfoura  43776  sqwvfourb  43777  fourierswlem  43778  fouriersw  43779  elaa2lem  43781  etransclem4  43786  etransclem18  43800  etransclem19  43801  etransclem23  43805  etransclem27  43809  etransclem31  43813  etransclem32  43814  etransclem35  43817  etransclem41  43823  etransclem46  43828  etransclem48  43830  rrxtopnfi  43835  qndenserrnbllem  43842  salgencntex  43889  sge0tsms  43925  sge0isum  43972  volicorecl  44091  hoiprodcl  44092  ovnlerp  44107  ovnsubaddlem1  44115  hoiprodcl3  44125  volicore  44126  hoidmvcl  44127  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem3  44142  ovnhoi  44148  hoiqssbllem2  44168  volicorege0  44182  vonhoire  44217  pimrecltpos  44253  pimrecltneg  44269  smfmbfcex  44305  nsssmfmbflem  44323  smfrec  44334  smfmullem3  44338  sharhght  44392  zm1nn  44805  eluzge0nn0  44815  elfz2z  44818  2ffzoeq  44831  iccpartigtl  44886  iccpartgt  44890  requad01  45084  requad1  45085  requad2  45086  expnegico01  45870  m1modmmod  45878  difmodm1lt  45879  regt1loggt0  45893  refdivmptf  45899  elbigolo1  45914  rege1logbrege0  45915  fllog2  45925  dignn0flhalflem1  45972  eenglngeehlnmlem2  46095  line2  46109  line2xlem  46110  line2x  46111  line2y  46112  itsclc0yqsol  46121  2itscp  46138  inlinecirc02plem  46143  amgmwlem  46517  natglobalincr  46523  upwordnul  46526