Theorem 0red 11229

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℝcr 11117  0cc0 11118

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-1cn 11176  ax-addrcl 11179  ax-rnegex 11189  ax-cnre 11191

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-clel 2841  df-rex 3093

This theorem is used by:  gt0ne0  11697  add20  11744  subge0  11745  lesub0  11749  mulge0  11750  msqgt0  11752  msqge0  11753  gt0ne0d  11796  addgt0d  11807  sublt0d  11858  prodgt0  12080  mulgt1  12094  lt2msq1  12117  fiminre2  12181  supmul1  12202  supmul  12205  nnne0  12288  0mnnnnn0  12554  nn0negleid  12574  neglt  13054  rpgecl  13064  ge0p1rp  13067  ledivge1le  13107  mul2lt0rlt0  13138  mul2lt0rgt0  13139  mul2lt0bi  13142  prodge0rd  13143  max0sub  13240  reltxrnmnf  13387  infmrp1  13389  lincmb01cmp  13540  iccf1o  13541  xov1plusxeqvd  13543  elfz0fzfz0  13680  fz0fzelfz0  13681  elfzo0z  13749  fzofzim  13757  fzo1fzo0n0  13763  elfzodifsumelfzo  13779  ssfzoulel  13808  elfznelfzo  13821  muladdmodid  13966  modltm1p1mod  13979  addmodlteq  14002  expgt1  14156  ltexp2a  14222  expcan  14225  ltexp2  14226  leexp2  14227  leexp2a  14228  zzlesq  14262  expnlbnd2  14290  discr  14296  fi1uzind  14564  ccatsymb  14640  ccat2s1fvw  14698  swrdnd  14716  swrdnnn0nd  14718  swrdswrdlem  14765  swrdswrd  14766  repswswrd  14847  swrd2lsw  15015  2swrd2eqwrdeq  15016  sgnneg  15163  sgnsub  15169  sgnmul  15170  leabs  15376  max0add  15387  absgt0  15402  rlimrege0  15656  iseraltlem2  15760  fsumrecl  15811  o1fsum  15891  cvgcmp  15894  cvgcmpce  15896  geomulcvg  15956  mertenslem2  15965  fprodle  16076  rpnnen2lem4  16298  p1modz1  16342  moddvds  16346  oddge22np1  16432  bitsfzolem  16517  bitsinv1lem  16524  sadcaddlem  16540  nn0rppwr  16644  nn0expgcd  16647  lcmgcdlem  16689  dvdsnprmd  16773  2mulprm  16776  isprm7  16792  qnumgt0  16834  modprm0  16890  qexpz  16986  prmreclem4  17004  4sqlem6  17028  prmgaplem7  17142  gzrngunit  21620  regsumfsum  21622  regsumsupp  21809  fvmptnn04ifd  23047  chfacffsupp  23050  chfacfscmul0  23052  chfacfscmulgsum  23054  chfacfpmmul0  23056  chfacfpmmulgsum  23058  prdsmet  24564  metustexhalf  24750  nlmvscnlem2  24879  nlmvscnlem1  24880  nmo0  24929  blcvx  24992  iihalf1cn  25128  evth  25155  lebnumlem1  25157  lebnumii  25162  htpycc  25176  pcohtpylem  25215  pcoass  25220  pcorevlem  25222  nmoleub2lem3  25311  ipcnlem2  25440  ipcnlem1  25441  rrxcph  25588  rrxmetlem  25603  rrxmet  25604  rrxdstprj1  25605  ehlbase  25611  minveclem3b  25624  minveclem6  25630  pjthlem1  25633  ovolicopnf  25720  ioorcl2  25768  volivth  25803  mbfposr  25848  i1fmulc  25899  itg1mulc  25900  itg1ge0a  25907  mbfi1flim  25919  itg2split  25945  itg2monolem1  25946  itg2monolem3  25948  itg2mono  25949  itg2cnlem2  25958  itgge0  26007  bddiblnc  26038  dvlip  26189  dvlipcn  26190  dveq0  26196  dv11cn  26197  dvlt0  26201  dvfsumge  26218  dgradd2  26462  plydivlem3  26493  mtest  26604  radcnvlem1  26613  radcnv0  26616  radcnvlt1  26618  radcnvle  26620  pserulm  26622  pserdvlem1  26627  pserdv  26629  abelthlem2  26632  abelthlem7  26638  pilem2  26652  pilem3  26653  coseq00topi  26704  tanabsge  26708  cosq34lt1  26729  tanord1  26739  tanord  26740  rplogcl  26806  logdivle  26824  logcnlem3  26846  logcnlem4  26847  dvloglem  26850  logtayl  26862  abscxp2  26895  cxplt  26896  cxple  26897  cxple2a  26901  cxpcn3lem  26949  abscxpbnd  26955  rtprmirr  26962  chordthmlem4  27037  chordthmlem5  27038  asinlem3  27073  atanre  27087  atanlogaddlem  27115  atanlogadd  27116  atanlogsublem  27117  atantan  27125  atans2  27133  efrlim  27171  cxp2limlem  27177  cxp2lim  27178  cxploglim2  27180  divsqrtsumlem  27181  jensenlem2  27189  harmonicubnd  27211  fsumharmonic  27213  dmlogdmgm  27225  lgamgulmlem1  27230  lgamgulmlem2  27231  ftalem1  27274  ftalem2  27275  ftalem5  27278  vmacl  27319  chtwordi  27357  ppiwordi  27363  chtrpcl  27376  fsumfldivdiaglem  27390  fsumvma2  27415  chpval2  27419  chpchtsum  27420  chpub  27421  logfacbnd3  27424  logexprlim  27426  mersenne  27428  lgsdilem  27525  lgsne0  27536  gausslemma2dlem1a  27566  lgseisen  27580  lgsquadlem1  27581  lgsquadlem2  27582  2sqmod  27637  2sqnn0  27639  chebbnd1lem2  27671  chebbnd1lem3  27672  chebbnd1  27673  chtppilimlem1  27674  chtppilimlem2  27675  chtppilim  27676  chebbnd2  27678  chto1lb  27679  chpchtlim  27680  chpo1ub  27681  dchrisumlema  27689  dchrisumlem2  27691  dchrisumlem3  27692  dchrmusumlema  27694  dchrvmasumlem2  27699  dchrvmasumiflem1  27702  dchrisum0flblem1  27709  dchrisum0flblem2  27710  dchrisum0re  27714  dchrisum0lema  27715  dchrisum0  27721  dirith2  27729  mulog2sumlem1  27735  vmalogdivsum2  27739  log2sumbnd  27745  selberg2lem  27751  chpdifbndlem1  27754  chpdifbnd  27756  selberg3lem1  27758  pntrmax  27765  pntrsumo1  27766  pntrlog2bndlem4  27781  pntrlog2bndlem5  27782  pntpbnd1a  27786  pntpbnd1  27787  pntpbnd2  27788  pntlemg  27799  pntlemj  27804  pntlemk  27807  pntlem3  27810  pnt2  27814  pnt  27815  ostth2lem1  27819  padicabv  27831  padicabvcxp  27833  ostth2lem3  27836  ostth2lem4  27837  ostth3  27839  trgcgrg  28821  tgcgr4  28837  axsegconlem7  29310  axsegconlem10  29313  axcontlem2  29352  axcontlem4  29354  axcontlem7  29357  axcontlem10  29360  crctcshwlkn0lem3  30198  crctcshwlkn0  30207  clwlkclwwlklem2a2  30381  clwlkclwwlklem2a  30386  wwlksubclwwlk  30446  frgrogt3nreg  30785  friendshipgt3  30786  minvecolem5  31270  minvecolem6  31271  htthlem  31306  pjhthlem1  31780  sgnval2  33117  nndiffz1  33168  bcm1n  33177  fzo0opth  33185  expgt0b  33198  nexple  33214  oexpled  33217  indf1o  33221  wrdt2ind  33306  cycpmrn  33494  cyc3conja  33508  ccfldextdgrr  34093  constrsslem  34162  constrresqrtcl  34198  constrsqrtcl  34200  cos9thpiminplylem1  34203  pnfneige0  34372  measinb  34643  eulerpartlems  34782  eulerpartlemgc  34784  ballotlemfc0  34915  ballotlemfcc  34916  ballotlemodife  34920  signsply0  34970  signslema  34981  signsvtp  35002  itgexpif  35025  breprexplemc  35051  circlemeth  35059  logdivsqrle  35069  0nn0m1nnn0  35628  cvmliftlem2  35799  dnibndlem9  37116  unbdqndv2lem2  37140  knoppndvlem1  37142  knoppndvlem2  37143  knoppndvlem7  37148  knoppndvlem11  37152  knoppndvlem14  37155  knoppndvlem15  37156  knoppndvlem17  37158  knoppndvlem19  37160  knoppndvlem20  37161  bj-pinftynminfty  37912  poimirlem10  38322  poimirlem11  38323  poimirlem24  38336  poimirlem29  38341  poimirlem31  38343  poimirlem32  38344  poimir  38345  mblfinlem2  38350  ftc1anclem7  38391  ftc1anclem8  38392  ftc1anc  38393  areacirclem1  38400  areacirclem4  38403  areacirc  38405  geomcau  38451  isbnd3b  38477  prdsbnd  38485  bfp  38516  rrnequiv  38527  resdvopclptsd  42836  lcmineqlem2  42838  lcmineqlem3  42839  lcmineqlem10  42846  lcmineqlem12  42848  lcmineqlem23  42859  3lexlogpow5ineq1  42862  3lexlogpow5ineq2  42863  3lexlogpow5ineq4  42864  3lexlogpow5ineq3  42865  3lexlogpow2ineq2  42867  3lexlogpow5ineq5  42868  aks4d1lem1  42870  dvrelog2  42872  dvrelog3  42873  dvrelog2b  42874  0nonelalab  42875  dvrelogpow2b  42876  aks4d1p1p3  42877  aks4d1p1p2  42878  aks4d1p1p4  42879  aks4d1p1p6  42881  aks4d1p1p7  42882  aks4d1p1p5  42883  aks4d1p1  42884  aks4d1p2  42885  aks4d1p3  42886  aks4d1p5  42888  aks4d1p6  42889  aks4d1p7d1  42890  aks4d1p7  42891  aks4d1p8d2  42893  aks4d1p8d3  42894  aks4d1p8  42895  aks4d1p9  42896  posbezout  42908  primrootspoweq0  42914  aks6d1c1  42924  hashscontpow1  42929  aks6d1c2lem4  42935  aks6d1c5lem2  42946  deg1gprod  42948  2np3bcnp1  42952  2ap1caineq  42953  sticksstones7  42960  sticksstones10  42963  sticksstones12a  42965  sticksstones12  42966  sticksstones22  42976  aks6d1c6lem3  42980  bcled  42986  bcle2d  42987  aks6d1c7lem1  42988  aks6d1c7lem2  42989  aks6d1c7  42992  aks5lem6  43000  unitscyglem5  43007  aks5lem8  43009  sn-1ne2  43073  oexpreposd  43124  posqsqznn  43138  redvmptabs  43162  readvrec  43164  re1m1e0m0  43199  re0m0e0  43204  remul01  43209  sn-remul0ord  43210  remulneg2d  43217  rediveq0d  43251  sn-rediv0d  43255  sn-addlt0d  43273  sn-addgt0d  43274  renegmulnnass  43280  zmulcomlem  43282  mulgt0con1dlem  43284  sn-mulgt1d  43294  mulltgt0d  43297  mullt0b2d  43299  sn-mullt0d  43300  sn-msqgt0d  43301  fimgmcyc  43343  dffltz  43407  3cubeslem1  43456  irrapxlem1  43590  irrapxlem2  43591  irrapxlem3  43592  irrapxlem4  43593  pellexlem6  43602  pell14qrgt0  43627  pell1qrgaplem  43641  pellfundex  43654  pellfundrp  43656  monotoddzzfi  43710  jm2.24  43731  jm2.23  43764  jm2.26lem3  43769  jm3.1lem3  43787  sqrtcvallem1  44398  reabsifneg  44399  reabsifpos  44401  sqrtcval  44408  k0004ss2  44919  imo72b2lem1  44936  dvgrat  45063  hashnzfz2  45072  binomcxplemnn0  45100  binomcxplemnotnn0  45107  divlt0gt0d  46046  upbdrech2  46068  xralrple2  46111  xralrple3  46130  reclt0d  46143  reclt0  46147  xrpnf  46240  fsumnncl  46329  fsumsupp0  46335  sumnnodd  46387  lptre2pt  46395  limsupubuz  46468  liminfresre  46534  liminf0  46548  dvmptconst  46670  dvdivbd  46678  dvcosax  46681  dvbdfbdioolem1  46683  dvbdfbdioolem2  46684  ioodvbdlimc1lem1  46686  ioodvbdlimc1lem2  46687  ioodvbdlimc2lem  46689  dvxpaek  46695  dvnxpaek  46697  volioc  46727  volico  46738  stoweidlem1  46756  stoweidlem7  46762  stoweidlem11  46766  stoweidlem25  46780  stoweidlem26  46781  stoweidlem34  46789  stoweidlem36  46791  stoweidlem41  46796  stoweidlem42  46797  stoweidlem44  46799  stoweidlem45  46800  wallispilem3  46822  wallispilem4  46823  wallispi  46825  stirlinglem3  46831  stirlinglem5  46833  stirlinglem6  46834  stirlinglem7  46835  stirlinglem10  46838  stirlinglem11  46839  stirlinglem12  46840  dirkeritg  46857  dirkercncflem2  46859  fourierdlem9  46871  fourierdlem11  46873  fourierdlem12  46874  fourierdlem14  46876  fourierdlem15  46877  fourierdlem19  46881  fourierdlem24  46886  fourierdlem28  46890  fourierdlem30  46892  fourierdlem40  46902  fourierdlem41  46903  fourierdlem43  46905  fourierdlem44  46906  fourierdlem47  46908  fourierdlem50  46911  fourierdlem51  46912  fourierdlem57  46918  fourierdlem60  46921  fourierdlem61  46922  fourierdlem66  46927  fourierdlem68  46929  fourierdlem73  46934  fourierdlem74  46935  fourierdlem75  46936  fourierdlem78  46939  fourierdlem79  46940  fourierdlem83  46944  fourierdlem88  46949  fourierdlem92  46953  fourierdlem93  46954  fourierdlem97  46958  fourierdlem103  46964  fourierdlem104  46965  fourierdlem109  46970  fourierdlem111  46972  sqwvfoura  46983  sqwvfourb  46984  fourierswlem  46985  fouriersw  46986  elaa2lem  46988  etransclem4  46993  etransclem18  47007  etransclem19  47008  etransclem23  47012  etransclem27  47016  etransclem31  47020  etransclem32  47021  etransclem35  47024  etransclem41  47030  etransclem46  47035  etransclem48  47037  rrxtopnfi  47042  qndenserrnbllem  47049  salgencntex  47098  sge0tsms  47135  sge0isum  47182  volicorecl  47301  hoiprodcl  47302  ovnlerp  47317  ovnsubaddlem1  47325  hoiprodcl3  47335  volicore  47336  hoidmvcl  47337  hoidmvlelem1  47350  hoidmvlelem2  47351  hoidmvlelem3  47352  ovnhoi  47358  hoiqssbllem2  47378  volicorege0  47392  vonhoire  47427  pimrecltpos  47463  pimrecltneg  47479  smfmbfcex  47515  nsssmfmbflem  47533  smfrec  47544  smfmullem3  47548  smfdivdmmbl  47593  sharhght  47620  et-sqrtnegnre  47628  ormkglobd  47632  natglobalincr  47634  chnsubseqwl  47636  zm1nn  48080  eluzge0nn0  48090  elfz2z  48093  2ffzoeq  48106  m1modmmod  48142  modm1p1ne  48154  muldvdsfacm1  48165  iccpartigtl  48213  iccpartgt  48217  nprmdvdsfacm1lem4  48416  requad01  48427  requad1  48428  requad2  48429  stgrusgra  48765  gpgedgvtx1  48868  expnegico01  49339  regt1loggt0  49357  refdivmptf  49363  elbigolo1  49378  rege1logbrege0  49379  fllog2  49389  dignn0flhalflem1  49436  eenglngeehlnmlem2  49559  line2  49573  line2xlem  49574  line2x  49575  line2y  49576  itsclc0yqsol  49585  2itscp  49602  inlinecirc02plem  49607  amgmwlem  50691