Theorem 0red 11135

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 11134	. 2 ⊢ 0 ∈ ℝ
2	1	a1i 11	1 ⊢ (𝜑 → 0 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11025  0cc0 11026

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-addrcl 11087  ax-rnegex 11097  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811  df-rex 3061

This theorem is referenced by:  gt0ne0  11602  add20  11649  subge0  11650  lesub0  11654  mulge0  11655  msqgt0  11657  msqge0  11658  gt0ne0d  11701  addgt0d  11712  sublt0d  11763  prodgt0  11988  mulgt1  12003  lt2msq1  12026  fiminre2  12090  supmul1  12111  supmul  12114  nnne0  12179  0mnnnnn0  12433  nn0negleid  12453  neglt  12925  rpgecl  12935  ge0p1rp  12938  ledivge1le  12978  mul2lt0rlt0  13009  mul2lt0rgt0  13010  mul2lt0bi  13013  prodge0rd  13014  max0sub  13111  reltxrnmnf  13258  infmrp1  13260  lincmb01cmp  13411  iccf1o  13412  xov1plusxeqvd  13414  elfz0fzfz0  13549  fz0fzelfz0  13550  elfzo0z  13617  fzofzim  13625  fzo1fzo0n0  13631  elfzodifsumelfzo  13647  ssfzoulel  13676  elfznelfzo  13689  muladdmodid  13833  modltm1p1mod  13846  addmodlteq  13869  expgt1  14023  ltexp2a  14089  expcan  14092  ltexp2  14093  leexp2  14094  leexp2a  14095  zzlesq  14129  expnlbnd2  14157  discr  14163  fi1uzind  14430  ccatsymb  14506  ccat2s1fvw  14562  swrdnd  14578  swrdnnn0nd  14580  swrdswrdlem  14627  swrdswrd  14628  repswswrd  14707  swrd2lsw  14875  2swrd2eqwrdeq  14876  leabs  15222  max0add  15233  absgt0  15248  rlimrege0  15502  iseraltlem2  15606  fsumrecl  15657  o1fsum  15736  cvgcmp  15739  cvgcmpce  15741  geomulcvg  15799  mertenslem2  15808  fprodle  15919  rpnnen2lem4  16142  p1modz1  16186  moddvds  16190  oddge22np1  16276  bitsfzolem  16361  bitsinv1lem  16368  sadcaddlem  16384  nn0rppwr  16488  nn0expgcd  16491  lcmgcdlem  16533  dvdsnprmd  16617  2mulprm  16620  isprm7  16635  qnumgt0  16677  modprm0  16733  qexpz  16829  prmreclem4  16847  4sqlem6  16871  prmgaplem7  16985  gzrngunit  21388  regsumfsum  21390  regsumsupp  21577  fvmptnn04ifd  22797  chfacffsupp  22800  chfacfscmul0  22802  chfacfscmulgsum  22804  chfacfpmmul0  22806  chfacfpmmulgsum  22808  prdsmet  24314  metustexhalf  24500  nlmvscnlem2  24629  nlmvscnlem1  24630  nmo0  24679  blcvx  24742  iihalf1cn  24882  evth  24914  lebnumlem1  24916  lebnumii  24921  htpycc  24935  pcohtpylem  24975  pcoass  24980  pcorevlem  24982  nmoleub2lem3  25071  ipcnlem2  25200  ipcnlem1  25201  rrxcph  25348  rrxmetlem  25363  rrxmet  25364  rrxdstprj1  25365  ehlbase  25371  minveclem3b  25384  minveclem6  25390  pjthlem1  25393  ovolicopnf  25481  ioorcl2  25529  volivth  25564  mbfposr  25609  i1fmulc  25660  itg1mulc  25661  itg1ge0a  25668  mbfi1flim  25680  itg2split  25706  itg2monolem1  25707  itg2monolem3  25709  itg2mono  25710  itg2cnlem2  25719  itgge0  25768  bddiblnc  25799  dvlip  25954  dvlipcn  25955  dveq0  25961  dv11cn  25962  dvlt0  25966  dvfsumge  25984  dgradd2  26230  plydivlem3  26259  mtest  26369  radcnvlem1  26378  radcnv0  26381  radcnvlt1  26383  radcnvle  26385  pserulm  26387  pserdvlem1  26393  pserdv  26395  abelthlem2  26398  abelthlem7  26404  pilem2  26418  pilem3  26419  coseq00topi  26467  tanabsge  26471  cosq34lt1  26492  tanord1  26502  tanord  26503  rplogcl  26569  logdivle  26587  logcnlem3  26609  logcnlem4  26610  dvloglem  26613  logtayl  26625  abscxp2  26658  cxplt  26659  cxple  26660  cxple2a  26664  cxpcn3lem  26713  abscxpbnd  26719  rtprmirr  26726  chordthmlem4  26801  chordthmlem5  26802  asinlem3  26837  atanre  26851  atanlogaddlem  26879  atanlogadd  26880  atanlogsublem  26881  atantan  26889  atans2  26897  efrlim  26935  efrlimOLD  26936  cxp2limlem  26942  cxp2lim  26943  cxploglim2  26945  divsqrtsumlem  26946  jensenlem2  26954  harmonicubnd  26976  fsumharmonic  26978  dmlogdmgm  26990  lgamgulmlem1  26995  lgamgulmlem2  26996  ftalem1  27039  ftalem2  27040  ftalem5  27043  vmacl  27084  chtwordi  27122  ppiwordi  27128  chtrpcl  27141  fsumfldivdiaglem  27155  fsumvma2  27181  chpval2  27185  chpchtsum  27186  chpub  27187  logfacbnd3  27190  logexprlim  27192  mersenne  27194  lgsdilem  27291  lgsne0  27302  gausslemma2dlem1a  27332  lgseisen  27346  lgsquadlem1  27347  lgsquadlem2  27348  2sqmod  27403  2sqnn0  27405  chebbnd1lem2  27437  chebbnd1lem3  27438  chebbnd1  27439  chtppilimlem1  27440  chtppilimlem2  27441  chtppilim  27442  chebbnd2  27444  chto1lb  27445  chpchtlim  27446  chpo1ub  27447  dchrisumlema  27455  dchrisumlem2  27457  dchrisumlem3  27458  dchrmusumlema  27460  dchrvmasumlem2  27465  dchrvmasumiflem1  27468  dchrisum0flblem1  27475  dchrisum0flblem2  27476  dchrisum0re  27480  dchrisum0lema  27481  dchrisum0  27487  dirith2  27495  mulog2sumlem1  27501  vmalogdivsum2  27505  log2sumbnd  27511  selberg2lem  27517  chpdifbndlem1  27520  chpdifbnd  27522  selberg3lem1  27524  pntrmax  27531  pntrsumo1  27532  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntpbnd1a  27552  pntpbnd1  27553  pntpbnd2  27554  pntlemg  27565  pntlemj  27570  pntlemk  27573  pntlem3  27576  pnt2  27580  pnt  27581  ostth2lem1  27585  padicabv  27597  padicabvcxp  27599  ostth2lem3  27602  ostth2lem4  27603  ostth3  27605  trgcgrg  28587  tgcgr4  28603  axsegconlem7  28996  axsegconlem10  28999  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  axcontlem10  29046  crctcshwlkn0lem3  29885  crctcshwlkn0  29894  clwlkclwwlklem2a2  30068  clwlkclwwlklem2a  30073  wwlksubclwwlk  30133  frgrogt3nreg  30472  friendshipgt3  30473  minvecolem5  30956  minvecolem6  30957  htthlem  30992  pjhthlem1  31466  sgnval2  32814  nndiffz1  32866  bcm1n  32875  fzo0opth  32883  expgt0b  32897  sgnneg  32914  sgnmul  32916  sgnsub  32918  nexple  32925  oexpled  32928  indf1o  32946  wrdt2ind  33035  cycpmrn  33225  cyc3conja  33239  ccfldextdgrr  33829  constrsslem  33898  constrresqrtcl  33934  constrsqrtcl  33936  cos9thpiminplylem1  33939  pnfneige0  34108  measinb  34378  eulerpartlems  34517  eulerpartlemgc  34519  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemodife  34655  signsply0  34708  signslema  34719  signsvtp  34740  itgexpif  34763  breprexplemc  34789  circlemeth  34797  logdivsqrle  34807  0nn0m1nnn0  35307  cvmliftlem2  35480  dnibndlem9  36686  unbdqndv2lem2  36710  knoppndvlem1  36712  knoppndvlem2  36713  knoppndvlem7  36718  knoppndvlem11  36722  knoppndvlem14  36725  knoppndvlem15  36726  knoppndvlem17  36728  knoppndvlem19  36730  knoppndvlem20  36731  bj-pinftynminfty  37428  poimirlem10  37827  poimirlem11  37828  poimirlem24  37841  poimirlem29  37846  poimirlem31  37848  poimirlem32  37849  poimir  37850  mblfinlem2  37855  ftc1anclem7  37896  ftc1anclem8  37897  ftc1anc  37898  areacirclem1  37905  areacirclem4  37908  areacirc  37910  geomcau  37956  isbnd3b  37982  prdsbnd  37990  bfp  38021  rrnequiv  38032  resdvopclptsd  42278  lcmineqlem2  42280  lcmineqlem3  42281  lcmineqlem10  42288  lcmineqlem12  42290  lcmineqlem23  42301  3lexlogpow5ineq1  42304  3lexlogpow5ineq2  42305  3lexlogpow5ineq4  42306  3lexlogpow5ineq3  42307  3lexlogpow2ineq2  42309  3lexlogpow5ineq5  42310  aks4d1lem1  42312  dvrelog2  42314  dvrelog3  42315  dvrelog2b  42316  0nonelalab  42317  dvrelogpow2b  42318  aks4d1p1p3  42319  aks4d1p1p2  42320  aks4d1p1p4  42321  aks4d1p1p6  42323  aks4d1p1p7  42324  aks4d1p1p5  42325  aks4d1p1  42326  aks4d1p2  42327  aks4d1p3  42328  aks4d1p5  42330  aks4d1p6  42331  aks4d1p7d1  42332  aks4d1p7  42333  aks4d1p8d2  42335  aks4d1p8d3  42336  aks4d1p8  42337  aks4d1p9  42338  posbezout  42350  primrootspoweq0  42356  aks6d1c1  42366  hashscontpow1  42371  aks6d1c2lem4  42377  aks6d1c5lem2  42388  deg1gprod  42390  2np3bcnp1  42394  2ap1caineq  42395  sticksstones7  42402  sticksstones10  42405  sticksstones12a  42407  sticksstones12  42408  sticksstones22  42418  aks6d1c6lem3  42422  bcled  42428  bcle2d  42429  aks6d1c7lem1  42430  aks6d1c7lem2  42431  aks6d1c7  42434  aks5lem6  42442  unitscyglem5  42449  aks5lem8  42451  sn-1ne2  42516  oexpreposd  42573  posqsqznn  42587  redvmptabs  42611  readvrec  42613  re1m1e0m0  42648  re0m0e0  42653  remul01  42658  sn-remul0ord  42659  remulneg2d  42666  sn-addlt0d  42709  sn-addgt0d  42710  renegmulnnass  42716  zmulcomlem  42718  mulgt0con1dlem  42720  sn-mulgt1d  42730  mulltgt0d  42733  mullt0b2d  42735  sn-mullt0d  42736  sn-msqgt0d  42737  fimgmcyc  42785  dffltz  42873  3cubeslem1  42922  irrapxlem1  43060  irrapxlem2  43061  irrapxlem3  43062  irrapxlem4  43063  pellexlem6  43072  pell14qrgt0  43097  pell1qrgaplem  43111  pellfundex  43124  pellfundrp  43126  monotoddzzfi  43180  jm2.24  43201  jm2.23  43234  jm2.26lem3  43239  jm3.1lem3  43257  sqrtcvallem1  43868  reabsifneg  43869  reabsifpos  43871  sqrtcval  43878  k0004ss2  44389  imo72b2lem1  44406  dvgrat  44549  hashnzfz2  44558  binomcxplemnn0  44586  binomcxplemnotnn0  44593  divlt0gt0d  45530  upbdrech2  45552  xralrple2  45595  xralrple3  45614  reclt0d  45627  reclt0  45631  xrpnf  45725  fsumnncl  45814  fsumsupp0  45820  sumnnodd  45872  lptre2pt  45880  limsupubuz  45953  liminfresre  46019  liminf0  46033  dvmptconst  46155  dvdivbd  46163  dvcosax  46166  dvbdfbdioolem1  46168  dvbdfbdioolem2  46169  ioodvbdlimc1lem1  46171  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  dvxpaek  46180  dvnxpaek  46182  volioc  46212  volico  46223  stoweidlem1  46241  stoweidlem7  46247  stoweidlem11  46251  stoweidlem25  46265  stoweidlem26  46266  stoweidlem34  46274  stoweidlem36  46276  stoweidlem41  46281  stoweidlem42  46282  stoweidlem44  46284  stoweidlem45  46285  wallispilem3  46307  wallispilem4  46308  wallispi  46310  stirlinglem3  46316  stirlinglem5  46318  stirlinglem6  46319  stirlinglem7  46320  stirlinglem10  46323  stirlinglem11  46324  stirlinglem12  46325  dirkeritg  46342  dirkercncflem2  46344  fourierdlem9  46356  fourierdlem11  46358  fourierdlem12  46359  fourierdlem14  46361  fourierdlem15  46362  fourierdlem19  46366  fourierdlem24  46371  fourierdlem28  46375  fourierdlem30  46377  fourierdlem40  46387  fourierdlem41  46388  fourierdlem43  46390  fourierdlem44  46391  fourierdlem47  46393  fourierdlem50  46396  fourierdlem51  46397  fourierdlem57  46403  fourierdlem60  46406  fourierdlem61  46407  fourierdlem66  46412  fourierdlem68  46414  fourierdlem73  46419  fourierdlem74  46420  fourierdlem75  46421  fourierdlem78  46424  fourierdlem79  46425  fourierdlem83  46429  fourierdlem88  46434  fourierdlem92  46438  fourierdlem93  46439  fourierdlem97  46443  fourierdlem103  46449  fourierdlem104  46450  fourierdlem109  46455  fourierdlem111  46457  sqwvfoura  46468  sqwvfourb  46469  fourierswlem  46470  fouriersw  46471  elaa2lem  46473  etransclem4  46478  etransclem18  46492  etransclem19  46493  etransclem23  46497  etransclem27  46501  etransclem31  46505  etransclem32  46506  etransclem35  46509  etransclem41  46515  etransclem46  46520  etransclem48  46522  rrxtopnfi  46527  qndenserrnbllem  46534  salgencntex  46583  sge0tsms  46620  sge0isum  46667  volicorecl  46786  hoiprodcl  46787  ovnlerp  46802  ovnsubaddlem1  46810  hoiprodcl3  46820  volicore  46821  hoidmvcl  46822  hoidmvlelem1  46835  hoidmvlelem2  46836  hoidmvlelem3  46837  ovnhoi  46843  hoiqssbllem2  46863  volicorege0  46877  vonhoire  46912  pimrecltpos  46948  pimrecltneg  46964  smfmbfcex  47000  nsssmfmbflem  47018  smfrec  47029  smfmullem3  47033  smfdivdmmbl  47078  sharhght  47105  et-sqrtnegnre  47113  ormkglobd  47115  natglobalincr  47117  chnsubseqwl  47119  zm1nn  47544  eluzge0nn0  47554  elfz2z  47557  2ffzoeq  47569  m1modmmod  47600  modm1p1ne  47612  iccpartigtl  47665  iccpartgt  47669  requad01  47863  requad1  47864  requad2  47865  stgrusgra  48201  gpgedgvtx1  48304  expnegico01  48760  regt1loggt0  48778  refdivmptf  48784  elbigolo1  48799  rege1logbrege0  48800  fllog2  48810  dignn0flhalflem1  48857  eenglngeehlnmlem2  48980  line2  48994  line2xlem  48995  line2x  48996  line2y  48997  itsclc0yqsol  49006  2itscp  49023  inlinecirc02plem  49028  amgmwlem  50043