Theorem 0red 11147

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  0cc0 11038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096  ax-addrcl 11099  ax-rnegex 11109  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-rex 3063

This theorem is referenced by:  gt0ne0  11614  add20  11661  subge0  11662  lesub0  11666  mulge0  11667  msqgt0  11669  msqge0  11670  gt0ne0d  11713  addgt0d  11724  sublt0d  11775  prodgt0  12000  mulgt1  12015  lt2msq1  12038  fiminre2  12102  supmul1  12123  supmul  12126  nnne0  12191  0mnnnnn0  12445  nn0negleid  12465  neglt  12937  rpgecl  12947  ge0p1rp  12950  ledivge1le  12990  mul2lt0rlt0  13021  mul2lt0rgt0  13022  mul2lt0bi  13025  prodge0rd  13026  max0sub  13123  reltxrnmnf  13270  infmrp1  13272  lincmb01cmp  13423  iccf1o  13424  xov1plusxeqvd  13426  elfz0fzfz0  13561  fz0fzelfz0  13562  elfzo0z  13629  fzofzim  13637  fzo1fzo0n0  13643  elfzodifsumelfzo  13659  ssfzoulel  13688  elfznelfzo  13701  muladdmodid  13845  modltm1p1mod  13858  addmodlteq  13881  expgt1  14035  ltexp2a  14101  expcan  14104  ltexp2  14105  leexp2  14106  leexp2a  14107  zzlesq  14141  expnlbnd2  14169  discr  14175  fi1uzind  14442  ccatsymb  14518  ccat2s1fvw  14574  swrdnd  14590  swrdnnn0nd  14592  swrdswrdlem  14639  swrdswrd  14640  repswswrd  14719  swrd2lsw  14887  2swrd2eqwrdeq  14888  leabs  15234  max0add  15245  absgt0  15260  rlimrege0  15514  iseraltlem2  15618  fsumrecl  15669  o1fsum  15748  cvgcmp  15751  cvgcmpce  15753  geomulcvg  15811  mertenslem2  15820  fprodle  15931  rpnnen2lem4  16154  p1modz1  16198  moddvds  16202  oddge22np1  16288  bitsfzolem  16373  bitsinv1lem  16380  sadcaddlem  16396  nn0rppwr  16500  nn0expgcd  16503  lcmgcdlem  16545  dvdsnprmd  16629  2mulprm  16632  isprm7  16647  qnumgt0  16689  modprm0  16745  qexpz  16841  prmreclem4  16859  4sqlem6  16883  prmgaplem7  16997  gzrngunit  21400  regsumfsum  21402  regsumsupp  21589  fvmptnn04ifd  22809  chfacffsupp  22812  chfacfscmul0  22814  chfacfscmulgsum  22816  chfacfpmmul0  22818  chfacfpmmulgsum  22820  prdsmet  24326  metustexhalf  24512  nlmvscnlem2  24641  nlmvscnlem1  24642  nmo0  24691  blcvx  24754  iihalf1cn  24894  evth  24926  lebnumlem1  24928  lebnumii  24933  htpycc  24947  pcohtpylem  24987  pcoass  24992  pcorevlem  24994  nmoleub2lem3  25083  ipcnlem2  25212  ipcnlem1  25213  rrxcph  25360  rrxmetlem  25375  rrxmet  25376  rrxdstprj1  25377  ehlbase  25383  minveclem3b  25396  minveclem6  25402  pjthlem1  25405  ovolicopnf  25493  ioorcl2  25541  volivth  25576  mbfposr  25621  i1fmulc  25672  itg1mulc  25673  itg1ge0a  25680  mbfi1flim  25692  itg2split  25718  itg2monolem1  25719  itg2monolem3  25721  itg2mono  25722  itg2cnlem2  25731  itgge0  25780  bddiblnc  25811  dvlip  25966  dvlipcn  25967  dveq0  25973  dv11cn  25974  dvlt0  25978  dvfsumge  25996  dgradd2  26242  plydivlem3  26271  mtest  26381  radcnvlem1  26390  radcnv0  26393  radcnvlt1  26395  radcnvle  26397  pserulm  26399  pserdvlem1  26405  pserdv  26407  abelthlem2  26410  abelthlem7  26416  pilem2  26430  pilem3  26431  coseq00topi  26479  tanabsge  26483  cosq34lt1  26504  tanord1  26514  tanord  26515  rplogcl  26581  logdivle  26599  logcnlem3  26621  logcnlem4  26622  dvloglem  26625  logtayl  26637  abscxp2  26670  cxplt  26671  cxple  26672  cxple2a  26676  cxpcn3lem  26725  abscxpbnd  26731  rtprmirr  26738  chordthmlem4  26813  chordthmlem5  26814  asinlem3  26849  atanre  26863  atanlogaddlem  26891  atanlogadd  26892  atanlogsublem  26893  atantan  26901  atans2  26909  efrlim  26947  efrlimOLD  26948  cxp2limlem  26954  cxp2lim  26955  cxploglim2  26957  divsqrtsumlem  26958  jensenlem2  26966  harmonicubnd  26988  fsumharmonic  26990  dmlogdmgm  27002  lgamgulmlem1  27007  lgamgulmlem2  27008  ftalem1  27051  ftalem2  27052  ftalem5  27055  vmacl  27096  chtwordi  27134  ppiwordi  27140  chtrpcl  27153  fsumfldivdiaglem  27167  fsumvma2  27193  chpval2  27197  chpchtsum  27198  chpub  27199  logfacbnd3  27202  logexprlim  27204  mersenne  27206  lgsdilem  27303  lgsne0  27314  gausslemma2dlem1a  27344  lgseisen  27358  lgsquadlem1  27359  lgsquadlem2  27360  2sqmod  27415  2sqnn0  27417  chebbnd1lem2  27449  chebbnd1lem3  27450  chebbnd1  27451  chtppilimlem1  27452  chtppilimlem2  27453  chtppilim  27454  chebbnd2  27456  chto1lb  27457  chpchtlim  27458  chpo1ub  27459  dchrisumlema  27467  dchrisumlem2  27469  dchrisumlem3  27470  dchrmusumlema  27472  dchrvmasumlem2  27477  dchrvmasumiflem1  27480  dchrisum0flblem1  27487  dchrisum0flblem2  27488  dchrisum0re  27492  dchrisum0lema  27493  dchrisum0  27499  dirith2  27507  mulog2sumlem1  27513  vmalogdivsum2  27517  log2sumbnd  27523  selberg2lem  27529  chpdifbndlem1  27532  chpdifbnd  27534  selberg3lem1  27536  pntrmax  27543  pntrsumo1  27544  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntpbnd1a  27564  pntpbnd1  27565  pntpbnd2  27566  pntlemg  27577  pntlemj  27582  pntlemk  27585  pntlem3  27588  pnt2  27592  pnt  27593  ostth2lem1  27597  padicabv  27609  padicabvcxp  27611  ostth2lem3  27614  ostth2lem4  27615  ostth3  27617  trgcgrg  28599  tgcgr4  28615  axsegconlem7  29008  axsegconlem10  29011  axcontlem2  29050  axcontlem4  29052  axcontlem7  29055  axcontlem10  29058  crctcshwlkn0lem3  29897  crctcshwlkn0  29906  clwlkclwwlklem2a2  30080  clwlkclwwlklem2a  30085  wwlksubclwwlk  30145  frgrogt3nreg  30484  friendshipgt3  30485  minvecolem5  30968  minvecolem6  30969  htthlem  31004  pjhthlem1  31478  sgnval2  32824  nndiffz1  32876  bcm1n  32885  fzo0opth  32893  expgt0b  32907  sgnneg  32924  sgnmul  32926  sgnsub  32928  nexple  32935  oexpled  32938  indf1o  32956  wrdt2ind  33045  cycpmrn  33236  cyc3conja  33250  ccfldextdgrr  33849  constrsslem  33918  constrresqrtcl  33954  constrsqrtcl  33956  cos9thpiminplylem1  33959  pnfneige0  34128  measinb  34398  eulerpartlems  34537  eulerpartlemgc  34539  ballotlemfc0  34670  ballotlemfcc  34671  ballotlemodife  34675  signsply0  34728  signslema  34739  signsvtp  34760  itgexpif  34783  breprexplemc  34809  circlemeth  34817  logdivsqrle  34827  0nn0m1nnn0  35326  cvmliftlem2  35499  dnibndlem9  36705  unbdqndv2lem2  36729  knoppndvlem1  36731  knoppndvlem2  36732  knoppndvlem7  36737  knoppndvlem11  36741  knoppndvlem14  36744  knoppndvlem15  36745  knoppndvlem17  36747  knoppndvlem19  36749  knoppndvlem20  36750  bj-pinftynminfty  37476  poimirlem10  37875  poimirlem11  37876  poimirlem24  37889  poimirlem29  37894  poimirlem31  37896  poimirlem32  37897  poimir  37898  mblfinlem2  37903  ftc1anclem7  37944  ftc1anclem8  37945  ftc1anc  37946  areacirclem1  37953  areacirclem4  37956  areacirc  37958  geomcau  38004  isbnd3b  38030  prdsbnd  38038  bfp  38069  rrnequiv  38080  resdvopclptsd  42392  lcmineqlem2  42394  lcmineqlem3  42395  lcmineqlem10  42402  lcmineqlem12  42404  lcmineqlem23  42415  3lexlogpow5ineq1  42418  3lexlogpow5ineq2  42419  3lexlogpow5ineq4  42420  3lexlogpow5ineq3  42421  3lexlogpow2ineq2  42423  3lexlogpow5ineq5  42424  aks4d1lem1  42426  dvrelog2  42428  dvrelog3  42429  dvrelog2b  42430  0nonelalab  42431  dvrelogpow2b  42432  aks4d1p1p3  42433  aks4d1p1p2  42434  aks4d1p1p4  42435  aks4d1p1p6  42437  aks4d1p1p7  42438  aks4d1p1p5  42439  aks4d1p1  42440  aks4d1p2  42441  aks4d1p3  42442  aks4d1p5  42444  aks4d1p6  42445  aks4d1p7d1  42446  aks4d1p7  42447  aks4d1p8d2  42449  aks4d1p8d3  42450  aks4d1p8  42451  aks4d1p9  42452  posbezout  42464  primrootspoweq0  42470  aks6d1c1  42480  hashscontpow1  42485  aks6d1c2lem4  42491  aks6d1c5lem2  42502  deg1gprod  42504  2np3bcnp1  42508  2ap1caineq  42509  sticksstones7  42516  sticksstones10  42519  sticksstones12a  42521  sticksstones12  42522  sticksstones22  42532  aks6d1c6lem3  42536  bcled  42542  bcle2d  42543  aks6d1c7lem1  42544  aks6d1c7lem2  42545  aks6d1c7  42548  aks5lem6  42556  unitscyglem5  42563  aks5lem8  42565  sn-1ne2  42629  oexpreposd  42686  posqsqznn  42700  redvmptabs  42724  readvrec  42726  re1m1e0m0  42761  re0m0e0  42766  remul01  42771  sn-remul0ord  42772  remulneg2d  42779  sn-addlt0d  42822  sn-addgt0d  42823  renegmulnnass  42829  zmulcomlem  42831  mulgt0con1dlem  42833  sn-mulgt1d  42843  mulltgt0d  42846  mullt0b2d  42848  sn-mullt0d  42849  sn-msqgt0d  42850  fimgmcyc  42898  dffltz  42986  3cubeslem1  43035  irrapxlem1  43173  irrapxlem2  43174  irrapxlem3  43175  irrapxlem4  43176  pellexlem6  43185  pell14qrgt0  43210  pell1qrgaplem  43224  pellfundex  43237  pellfundrp  43239  monotoddzzfi  43293  jm2.24  43314  jm2.23  43347  jm2.26lem3  43352  jm3.1lem3  43370  sqrtcvallem1  43981  reabsifneg  43982  reabsifpos  43984  sqrtcval  43991  k0004ss2  44502  imo72b2lem1  44519  dvgrat  44662  hashnzfz2  44671  binomcxplemnn0  44699  binomcxplemnotnn0  44706  divlt0gt0d  45642  upbdrech2  45664  xralrple2  45707  xralrple3  45726  reclt0d  45739  reclt0  45743  xrpnf  45837  fsumnncl  45926  fsumsupp0  45932  sumnnodd  45984  lptre2pt  45992  limsupubuz  46065  liminfresre  46131  liminf0  46145  dvmptconst  46267  dvdivbd  46275  dvcosax  46278  dvbdfbdioolem1  46280  dvbdfbdioolem2  46281  ioodvbdlimc1lem1  46283  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  dvxpaek  46292  dvnxpaek  46294  volioc  46324  volico  46335  stoweidlem1  46353  stoweidlem7  46359  stoweidlem11  46363  stoweidlem25  46377  stoweidlem26  46378  stoweidlem34  46386  stoweidlem36  46388  stoweidlem41  46393  stoweidlem42  46394  stoweidlem44  46396  stoweidlem45  46397  wallispilem3  46419  wallispilem4  46420  wallispi  46422  stirlinglem3  46428  stirlinglem5  46430  stirlinglem6  46431  stirlinglem7  46432  stirlinglem10  46435  stirlinglem11  46436  stirlinglem12  46437  dirkeritg  46454  dirkercncflem2  46456  fourierdlem9  46468  fourierdlem11  46470  fourierdlem12  46471  fourierdlem14  46473  fourierdlem15  46474  fourierdlem19  46478  fourierdlem24  46483  fourierdlem28  46487  fourierdlem30  46489  fourierdlem40  46499  fourierdlem41  46500  fourierdlem43  46502  fourierdlem44  46503  fourierdlem47  46505  fourierdlem50  46508  fourierdlem51  46509  fourierdlem57  46515  fourierdlem60  46518  fourierdlem61  46519  fourierdlem66  46524  fourierdlem68  46526  fourierdlem73  46531  fourierdlem74  46532  fourierdlem75  46533  fourierdlem78  46536  fourierdlem79  46537  fourierdlem83  46541  fourierdlem88  46546  fourierdlem92  46550  fourierdlem93  46551  fourierdlem97  46555  fourierdlem103  46561  fourierdlem104  46562  fourierdlem109  46567  fourierdlem111  46569  sqwvfoura  46580  sqwvfourb  46581  fourierswlem  46582  fouriersw  46583  elaa2lem  46585  etransclem4  46590  etransclem18  46604  etransclem19  46605  etransclem23  46609  etransclem27  46613  etransclem31  46617  etransclem32  46618  etransclem35  46621  etransclem41  46627  etransclem46  46632  etransclem48  46634  rrxtopnfi  46639  qndenserrnbllem  46646  salgencntex  46695  sge0tsms  46732  sge0isum  46779  volicorecl  46898  hoiprodcl  46899  ovnlerp  46914  ovnsubaddlem1  46922  hoiprodcl3  46932  volicore  46933  hoidmvcl  46934  hoidmvlelem1  46947  hoidmvlelem2  46948  hoidmvlelem3  46949  ovnhoi  46955  hoiqssbllem2  46975  volicorege0  46989  vonhoire  47024  pimrecltpos  47060  pimrecltneg  47076  smfmbfcex  47112  nsssmfmbflem  47130  smfrec  47141  smfmullem3  47145  smfdivdmmbl  47190  sharhght  47217  et-sqrtnegnre  47225  ormkglobd  47227  natglobalincr  47229  chnsubseqwl  47231  zm1nn  47656  eluzge0nn0  47666  elfz2z  47669  2ffzoeq  47681  m1modmmod  47712  modm1p1ne  47724  iccpartigtl  47777  iccpartgt  47781  requad01  47975  requad1  47976  requad2  47977  stgrusgra  48313  gpgedgvtx1  48416  expnegico01  48872  regt1loggt0  48890  refdivmptf  48896  elbigolo1  48911  rege1logbrege0  48912  fllog2  48922  dignn0flhalflem1  48969  eenglngeehlnmlem2  49092  line2  49106  line2xlem  49107  line2x  49108  line2y  49109  itsclc0yqsol  49118  2itscp  49135  inlinecirc02plem  49140  amgmwlem  50155