Theorem 0red 11293

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11183  0cc0 11184

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-addrcl 11245  ax-rnegex 11255  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819  df-rex 3077

This theorem is referenced by:  gt0ne0  11755  add20  11802  subge0  11803  lesub0  11807  mulge0  11808  msqgt0  11810  msqge0  11811  addgt0d  11865  sublt0d  11916  prodgt0  12141  mulgt1  12156  lt2msq1  12179  fiminre2  12243  supmul1  12264  supmul  12267  nnne0  12327  0mnnnnn0  12585  nn0negleid  12605  rpgecl  13085  ge0p1rp  13088  ledivge1le  13128  mul2lt0rlt0  13159  mul2lt0rgt0  13160  mul2lt0bi  13163  prodge0rd  13164  max0sub  13258  reltxrnmnf  13404  infmrp1  13406  lincmb01cmp  13555  iccf1o  13556  xov1plusxeqvd  13558  elfz0fzfz0  13690  fz0fzelfz0  13691  elfzo0z  13758  fzofzim  13763  fzo1fzo0n0  13767  elfzodifsumelfzo  13782  ssfzoulel  13810  elfznelfzo  13822  muladdmodid  13962  modltm1p1mod  13974  addmodlteq  13997  expgt1  14151  ltexp2a  14216  expcan  14219  ltexp2  14220  leexp2  14221  leexp2a  14222  zzlesq  14255  expnlbnd2  14283  discr  14289  fi1uzind  14556  ccatsymb  14630  ccat2s1fvw  14686  swrdnd  14702  swrdnnn0nd  14704  swrdswrdlem  14752  swrdswrd  14753  repswswrd  14832  swrd2lsw  15001  2swrd2eqwrdeq  15002  leabs  15348  max0add  15359  absgt0  15373  rlimrege0  15625  iseraltlem2  15731  fsumrecl  15782  o1fsum  15861  cvgcmp  15864  cvgcmpce  15866  geomulcvg  15924  mertenslem2  15933  fprodle  16044  rpnnen2lem4  16265  p1modz1  16309  moddvds  16313  oddge22np1  16397  bitsfzolem  16480  bitsinv1lem  16487  sadcaddlem  16503  nn0rppwr  16608  nn0expgcd  16611  lcmgcdlem  16653  dvdsnprmd  16737  2mulprm  16740  isprm7  16755  qnumgt0  16797  modprm0  16852  qexpz  16948  prmreclem4  16966  4sqlem6  16990  prmgaplem7  17104  gzrngunit  21474  regsumfsum  21476  regsumsupp  21663  fvmptnn04ifd  22880  chfacffsupp  22883  chfacfscmul0  22885  chfacfscmulgsum  22887  chfacfpmmul0  22889  chfacfpmmulgsum  22891  prdsmet  24401  metustexhalf  24590  nlmvscnlem2  24727  nlmvscnlem1  24728  nmo0  24777  blcvx  24839  iihalf1cn  24978  evth  25010  lebnumlem1  25012  lebnumii  25017  htpycc  25031  pcohtpylem  25071  pcoass  25076  pcorevlem  25078  nmoleub2lem3  25167  ipcnlem2  25297  ipcnlem1  25298  rrxcph  25445  rrxmetlem  25460  rrxmet  25461  rrxdstprj1  25462  ehlbase  25468  minveclem3b  25481  minveclem6  25487  pjthlem1  25490  ovolicopnf  25578  ioorcl2  25626  volivth  25661  mbfposr  25706  i1fmulc  25758  itg1mulc  25759  itg1ge0a  25766  mbfi1flim  25778  itg2split  25804  itg2monolem1  25805  itg2monolem3  25807  itg2mono  25808  itg2cnlem2  25817  itgge0  25866  bddiblnc  25897  dvlip  26052  dvlipcn  26053  dveq0  26059  dv11cn  26060  dvlt0  26064  dvfsumge  26082  dgradd2  26328  plydivlem3  26355  mtest  26465  radcnvlem1  26474  radcnv0  26477  radcnvlt1  26479  radcnvle  26481  pserulm  26483  pserdvlem1  26489  pserdv  26491  abelthlem2  26494  abelthlem7  26500  pilem2  26514  pilem3  26515  coseq00topi  26562  tanabsge  26566  cosq34lt1  26587  tanord1  26597  tanord  26598  rplogcl  26664  logdivle  26682  logcnlem3  26704  logcnlem4  26705  dvloglem  26708  logtayl  26720  abscxp2  26753  cxplt  26754  cxple  26755  cxple2a  26759  cxpcn3lem  26808  abscxpbnd  26814  rtprmirr  26821  chordthmlem4  26896  chordthmlem5  26897  asinlem3  26932  atanre  26946  atanlogaddlem  26974  atanlogadd  26975  atanlogsublem  26976  atantan  26984  atans2  26992  efrlim  27030  efrlimOLD  27031  cxp2limlem  27037  cxp2lim  27038  cxploglim2  27040  divsqrtsumlem  27041  jensenlem2  27049  harmonicubnd  27071  fsumharmonic  27073  dmlogdmgm  27085  lgamgulmlem1  27090  lgamgulmlem2  27091  ftalem1  27134  ftalem2  27135  ftalem5  27138  vmacl  27179  chtwordi  27217  ppiwordi  27223  chtrpcl  27236  fsumfldivdiaglem  27250  fsumvma2  27276  chpval2  27280  chpchtsum  27281  chpub  27282  logfacbnd3  27285  logexprlim  27287  mersenne  27289  lgsdilem  27386  lgsne0  27397  gausslemma2dlem1a  27427  lgseisen  27441  lgsquadlem1  27442  lgsquadlem2  27443  2sqmod  27498  2sqnn0  27500  chebbnd1lem2  27532  chebbnd1lem3  27533  chebbnd1  27534  chtppilimlem1  27535  chtppilimlem2  27536  chtppilim  27537  chebbnd2  27539  chto1lb  27540  chpchtlim  27541  chpo1ub  27542  dchrisumlema  27550  dchrisumlem2  27552  dchrisumlem3  27553  dchrmusumlema  27555  dchrvmasumlem2  27560  dchrvmasumiflem1  27563  dchrisum0flblem1  27570  dchrisum0flblem2  27571  dchrisum0re  27575  dchrisum0lema  27576  dchrisum0  27582  dirith2  27590  mulog2sumlem1  27596  vmalogdivsum2  27600  log2sumbnd  27606  selberg2lem  27612  chpdifbndlem1  27615  chpdifbnd  27617  selberg3lem1  27619  pntrmax  27626  pntrsumo1  27627  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  pntpbnd1a  27647  pntpbnd1  27648  pntpbnd2  27649  pntlemg  27660  pntlemj  27665  pntlemk  27668  pntlem3  27671  pnt2  27675  pnt  27676  ostth2lem1  27680  padicabv  27692  padicabvcxp  27694  ostth2lem3  27697  ostth2lem4  27698  ostth3  27700  trgcgrg  28541  tgcgr4  28557  axsegconlem7  28956  axsegconlem10  28959  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  axcontlem10  29006  crctcshwlkn0lem3  29845  crctcshwlkn0  29854  clwlkclwwlklem2a2  30025  clwlkclwwlklem2a  30030  wwlksubclwwlk  30090  frgrogt3nreg  30429  friendshipgt3  30430  minvecolem5  30913  minvecolem6  30914  htthlem  30949  pjhthlem1  31423  nndiffz1  32791  bcm1n  32800  fzo0opth  32810  expgt0b  32820  wrdt2ind  32920  cycpmrn  33136  cyc3conja  33150  ccfldextdgrr  33682  constrsslem  33731  pnfneige0  33897  nexple  33973  indf1o  33988  measinb  34185  eulerpartlems  34325  eulerpartlemgc  34327  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemodife  34462  sgnneg  34505  sgnmul  34507  sgnsub  34509  signsply0  34528  signslema  34539  signsvtp  34560  itgexpif  34583  breprexplemc  34609  circlemeth  34617  logdivsqrle  34627  0nn0m1nnn0  35080  cvmliftlem2  35254  dnibndlem9  36452  unbdqndv2lem2  36476  knoppndvlem1  36478  knoppndvlem2  36479  knoppndvlem7  36484  knoppndvlem11  36488  knoppndvlem14  36491  knoppndvlem15  36492  knoppndvlem17  36494  knoppndvlem19  36496  knoppndvlem20  36497  bj-pinftynminfty  37193  poimirlem10  37590  poimirlem11  37591  poimirlem24  37604  poimirlem29  37609  poimirlem31  37611  poimirlem32  37612  poimir  37613  mblfinlem2  37618  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  areacirclem1  37668  areacirclem4  37671  areacirc  37673  geomcau  37719  isbnd3b  37745  prdsbnd  37753  bfp  37784  rrnequiv  37795  resdvopclptsd  41985  lcmineqlem2  41987  lcmineqlem3  41988  lcmineqlem10  41995  lcmineqlem12  41997  lcmineqlem23  42008  3lexlogpow5ineq1  42011  3lexlogpow5ineq2  42012  3lexlogpow5ineq4  42013  3lexlogpow5ineq3  42014  3lexlogpow2ineq2  42016  3lexlogpow5ineq5  42017  aks4d1lem1  42019  dvrelog2  42021  dvrelog3  42022  dvrelog2b  42023  0nonelalab  42024  dvrelogpow2b  42025  aks4d1p1p3  42026  aks4d1p1p2  42027  aks4d1p1p4  42028  aks4d1p1p6  42030  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p1  42033  aks4d1p2  42034  aks4d1p3  42035  aks4d1p5  42037  aks4d1p6  42038  aks4d1p7d1  42039  aks4d1p7  42040  aks4d1p8d2  42042  aks4d1p8d3  42043  aks4d1p8  42044  aks4d1p9  42045  posbezout  42057  primrootspoweq0  42063  aks6d1c1  42073  hashscontpow1  42078  aks6d1c2lem4  42084  aks6d1c5lem2  42095  deg1gprod  42097  2np3bcnp1  42101  2ap1caineq  42102  sticksstones7  42109  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  sticksstones22  42125  aks6d1c6lem3  42129  bcled  42135  bcle2d  42136  aks6d1c7lem1  42137  aks6d1c7lem2  42138  aks6d1c7  42141  aks5lem6  42149  unitscyglem5  42156  aks5lem8  42158  metakunt2  42163  metakunt29  42190  sn-1ne2  42254  oexpreposd  42309  posqsqznn  42323  re1m1e0m0  42373  re0m0e0  42378  remul01  42383  remulneg2d  42390  sn-addlt0d  42422  sn-addgt0d  42423  renegmulnnass  42429  zmulcomlem  42431  mulgt0con1dlem  42433  sn-mulgt1d  42441  fimgmcyc  42489  dffltz  42589  3cubeslem1  42640  irrapxlem1  42778  irrapxlem2  42779  irrapxlem3  42780  irrapxlem4  42781  pellexlem6  42790  pell14qrgt0  42815  pell1qrgaplem  42829  pellfundex  42842  pellfundrp  42844  monotoddzzfi  42899  jm2.24  42920  jm2.23  42953  jm2.26lem3  42958  jm3.1lem3  42976  sqrtcvallem1  43593  reabsifneg  43594  reabsifpos  43596  sqrtcval  43603  k0004ss2  44114  imo72b2lem1  44131  dvgrat  44281  hashnzfz2  44290  binomcxplemnn0  44318  binomcxplemnotnn0  44325  neglt  45199  divlt0gt0d  45201  upbdrech2  45223  xralrple2  45269  xralrple3  45289  reclt0d  45302  reclt0  45306  xrpnf  45401  fsumnncl  45493  fsumsupp0  45499  sumnnodd  45551  lptre2pt  45561  limsupubuz  45634  liminfresre  45700  liminf0  45714  dvmptconst  45836  dvdivbd  45844  dvcosax  45847  dvbdfbdioolem1  45849  dvbdfbdioolem2  45850  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvxpaek  45861  dvnxpaek  45863  volioc  45893  volico  45904  stoweidlem1  45922  stoweidlem7  45928  stoweidlem11  45932  stoweidlem25  45946  stoweidlem26  45947  stoweidlem34  45955  stoweidlem36  45957  stoweidlem41  45962  stoweidlem42  45963  stoweidlem44  45965  stoweidlem45  45966  wallispilem3  45988  wallispilem4  45989  wallispi  45991  stirlinglem3  45997  stirlinglem5  45999  stirlinglem6  46000  stirlinglem7  46001  stirlinglem10  46004  stirlinglem11  46005  stirlinglem12  46006  dirkeritg  46023  dirkercncflem2  46025  fourierdlem9  46037  fourierdlem11  46039  fourierdlem12  46040  fourierdlem14  46042  fourierdlem15  46043  fourierdlem19  46047  fourierdlem24  46052  fourierdlem28  46056  fourierdlem30  46058  fourierdlem40  46068  fourierdlem41  46069  fourierdlem43  46071  fourierdlem44  46072  fourierdlem47  46074  fourierdlem50  46077  fourierdlem51  46078  fourierdlem57  46084  fourierdlem60  46087  fourierdlem61  46088  fourierdlem66  46093  fourierdlem68  46095  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem78  46105  fourierdlem79  46106  fourierdlem83  46110  fourierdlem88  46115  fourierdlem92  46119  fourierdlem93  46120  fourierdlem97  46124  fourierdlem103  46130  fourierdlem104  46131  fourierdlem109  46136  fourierdlem111  46138  sqwvfoura  46149  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  elaa2lem  46154  etransclem4  46159  etransclem18  46173  etransclem19  46174  etransclem23  46178  etransclem27  46182  etransclem31  46186  etransclem32  46187  etransclem35  46190  etransclem41  46196  etransclem46  46201  etransclem48  46203  rrxtopnfi  46208  qndenserrnbllem  46215  salgencntex  46264  sge0tsms  46301  sge0isum  46348  volicorecl  46467  hoiprodcl  46468  ovnlerp  46483  ovnsubaddlem1  46491  hoiprodcl3  46501  volicore  46502  hoidmvcl  46503  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  ovnhoi  46524  hoiqssbllem2  46544  volicorege0  46558  vonhoire  46593  pimrecltpos  46629  pimrecltneg  46645  smfmbfcex  46681  nsssmfmbflem  46699  smfrec  46710  smfmullem3  46714  smfdivdmmbl  46759  sharhght  46786  et-sqrtnegnre  46794  natglobalincr  46796  upwordnul  46799  zm1nn  47217  eluzge0nn0  47227  elfz2z  47230  2ffzoeq  47242  iccpartigtl  47297  iccpartgt  47301  requad01  47495  requad1  47496  requad2  47497  expnegico01  48247  m1modmmod  48255  difmodm1lt  48256  regt1loggt0  48270  refdivmptf  48276  elbigolo1  48291  rege1logbrege0  48292  fllog2  48302  dignn0flhalflem1  48349  eenglngeehlnmlem2  48472  line2  48486  line2xlem  48487  line2x  48488  line2y  48489  itsclc0yqsol  48498  2itscp  48515  inlinecirc02plem  48520  amgmwlem  48896