Theorem 0red 11167

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℝcr 11059  0cc0 11060

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-1cn 11118  ax-addrcl 11121  ax-rnegex 11131  ax-cnre 11133

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-clel 2809  df-rex 3070

This theorem is referenced by:  gt0ne0  11629  add20  11676  subge0  11677  lesub0  11681  mulge0  11682  msqgt0  11684  msqge0  11685  addgt0d  11739  sublt0d  11790  prodgt0  12011  lt2msq1  12048  fiminre2  12112  supmul1  12133  supmul  12136  nnne0  12196  0mnnnnn0  12454  nn0negleid  12474  rpgecl  12952  ge0p1rp  12955  ledivge1le  12995  mul2lt0rlt0  13026  mul2lt0rgt0  13027  mul2lt0bi  13030  prodge0rd  13031  max0sub  13125  reltxrnmnf  13271  infmrp1  13273  lincmb01cmp  13422  iccf1o  13423  xov1plusxeqvd  13425  elfz0fzfz0  13556  fz0fzelfz0  13557  elfzo0z  13624  fzofzim  13629  fzo1fzo0n0  13633  elfzodifsumelfzo  13648  ssfzoulel  13676  elfznelfzo  13687  muladdmodid  13826  modltm1p1mod  13838  addmodlteq  13861  expgt1  14016  ltexp2a  14081  expcan  14084  ltexp2  14085  leexp2  14086  leexp2a  14087  zzlesq  14120  expnlbnd2  14147  discr  14153  fi1uzind  14408  ccatsymb  14482  ccat2s1fvw  14538  swrdnd  14554  swrdnnn0nd  14556  swrdswrdlem  14604  swrdswrd  14605  repswswrd  14684  swrd2lsw  14853  2swrd2eqwrdeq  14854  leabs  15196  max0add  15207  absgt0  15221  rlimrege0  15473  iseraltlem2  15579  fsumrecl  15630  o1fsum  15709  cvgcmp  15712  cvgcmpce  15714  geomulcvg  15772  mertenslem2  15781  fprodle  15890  rpnnen2lem4  16110  p1modz1  16154  moddvds  16158  oddge22np1  16242  bitsfzolem  16325  bitsinv1lem  16332  sadcaddlem  16348  lcmgcdlem  16493  dvdsnprmd  16577  2mulprm  16580  isprm7  16595  qnumgt0  16636  modprm0  16688  qexpz  16784  prmreclem4  16802  4sqlem6  16826  prmgaplem7  16940  gzrngunit  20900  regsumfsum  20902  regsumsupp  21063  fvmptnn04ifd  22239  chfacffsupp  22242  chfacfscmul0  22244  chfacfscmulgsum  22246  chfacfpmmul0  22248  chfacfpmmulgsum  22250  prdsmet  23760  metustexhalf  23949  nlmvscnlem2  24086  nlmvscnlem1  24087  nmo0  24136  blcvx  24198  evth  24359  lebnumlem1  24361  lebnumii  24366  htpycc  24380  pcohtpylem  24419  pcoass  24424  pcorevlem  24426  nmoleub2lem3  24515  ipcnlem2  24645  ipcnlem1  24646  rrxcph  24793  rrxmetlem  24808  rrxmet  24809  rrxdstprj1  24810  ehlbase  24816  minveclem3b  24829  minveclem6  24835  pjthlem1  24838  ovolicopnf  24925  ioorcl2  24973  volivth  25008  mbfposr  25053  i1fmulc  25105  itg1mulc  25106  itg1ge0a  25113  mbfi1flim  25125  itg2split  25151  itg2monolem1  25152  itg2monolem3  25154  itg2mono  25155  itg2cnlem2  25164  itgge0  25212  bddiblnc  25243  dvlip  25394  dvlipcn  25395  dveq0  25401  dv11cn  25402  dvlt0  25406  dvfsumge  25423  dgradd2  25666  plydivlem3  25692  mtest  25800  radcnvlem1  25809  radcnv0  25812  radcnvlt1  25814  radcnvle  25816  pserulm  25818  pserdvlem1  25823  pserdv  25825  abelthlem2  25828  abelthlem7  25834  pilem2  25848  pilem3  25849  coseq00topi  25896  tanabsge  25900  cosq34lt1  25920  tanord1  25930  tanord  25931  rplogcl  25996  logdivle  26014  logcnlem3  26036  logcnlem4  26037  dvloglem  26040  logtayl  26052  abscxp2  26085  cxplt  26086  cxple  26087  cxple2a  26091  cxpcn3lem  26137  abscxpbnd  26143  chordthmlem4  26222  chordthmlem5  26223  asinlem3  26258  atanre  26272  atanlogaddlem  26300  atanlogadd  26301  atanlogsublem  26302  atantan  26310  atans2  26318  efrlim  26356  cxp2limlem  26362  cxp2lim  26363  cxploglim2  26365  divsqrtsumlem  26366  jensenlem2  26374  harmonicubnd  26396  fsumharmonic  26398  dmlogdmgm  26410  lgamgulmlem1  26415  lgamgulmlem2  26416  ftalem1  26459  ftalem2  26460  ftalem5  26463  vmacl  26504  chtwordi  26542  ppiwordi  26548  chtrpcl  26561  fsumfldivdiaglem  26575  fsumvma2  26599  chpval2  26603  chpchtsum  26604  chpub  26605  logfacbnd3  26608  logexprlim  26610  mersenne  26612  lgsdilem  26709  lgsne0  26720  gausslemma2dlem1a  26750  lgseisen  26764  lgsquadlem1  26765  lgsquadlem2  26766  2sqmod  26821  2sqnn0  26823  chebbnd1lem2  26855  chebbnd1lem3  26856  chebbnd1  26857  chtppilimlem1  26858  chtppilimlem2  26859  chtppilim  26860  chebbnd2  26862  chto1lb  26863  chpchtlim  26864  chpo1ub  26865  dchrisumlema  26873  dchrisumlem2  26875  dchrisumlem3  26876  dchrmusumlema  26878  dchrvmasumlem2  26883  dchrvmasumiflem1  26886  dchrisum0flblem1  26893  dchrisum0flblem2  26894  dchrisum0re  26898  dchrisum0lema  26899  dchrisum0  26905  dirith2  26913  mulog2sumlem1  26919  vmalogdivsum2  26923  log2sumbnd  26929  selberg2lem  26935  chpdifbndlem1  26938  chpdifbnd  26940  selberg3lem1  26942  pntrmax  26949  pntrsumo1  26950  pntrlog2bndlem4  26965  pntrlog2bndlem5  26966  pntpbnd1a  26970  pntpbnd1  26971  pntpbnd2  26972  pntlemg  26983  pntlemj  26988  pntlemk  26991  pntlem3  26994  pnt2  26998  pnt  26999  ostth2lem1  27003  padicabv  27015  padicabvcxp  27017  ostth2lem3  27020  ostth2lem4  27021  ostth3  27023  trgcgrg  27520  tgcgr4  27536  axsegconlem7  27935  axsegconlem10  27938  axcontlem2  27977  axcontlem4  27979  axcontlem7  27982  axcontlem10  27985  crctcshwlkn0lem3  28820  crctcshwlkn0  28829  clwlkclwwlklem2a2  29000  clwlkclwwlklem2a  29005  wwlksubclwwlk  29065  frgrogt3nreg  29404  friendshipgt3  29405  minvecolem5  29886  minvecolem6  29887  htthlem  29922  pjhthlem1  30396  nndiffz1  31757  bcm1n  31766  wrdt2ind  31877  cycpmrn  32062  cyc3conja  32076  ccfldextdgrr  32443  pnfneige0  32621  nexple  32697  indf1o  32712  measinb  32909  eulerpartlems  33049  eulerpartlemgc  33051  ballotlemfc0  33181  ballotlemfcc  33182  ballotlemodife  33186  sgnneg  33229  sgnmul  33231  sgnsub  33233  signsply0  33252  signslema  33263  signsvtp  33284  itgexpif  33308  breprexplemc  33334  circlemeth  33342  logdivsqrle  33352  0nn0m1nnn0  33792  cvmliftlem2  33967  dnibndlem9  35025  unbdqndv2lem2  35049  knoppndvlem1  35051  knoppndvlem2  35052  knoppndvlem7  35057  knoppndvlem11  35061  knoppndvlem14  35064  knoppndvlem15  35065  knoppndvlem17  35067  knoppndvlem19  35069  knoppndvlem20  35070  bj-pinftynminfty  35771  poimirlem10  36161  poimirlem11  36162  poimirlem24  36175  poimirlem29  36180  poimirlem31  36182  poimirlem32  36183  poimir  36184  mblfinlem2  36189  ftc1anclem7  36230  ftc1anclem8  36231  ftc1anc  36232  areacirclem1  36239  areacirclem4  36242  areacirc  36244  geomcau  36291  isbnd3b  36317  prdsbnd  36325  bfp  36356  rrnequiv  36367  resdvopclptsd  40558  lcmineqlem2  40560  lcmineqlem3  40561  lcmineqlem10  40568  lcmineqlem12  40570  lcmineqlem23  40581  3lexlogpow5ineq1  40584  3lexlogpow5ineq2  40585  3lexlogpow5ineq4  40586  3lexlogpow5ineq3  40587  3lexlogpow2ineq2  40589  3lexlogpow5ineq5  40590  aks4d1lem1  40592  dvrelog2  40594  dvrelog3  40595  dvrelog2b  40596  0nonelalab  40597  dvrelogpow2b  40598  aks4d1p1p3  40599  aks4d1p1p2  40600  aks4d1p1p4  40601  aks4d1p1p6  40603  aks4d1p1p7  40604  aks4d1p1p5  40605  aks4d1p1  40606  aks4d1p2  40607  aks4d1p3  40608  aks4d1p5  40610  aks4d1p6  40611  aks4d1p7d1  40612  aks4d1p7  40613  aks4d1p8d2  40615  aks4d1p8d3  40616  aks4d1p8  40617  aks4d1p9  40618  2np3bcnp1  40625  2ap1caineq  40626  sticksstones7  40633  sticksstones10  40636  sticksstones12a  40638  sticksstones12  40639  sticksstones22  40649  metakunt2  40651  metakunt29  40678  sn-1ne2  40839  oexpreposd  40865  nn0rppwr  40877  nn0expgcd  40879  posqsqznn  40887  rtprmirr  40891  re1m1e0m0  40924  re0m0e0  40929  remul01  40934  remulneg2d  40941  sn-addlt0d  40973  sn-addgt0d  40974  renegmulnnass  40980  zmulcomlem  40982  mulgt0con1dlem  40984  dffltz  41030  3cubeslem1  41065  irrapxlem1  41203  irrapxlem2  41204  irrapxlem3  41205  irrapxlem4  41206  pellexlem6  41215  pell14qrgt0  41240  pell1qrgaplem  41254  pellfundex  41267  pellfundrp  41269  monotoddzzfi  41324  jm2.24  41345  jm2.23  41378  jm2.26lem3  41383  jm3.1lem3  41401  sqrtcvallem1  42025  reabsifneg  42026  reabsifpos  42028  sqrtcval  42035  k0004ss2  42546  imo72b2lem1  42564  dvgrat  42714  hashnzfz2  42723  binomcxplemnn0  42751  binomcxplemnotnn0  42758  neglt  43639  divlt0gt0d  43641  upbdrech2  43663  xralrple2  43709  xralrple3  43729  reclt0d  43742  reclt0  43746  xrpnf  43841  fsumnncl  43933  fsumsupp0  43939  sumnnodd  43991  lptre2pt  44001  limsupubuz  44074  liminfresre  44140  liminf0  44154  dvmptconst  44276  dvdivbd  44284  dvcosax  44287  dvbdfbdioolem1  44289  dvbdfbdioolem2  44290  ioodvbdlimc1lem1  44292  ioodvbdlimc1lem2  44293  ioodvbdlimc2lem  44295  dvxpaek  44301  dvnxpaek  44303  volioc  44333  volico  44344  stoweidlem1  44362  stoweidlem7  44368  stoweidlem11  44372  stoweidlem25  44386  stoweidlem26  44387  stoweidlem34  44395  stoweidlem36  44397  stoweidlem41  44402  stoweidlem42  44403  stoweidlem44  44405  stoweidlem45  44406  wallispilem3  44428  wallispilem4  44429  wallispi  44431  stirlinglem3  44437  stirlinglem5  44439  stirlinglem6  44440  stirlinglem7  44441  stirlinglem10  44444  stirlinglem11  44445  stirlinglem12  44446  dirkeritg  44463  dirkercncflem2  44465  fourierdlem9  44477  fourierdlem11  44479  fourierdlem12  44480  fourierdlem14  44482  fourierdlem15  44483  fourierdlem19  44487  fourierdlem24  44492  fourierdlem28  44496  fourierdlem30  44498  fourierdlem40  44508  fourierdlem41  44509  fourierdlem43  44511  fourierdlem44  44512  fourierdlem47  44514  fourierdlem50  44517  fourierdlem51  44518  fourierdlem57  44524  fourierdlem60  44527  fourierdlem61  44528  fourierdlem66  44533  fourierdlem68  44535  fourierdlem73  44540  fourierdlem74  44541  fourierdlem75  44542  fourierdlem78  44545  fourierdlem79  44546  fourierdlem83  44550  fourierdlem88  44555  fourierdlem92  44559  fourierdlem93  44560  fourierdlem97  44564  fourierdlem103  44570  fourierdlem104  44571  fourierdlem109  44576  fourierdlem111  44578  sqwvfoura  44589  sqwvfourb  44590  fourierswlem  44591  fouriersw  44592  elaa2lem  44594  etransclem4  44599  etransclem18  44613  etransclem19  44614  etransclem23  44618  etransclem27  44622  etransclem31  44626  etransclem32  44627  etransclem35  44630  etransclem41  44636  etransclem46  44641  etransclem48  44643  rrxtopnfi  44648  qndenserrnbllem  44655  salgencntex  44704  sge0tsms  44741  sge0isum  44788  volicorecl  44907  hoiprodcl  44908  ovnlerp  44923  ovnsubaddlem1  44931  hoiprodcl3  44941  volicore  44942  hoidmvcl  44943  hoidmvlelem1  44956  hoidmvlelem2  44957  hoidmvlelem3  44958  ovnhoi  44964  hoiqssbllem2  44984  volicorege0  44998  vonhoire  45033  pimrecltpos  45069  pimrecltneg  45085  smfmbfcex  45121  nsssmfmbflem  45139  smfrec  45150  smfmullem3  45154  smfdivdmmbl  45199  sharhght  45226  et-sqrtnegnre  45234  natglobalincr  45236  upwordnul  45239  zm1nn  45654  eluzge0nn0  45664  elfz2z  45667  2ffzoeq  45680  iccpartigtl  45735  iccpartgt  45739  requad01  45933  requad1  45934  requad2  45935  expnegico01  46719  m1modmmod  46727  difmodm1lt  46728  regt1loggt0  46742  refdivmptf  46748  elbigolo1  46763  rege1logbrege0  46764  fllog2  46774  dignn0flhalflem1  46821  eenglngeehlnmlem2  46944  line2  46958  line2xlem  46959  line2x  46960  line2y  46961  itsclc0yqsol  46970  2itscp  46987  inlinecirc02plem  46992  amgmwlem  47369