Theorem 0red 11212

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℝcr 11100  0cc0 11101

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11159  ax-addrcl 11162  ax-rnegex 11172  ax-cnre 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838  df-rex 3090

This theorem is referenced by:  gt0ne0  11680  add20  11727  subge0  11728  lesub0  11732  mulge0  11733  msqgt0  11735  msqge0  11736  gt0ne0d  11779  addgt0d  11790  sublt0d  11841  prodgt0  12063  mulgt1  12077  lt2msq1  12100  fiminre2  12164  supmul1  12185  supmul  12188  nnne0  12271  0mnnnnn0  12537  nn0negleid  12557  neglt  13037  rpgecl  13047  ge0p1rp  13050  ledivge1le  13090  mul2lt0rlt0  13121  mul2lt0rgt0  13122  mul2lt0bi  13125  prodge0rd  13126  max0sub  13223  reltxrnmnf  13370  infmrp1  13372  lincmb01cmp  13523  iccf1o  13524  xov1plusxeqvd  13526  elfz0fzfz0  13663  fz0fzelfz0  13664  elfzo0z  13732  fzofzim  13740  fzo1fzo0n0  13746  elfzodifsumelfzo  13762  ssfzoulel  13791  elfznelfzo  13804  muladdmodid  13948  modltm1p1mod  13961  addmodlteq  13984  expgt1  14138  ltexp2a  14204  expcan  14207  ltexp2  14208  leexp2  14209  leexp2a  14210  zzlesq  14244  expnlbnd2  14272  discr  14278  fi1uzind  14546  ccatsymb  14622  ccat2s1fvw  14678  swrdnd  14694  swrdnnn0nd  14696  swrdswrdlem  14743  swrdswrd  14744  repswswrd  14823  swrd2lsw  14991  2swrd2eqwrdeq  14992  sgnneg  15139  sgnsub  15145  sgnmul  15146  leabs  15352  max0add  15363  absgt0  15378  rlimrege0  15632  iseraltlem2  15736  fsumrecl  15787  o1fsum  15867  cvgcmp  15870  cvgcmpce  15872  geomulcvg  15932  mertenslem2  15941  fprodle  16052  rpnnen2lem4  16274  p1modz1  16318  moddvds  16322  oddge22np1  16408  bitsfzolem  16493  bitsinv1lem  16500  sadcaddlem  16516  nn0rppwr  16620  nn0expgcd  16623  lcmgcdlem  16665  dvdsnprmd  16749  2mulprm  16752  isprm7  16768  qnumgt0  16810  modprm0  16866  qexpz  16962  prmreclem4  16980  4sqlem6  17004  prmgaplem7  17118  gzrngunit  21564  regsumfsum  21566  regsumsupp  21753  fvmptnn04ifd  22991  chfacffsupp  22994  chfacfscmul0  22996  chfacfscmulgsum  22998  chfacfpmmul0  23000  chfacfpmmulgsum  23002  prdsmet  24508  metustexhalf  24694  nlmvscnlem2  24823  nlmvscnlem1  24824  nmo0  24873  blcvx  24936  iihalf1cn  25072  evth  25099  lebnumlem1  25101  lebnumii  25106  htpycc  25120  pcohtpylem  25159  pcoass  25164  pcorevlem  25166  nmoleub2lem3  25255  ipcnlem2  25384  ipcnlem1  25385  rrxcph  25532  rrxmetlem  25547  rrxmet  25548  rrxdstprj1  25549  ehlbase  25555  minveclem3b  25568  minveclem6  25574  pjthlem1  25577  ovolicopnf  25664  ioorcl2  25712  volivth  25747  mbfposr  25792  i1fmulc  25843  itg1mulc  25844  itg1ge0a  25851  mbfi1flim  25863  itg2split  25889  itg2monolem1  25890  itg2monolem3  25892  itg2mono  25893  itg2cnlem2  25902  itgge0  25951  bddiblnc  25982  dvlip  26133  dvlipcn  26134  dveq0  26140  dv11cn  26141  dvlt0  26145  dvfsumge  26162  dgradd2  26406  plydivlem3  26437  mtest  26545  radcnvlem1  26554  radcnv0  26557  radcnvlt1  26559  radcnvle  26561  pserulm  26563  pserdvlem1  26568  pserdv  26570  abelthlem2  26573  abelthlem7  26579  pilem2  26593  pilem3  26594  coseq00topi  26645  tanabsge  26649  cosq34lt1  26670  tanord1  26680  tanord  26681  rplogcl  26747  logdivle  26765  logcnlem3  26787  logcnlem4  26788  dvloglem  26791  logtayl  26803  abscxp2  26836  cxplt  26837  cxple  26838  cxple2a  26842  cxpcn3lem  26890  abscxpbnd  26896  rtprmirr  26903  chordthmlem4  26978  chordthmlem5  26979  asinlem3  27014  atanre  27028  atanlogaddlem  27056  atanlogadd  27057  atanlogsublem  27058  atantan  27066  atans2  27074  efrlim  27112  cxp2limlem  27118  cxp2lim  27119  cxploglim2  27121  divsqrtsumlem  27122  jensenlem2  27130  harmonicubnd  27152  fsumharmonic  27154  dmlogdmgm  27166  lgamgulmlem1  27171  lgamgulmlem2  27172  ftalem1  27215  ftalem2  27216  ftalem5  27219  vmacl  27260  chtwordi  27298  ppiwordi  27304  chtrpcl  27317  fsumfldivdiaglem  27331  fsumvma2  27356  chpval2  27360  chpchtsum  27361  chpub  27362  logfacbnd3  27365  logexprlim  27367  mersenne  27369  lgsdilem  27466  lgsne0  27477  gausslemma2dlem1a  27507  lgseisen  27521  lgsquadlem1  27522  lgsquadlem2  27523  2sqmod  27578  2sqnn0  27580  chebbnd1lem2  27612  chebbnd1lem3  27613  chebbnd1  27614  chtppilimlem1  27615  chtppilimlem2  27616  chtppilim  27617  chebbnd2  27619  chto1lb  27620  chpchtlim  27621  chpo1ub  27622  dchrisumlema  27630  dchrisumlem2  27632  dchrisumlem3  27633  dchrmusumlema  27635  dchrvmasumlem2  27640  dchrvmasumiflem1  27643  dchrisum0flblem1  27650  dchrisum0flblem2  27651  dchrisum0re  27655  dchrisum0lema  27656  dchrisum0  27662  dirith2  27670  mulog2sumlem1  27676  vmalogdivsum2  27680  log2sumbnd  27686  selberg2lem  27692  chpdifbndlem1  27695  chpdifbnd  27697  selberg3lem1  27699  pntrmax  27706  pntrsumo1  27707  pntrlog2bndlem4  27722  pntrlog2bndlem5  27723  pntpbnd1a  27727  pntpbnd1  27728  pntpbnd2  27729  pntlemg  27740  pntlemj  27745  pntlemk  27748  pntlem3  27751  pnt2  27755  pnt  27756  ostth2lem1  27760  padicabv  27772  padicabvcxp  27774  ostth2lem3  27777  ostth2lem4  27778  ostth3  27780  trgcgrg  28762  tgcgr4  28778  axsegconlem7  29251  axsegconlem10  29254  axcontlem2  29293  axcontlem4  29295  axcontlem7  29298  axcontlem10  29301  crctcshwlkn0lem3  30139  crctcshwlkn0  30148  clwlkclwwlklem2a2  30322  clwlkclwwlklem2a  30327  wwlksubclwwlk  30387  frgrogt3nreg  30726  friendshipgt3  30727  minvecolem5  31211  minvecolem6  31212  htthlem  31247  pjhthlem1  31721  sgnval2  33058  nndiffz1  33109  bcm1n  33118  fzo0opth  33126  expgt0b  33139  nexple  33155  oexpled  33158  indf1o  33162  wrdt2ind  33251  cycpmrn  33441  cyc3conja  33455  ccfldextdgrr  34040  constrsslem  34109  constrresqrtcl  34145  constrsqrtcl  34147  cos9thpiminplylem1  34150  pnfneige0  34319  measinb  34589  eulerpartlems  34728  eulerpartlemgc  34730  ballotlemfc0  34861  ballotlemfcc  34862  ballotlemodife  34866  signsply0  34916  signslema  34927  signsvtp  34948  itgexpif  34971  breprexplemc  34997  circlemeth  35005  logdivsqrle  35015  0nn0m1nnn0  35582  cvmliftlem2  35756  dnibndlem9  37053  unbdqndv2lem2  37077  knoppndvlem1  37079  knoppndvlem2  37080  knoppndvlem7  37085  knoppndvlem11  37089  knoppndvlem14  37092  knoppndvlem15  37093  knoppndvlem17  37095  knoppndvlem19  37097  knoppndvlem20  37098  bj-pinftynminfty  37849  poimirlem10  38259  poimirlem11  38260  poimirlem24  38273  poimirlem29  38278  poimirlem31  38280  poimirlem32  38281  poimir  38282  mblfinlem2  38287  ftc1anclem7  38328  ftc1anclem8  38329  ftc1anc  38330  areacirclem1  38337  areacirclem4  38340  areacirc  38342  geomcau  38388  isbnd3b  38414  prdsbnd  38422  bfp  38453  rrnequiv  38464  resdvopclptsd  42773  lcmineqlem2  42775  lcmineqlem3  42776  lcmineqlem10  42783  lcmineqlem12  42785  lcmineqlem23  42796  3lexlogpow5ineq1  42799  3lexlogpow5ineq2  42800  3lexlogpow5ineq4  42801  3lexlogpow5ineq3  42802  3lexlogpow2ineq2  42804  3lexlogpow5ineq5  42805  aks4d1lem1  42807  dvrelog2  42809  dvrelog3  42810  dvrelog2b  42811  0nonelalab  42812  dvrelogpow2b  42813  aks4d1p1p3  42814  aks4d1p1p2  42815  aks4d1p1p4  42816  aks4d1p1p6  42818  aks4d1p1p7  42819  aks4d1p1p5  42820  aks4d1p1  42821  aks4d1p2  42822  aks4d1p3  42823  aks4d1p5  42825  aks4d1p6  42826  aks4d1p7d1  42827  aks4d1p7  42828  aks4d1p8d2  42830  aks4d1p8d3  42831  aks4d1p8  42832  aks4d1p9  42833  posbezout  42845  primrootspoweq0  42851  aks6d1c1  42861  hashscontpow1  42866  aks6d1c2lem4  42872  aks6d1c5lem2  42883  deg1gprod  42885  2np3bcnp1  42889  2ap1caineq  42890  sticksstones7  42897  sticksstones10  42900  sticksstones12a  42902  sticksstones12  42903  sticksstones22  42913  aks6d1c6lem3  42917  bcled  42923  bcle2d  42924  aks6d1c7lem1  42925  aks6d1c7lem2  42926  aks6d1c7  42929  aks5lem6  42937  unitscyglem5  42944  aks5lem8  42946  sn-1ne2  43010  oexpreposd  43061  posqsqznn  43075  redvmptabs  43099  readvrec  43101  re1m1e0m0  43136  re0m0e0  43141  remul01  43146  sn-remul0ord  43147  remulneg2d  43154  rediveq0d  43188  sn-rediv0d  43192  sn-addlt0d  43210  sn-addgt0d  43211  renegmulnnass  43217  zmulcomlem  43219  mulgt0con1dlem  43221  sn-mulgt1d  43231  mulltgt0d  43234  mullt0b2d  43236  sn-mullt0d  43237  sn-msqgt0d  43238  fimgmcyc  43282  dffltz  43346  3cubeslem1  43395  irrapxlem1  43529  irrapxlem2  43530  irrapxlem3  43531  irrapxlem4  43532  pellexlem6  43541  pell14qrgt0  43566  pell1qrgaplem  43580  pellfundex  43593  pellfundrp  43595  monotoddzzfi  43649  jm2.24  43670  jm2.23  43703  jm2.26lem3  43708  jm3.1lem3  43726  sqrtcvallem1  44337  reabsifneg  44338  reabsifpos  44340  sqrtcval  44347  k0004ss2  44858  imo72b2lem1  44875  dvgrat  45002  hashnzfz2  45011  binomcxplemnn0  45039  binomcxplemnotnn0  45046  divlt0gt0d  45985  upbdrech2  46007  xralrple2  46050  xralrple3  46069  reclt0d  46082  reclt0  46086  xrpnf  46179  fsumnncl  46268  fsumsupp0  46274  sumnnodd  46326  lptre2pt  46334  limsupubuz  46407  liminfresre  46473  liminf0  46487  dvmptconst  46609  dvdivbd  46617  dvcosax  46620  dvbdfbdioolem1  46622  dvbdfbdioolem2  46623  ioodvbdlimc1lem1  46625  ioodvbdlimc1lem2  46626  ioodvbdlimc2lem  46628  dvxpaek  46634  dvnxpaek  46636  volioc  46666  volico  46677  stoweidlem1  46695  stoweidlem7  46701  stoweidlem11  46705  stoweidlem25  46719  stoweidlem26  46720  stoweidlem34  46728  stoweidlem36  46730  stoweidlem41  46735  stoweidlem42  46736  stoweidlem44  46738  stoweidlem45  46739  wallispilem3  46761  wallispilem4  46762  wallispi  46764  stirlinglem3  46770  stirlinglem5  46772  stirlinglem6  46773  stirlinglem7  46774  stirlinglem10  46777  stirlinglem11  46778  stirlinglem12  46779  dirkeritg  46796  dirkercncflem2  46798  fourierdlem9  46810  fourierdlem11  46812  fourierdlem12  46813  fourierdlem14  46815  fourierdlem15  46816  fourierdlem19  46820  fourierdlem24  46825  fourierdlem28  46829  fourierdlem30  46831  fourierdlem40  46841  fourierdlem41  46842  fourierdlem43  46844  fourierdlem44  46845  fourierdlem47  46847  fourierdlem50  46850  fourierdlem51  46851  fourierdlem57  46857  fourierdlem60  46860  fourierdlem61  46861  fourierdlem66  46866  fourierdlem68  46868  fourierdlem73  46873  fourierdlem74  46874  fourierdlem75  46875  fourierdlem78  46878  fourierdlem79  46879  fourierdlem83  46883  fourierdlem88  46888  fourierdlem92  46892  fourierdlem93  46893  fourierdlem97  46897  fourierdlem103  46903  fourierdlem104  46904  fourierdlem109  46909  fourierdlem111  46911  sqwvfoura  46922  sqwvfourb  46923  fourierswlem  46924  fouriersw  46925  elaa2lem  46927  etransclem4  46932  etransclem18  46946  etransclem19  46947  etransclem23  46951  etransclem27  46955  etransclem31  46959  etransclem32  46960  etransclem35  46963  etransclem41  46969  etransclem46  46974  etransclem48  46976  rrxtopnfi  46981  qndenserrnbllem  46988  salgencntex  47037  sge0tsms  47074  sge0isum  47121  volicorecl  47240  hoiprodcl  47241  ovnlerp  47256  ovnsubaddlem1  47264  hoiprodcl3  47274  volicore  47275  hoidmvcl  47276  hoidmvlelem1  47289  hoidmvlelem2  47290  hoidmvlelem3  47291  ovnhoi  47297  hoiqssbllem2  47317  volicorege0  47331  vonhoire  47366  pimrecltpos  47402  pimrecltneg  47418  smfmbfcex  47454  nsssmfmbflem  47472  smfrec  47483  smfmullem3  47487  smfdivdmmbl  47532  sharhght  47559  et-sqrtnegnre  47567  ormkglobd  47571  natglobalincr  47573  chnsubseqwl  47575  zm1nn  48016  eluzge0nn0  48026  elfz2z  48029  2ffzoeq  48042  m1modmmod  48078  modm1p1ne  48090  muldvdsfacm1  48101  iccpartigtl  48149  iccpartgt  48153  nprmdvdsfacm1lem4  48352  requad01  48363  requad1  48364  requad2  48365  stgrusgra  48701  gpgedgvtx1  48804  expnegico01  49275  regt1loggt0  49293  refdivmptf  49299  elbigolo1  49314  rege1logbrege0  49315  fllog2  49325  dignn0flhalflem1  49372  eenglngeehlnmlem2  49495  line2  49509  line2xlem  49510  line2x  49511  line2y  49512  itsclc0yqsol  49521  2itscp  49538  inlinecirc02plem  49543  amgmwlem  50579