Theorem 0red 11122

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11012  0cc0 11013

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-1cn 11071  ax-addrcl 11074  ax-rnegex 11084  ax-cnre 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-clel 2808  df-rex 3058

This theorem is referenced by:  gt0ne0  11589  add20  11636  subge0  11637  lesub0  11641  mulge0  11642  msqgt0  11644  msqge0  11645  gt0ne0d  11688  addgt0d  11699  sublt0d  11750  prodgt0  11975  mulgt1  11990  lt2msq1  12013  fiminre2  12077  supmul1  12098  supmul  12101  nnne0  12166  0mnnnnn0  12420  nn0negleid  12440  neglt  12912  rpgecl  12922  ge0p1rp  12925  ledivge1le  12965  mul2lt0rlt0  12996  mul2lt0rgt0  12997  mul2lt0bi  13000  prodge0rd  13001  max0sub  13097  reltxrnmnf  13244  infmrp1  13246  lincmb01cmp  13397  iccf1o  13398  xov1plusxeqvd  13400  elfz0fzfz0  13535  fz0fzelfz0  13536  elfzo0z  13603  fzofzim  13611  fzo1fzo0n0  13617  elfzodifsumelfzo  13633  ssfzoulel  13662  elfznelfzo  13675  muladdmodid  13819  modltm1p1mod  13832  addmodlteq  13855  expgt1  14009  ltexp2a  14075  expcan  14078  ltexp2  14079  leexp2  14080  leexp2a  14081  zzlesq  14115  expnlbnd2  14143  discr  14149  fi1uzind  14416  ccatsymb  14492  ccat2s1fvw  14548  swrdnd  14564  swrdnnn0nd  14566  swrdswrdlem  14613  swrdswrd  14614  repswswrd  14693  swrd2lsw  14861  2swrd2eqwrdeq  14862  leabs  15208  max0add  15219  absgt0  15234  rlimrege0  15488  iseraltlem2  15592  fsumrecl  15643  o1fsum  15722  cvgcmp  15725  cvgcmpce  15727  geomulcvg  15785  mertenslem2  15794  fprodle  15905  rpnnen2lem4  16128  p1modz1  16172  moddvds  16176  oddge22np1  16262  bitsfzolem  16347  bitsinv1lem  16354  sadcaddlem  16370  nn0rppwr  16474  nn0expgcd  16477  lcmgcdlem  16519  dvdsnprmd  16603  2mulprm  16606  isprm7  16621  qnumgt0  16663  modprm0  16719  qexpz  16815  prmreclem4  16833  4sqlem6  16857  prmgaplem7  16971  gzrngunit  21372  regsumfsum  21374  regsumsupp  21561  fvmptnn04ifd  22769  chfacffsupp  22772  chfacfscmul0  22774  chfacfscmulgsum  22776  chfacfpmmul0  22778  chfacfpmmulgsum  22780  prdsmet  24286  metustexhalf  24472  nlmvscnlem2  24601  nlmvscnlem1  24602  nmo0  24651  blcvx  24714  iihalf1cn  24854  evth  24886  lebnumlem1  24888  lebnumii  24893  htpycc  24907  pcohtpylem  24947  pcoass  24952  pcorevlem  24954  nmoleub2lem3  25043  ipcnlem2  25172  ipcnlem1  25173  rrxcph  25320  rrxmetlem  25335  rrxmet  25336  rrxdstprj1  25337  ehlbase  25343  minveclem3b  25356  minveclem6  25362  pjthlem1  25365  ovolicopnf  25453  ioorcl2  25501  volivth  25536  mbfposr  25581  i1fmulc  25632  itg1mulc  25633  itg1ge0a  25640  mbfi1flim  25652  itg2split  25678  itg2monolem1  25679  itg2monolem3  25681  itg2mono  25682  itg2cnlem2  25691  itgge0  25740  bddiblnc  25771  dvlip  25926  dvlipcn  25927  dveq0  25933  dv11cn  25934  dvlt0  25938  dvfsumge  25956  dgradd2  26202  plydivlem3  26231  mtest  26341  radcnvlem1  26350  radcnv0  26353  radcnvlt1  26355  radcnvle  26357  pserulm  26359  pserdvlem1  26365  pserdv  26367  abelthlem2  26370  abelthlem7  26376  pilem2  26390  pilem3  26391  coseq00topi  26439  tanabsge  26443  cosq34lt1  26464  tanord1  26474  tanord  26475  rplogcl  26541  logdivle  26559  logcnlem3  26581  logcnlem4  26582  dvloglem  26585  logtayl  26597  abscxp2  26630  cxplt  26631  cxple  26632  cxple2a  26636  cxpcn3lem  26685  abscxpbnd  26691  rtprmirr  26698  chordthmlem4  26773  chordthmlem5  26774  asinlem3  26809  atanre  26823  atanlogaddlem  26851  atanlogadd  26852  atanlogsublem  26853  atantan  26861  atans2  26869  efrlim  26907  efrlimOLD  26908  cxp2limlem  26914  cxp2lim  26915  cxploglim2  26917  divsqrtsumlem  26918  jensenlem2  26926  harmonicubnd  26948  fsumharmonic  26950  dmlogdmgm  26962  lgamgulmlem1  26967  lgamgulmlem2  26968  ftalem1  27011  ftalem2  27012  ftalem5  27015  vmacl  27056  chtwordi  27094  ppiwordi  27100  chtrpcl  27113  fsumfldivdiaglem  27127  fsumvma2  27153  chpval2  27157  chpchtsum  27158  chpub  27159  logfacbnd3  27162  logexprlim  27164  mersenne  27166  lgsdilem  27263  lgsne0  27274  gausslemma2dlem1a  27304  lgseisen  27318  lgsquadlem1  27319  lgsquadlem2  27320  2sqmod  27375  2sqnn0  27377  chebbnd1lem2  27409  chebbnd1lem3  27410  chebbnd1  27411  chtppilimlem1  27412  chtppilimlem2  27413  chtppilim  27414  chebbnd2  27416  chto1lb  27417  chpchtlim  27418  chpo1ub  27419  dchrisumlema  27427  dchrisumlem2  27429  dchrisumlem3  27430  dchrmusumlema  27432  dchrvmasumlem2  27437  dchrvmasumiflem1  27440  dchrisum0flblem1  27447  dchrisum0flblem2  27448  dchrisum0re  27452  dchrisum0lema  27453  dchrisum0  27459  dirith2  27467  mulog2sumlem1  27473  vmalogdivsum2  27477  log2sumbnd  27483  selberg2lem  27489  chpdifbndlem1  27492  chpdifbnd  27494  selberg3lem1  27496  pntrmax  27503  pntrsumo1  27504  pntrlog2bndlem4  27519  pntrlog2bndlem5  27520  pntpbnd1a  27524  pntpbnd1  27525  pntpbnd2  27526  pntlemg  27537  pntlemj  27542  pntlemk  27545  pntlem3  27548  pnt2  27552  pnt  27553  ostth2lem1  27557  padicabv  27569  padicabvcxp  27571  ostth2lem3  27574  ostth2lem4  27575  ostth3  27577  trgcgrg  28494  tgcgr4  28510  axsegconlem7  28903  axsegconlem10  28906  axcontlem2  28945  axcontlem4  28947  axcontlem7  28950  axcontlem10  28953  crctcshwlkn0lem3  29792  crctcshwlkn0  29801  clwlkclwwlklem2a2  29975  clwlkclwwlklem2a  29980  wwlksubclwwlk  30040  frgrogt3nreg  30379  friendshipgt3  30380  minvecolem5  30863  minvecolem6  30864  htthlem  30899  pjhthlem1  31373  sgnval2  32722  nndiffz1  32773  bcm1n  32782  fzo0opth  32790  expgt0b  32804  sgnneg  32821  sgnmul  32823  sgnsub  32825  nexple  32832  oexpled  32835  indf1o  32852  wrdt2ind  32941  cycpmrn  33119  cyc3conja  33133  ccfldextdgrr  33706  constrsslem  33775  constrresqrtcl  33811  constrsqrtcl  33813  cos9thpiminplylem1  33816  pnfneige0  33985  measinb  34255  eulerpartlems  34394  eulerpartlemgc  34396  ballotlemfc0  34527  ballotlemfcc  34528  ballotlemodife  34532  signsply0  34585  signslema  34596  signsvtp  34617  itgexpif  34640  breprexplemc  34666  circlemeth  34674  logdivsqrle  34684  0nn0m1nnn0  35178  cvmliftlem2  35351  dnibndlem9  36551  unbdqndv2lem2  36575  knoppndvlem1  36577  knoppndvlem2  36578  knoppndvlem7  36583  knoppndvlem11  36587  knoppndvlem14  36590  knoppndvlem15  36591  knoppndvlem17  36593  knoppndvlem19  36595  knoppndvlem20  36596  bj-pinftynminfty  37292  poimirlem10  37691  poimirlem11  37692  poimirlem24  37705  poimirlem29  37710  poimirlem31  37712  poimirlem32  37713  poimir  37714  mblfinlem2  37719  ftc1anclem7  37760  ftc1anclem8  37761  ftc1anc  37762  areacirclem1  37769  areacirclem4  37772  areacirc  37774  geomcau  37820  isbnd3b  37846  prdsbnd  37854  bfp  37885  rrnequiv  37896  resdvopclptsd  42142  lcmineqlem2  42144  lcmineqlem3  42145  lcmineqlem10  42152  lcmineqlem12  42154  lcmineqlem23  42165  3lexlogpow5ineq1  42168  3lexlogpow5ineq2  42169  3lexlogpow5ineq4  42170  3lexlogpow5ineq3  42171  3lexlogpow2ineq2  42173  3lexlogpow5ineq5  42174  aks4d1lem1  42176  dvrelog2  42178  dvrelog3  42179  dvrelog2b  42180  0nonelalab  42181  dvrelogpow2b  42182  aks4d1p1p3  42183  aks4d1p1p2  42184  aks4d1p1p4  42185  aks4d1p1p6  42187  aks4d1p1p7  42188  aks4d1p1p5  42189  aks4d1p1  42190  aks4d1p2  42191  aks4d1p3  42192  aks4d1p5  42194  aks4d1p6  42195  aks4d1p7d1  42196  aks4d1p7  42197  aks4d1p8d2  42199  aks4d1p8d3  42200  aks4d1p8  42201  aks4d1p9  42202  posbezout  42214  primrootspoweq0  42220  aks6d1c1  42230  hashscontpow1  42235  aks6d1c2lem4  42241  aks6d1c5lem2  42252  deg1gprod  42254  2np3bcnp1  42258  2ap1caineq  42259  sticksstones7  42266  sticksstones10  42269  sticksstones12a  42271  sticksstones12  42272  sticksstones22  42282  aks6d1c6lem3  42286  bcled  42292  bcle2d  42293  aks6d1c7lem1  42294  aks6d1c7lem2  42295  aks6d1c7  42298  aks5lem6  42306  unitscyglem5  42313  aks5lem8  42315  sn-1ne2  42384  oexpreposd  42441  posqsqznn  42455  redvmptabs  42479  readvrec  42481  re1m1e0m0  42516  re0m0e0  42521  remul01  42526  sn-remul0ord  42527  remulneg2d  42534  sn-addlt0d  42577  sn-addgt0d  42578  renegmulnnass  42584  zmulcomlem  42586  mulgt0con1dlem  42588  sn-mulgt1d  42598  mulltgt0d  42601  mullt0b2d  42603  sn-mullt0d  42604  sn-msqgt0d  42605  fimgmcyc  42653  dffltz  42753  3cubeslem1  42802  irrapxlem1  42940  irrapxlem2  42941  irrapxlem3  42942  irrapxlem4  42943  pellexlem6  42952  pell14qrgt0  42977  pell1qrgaplem  42991  pellfundex  43004  pellfundrp  43006  monotoddzzfi  43060  jm2.24  43081  jm2.23  43114  jm2.26lem3  43119  jm3.1lem3  43137  sqrtcvallem1  43749  reabsifneg  43750  reabsifpos  43752  sqrtcval  43759  k0004ss2  44270  imo72b2lem1  44287  dvgrat  44430  hashnzfz2  44439  binomcxplemnn0  44467  binomcxplemnotnn0  44474  divlt0gt0d  45412  upbdrech2  45434  xralrple2  45478  xralrple3  45497  reclt0d  45510  reclt0  45514  xrpnf  45608  fsumnncl  45697  fsumsupp0  45703  sumnnodd  45755  lptre2pt  45763  limsupubuz  45836  liminfresre  45902  liminf0  45916  dvmptconst  46038  dvdivbd  46046  dvcosax  46049  dvbdfbdioolem1  46051  dvbdfbdioolem2  46052  ioodvbdlimc1lem1  46054  ioodvbdlimc1lem2  46055  ioodvbdlimc2lem  46057  dvxpaek  46063  dvnxpaek  46065  volioc  46095  volico  46106  stoweidlem1  46124  stoweidlem7  46130  stoweidlem11  46134  stoweidlem25  46148  stoweidlem26  46149  stoweidlem34  46157  stoweidlem36  46159  stoweidlem41  46164  stoweidlem42  46165  stoweidlem44  46167  stoweidlem45  46168  wallispilem3  46190  wallispilem4  46191  wallispi  46193  stirlinglem3  46199  stirlinglem5  46201  stirlinglem6  46202  stirlinglem7  46203  stirlinglem10  46206  stirlinglem11  46207  stirlinglem12  46208  dirkeritg  46225  dirkercncflem2  46227  fourierdlem9  46239  fourierdlem11  46241  fourierdlem12  46242  fourierdlem14  46244  fourierdlem15  46245  fourierdlem19  46249  fourierdlem24  46254  fourierdlem28  46258  fourierdlem30  46260  fourierdlem40  46270  fourierdlem41  46271  fourierdlem43  46273  fourierdlem44  46274  fourierdlem47  46276  fourierdlem50  46279  fourierdlem51  46280  fourierdlem57  46286  fourierdlem60  46289  fourierdlem61  46290  fourierdlem66  46295  fourierdlem68  46297  fourierdlem73  46302  fourierdlem74  46303  fourierdlem75  46304  fourierdlem78  46307  fourierdlem79  46308  fourierdlem83  46312  fourierdlem88  46317  fourierdlem92  46321  fourierdlem93  46322  fourierdlem97  46326  fourierdlem103  46332  fourierdlem104  46333  fourierdlem109  46338  fourierdlem111  46340  sqwvfoura  46351  sqwvfourb  46352  fourierswlem  46353  fouriersw  46354  elaa2lem  46356  etransclem4  46361  etransclem18  46375  etransclem19  46376  etransclem23  46380  etransclem27  46384  etransclem31  46388  etransclem32  46389  etransclem35  46392  etransclem41  46398  etransclem46  46403  etransclem48  46405  rrxtopnfi  46410  qndenserrnbllem  46417  salgencntex  46466  sge0tsms  46503  sge0isum  46550  volicorecl  46669  hoiprodcl  46670  ovnlerp  46685  ovnsubaddlem1  46693  hoiprodcl3  46703  volicore  46704  hoidmvcl  46705  hoidmvlelem1  46718  hoidmvlelem2  46719  hoidmvlelem3  46720  ovnhoi  46726  hoiqssbllem2  46746  volicorege0  46760  vonhoire  46795  pimrecltpos  46831  pimrecltneg  46847  smfmbfcex  46883  nsssmfmbflem  46901  smfrec  46912  smfmullem3  46916  smfdivdmmbl  46961  sharhght  46988  et-sqrtnegnre  46996  ormkglobd  46998  natglobalincr  47000  chnsubseqwl  47002  zm1nn  47427  eluzge0nn0  47437  elfz2z  47440  2ffzoeq  47452  m1modmmod  47483  modm1p1ne  47495  iccpartigtl  47548  iccpartgt  47552  requad01  47746  requad1  47747  requad2  47748  stgrusgra  48084  gpgedgvtx1  48187  expnegico01  48644  regt1loggt0  48662  refdivmptf  48668  elbigolo1  48683  rege1logbrege0  48684  fllog2  48694  dignn0flhalflem1  48741  eenglngeehlnmlem2  48864  line2  48878  line2xlem  48879  line2x  48880  line2y  48881  itsclc0yqsol  48890  2itscp  48907  inlinecirc02plem  48912  amgmwlem  49928