Theorem 0red 11261

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℝcr 11151  0cc0 11152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-addrcl 11213  ax-rnegex 11223  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813  df-rex 3068

This theorem is referenced by:  gt0ne0  11725  add20  11772  subge0  11773  lesub0  11777  mulge0  11778  msqgt0  11780  msqge0  11781  addgt0d  11835  sublt0d  11886  prodgt0  12111  mulgt1  12126  lt2msq1  12149  fiminre2  12213  supmul1  12234  supmul  12237  nnne0  12297  0mnnnnn0  12555  nn0negleid  12575  rpgecl  13060  ge0p1rp  13063  ledivge1le  13103  mul2lt0rlt0  13134  mul2lt0rgt0  13135  mul2lt0bi  13138  prodge0rd  13139  max0sub  13234  reltxrnmnf  13380  infmrp1  13382  lincmb01cmp  13531  iccf1o  13532  xov1plusxeqvd  13534  elfz0fzfz0  13669  fz0fzelfz0  13670  elfzo0z  13737  fzofzim  13745  fzo1fzo0n0  13750  elfzodifsumelfzo  13766  ssfzoulel  13795  elfznelfzo  13807  muladdmodid  13947  modltm1p1mod  13960  addmodlteq  13983  expgt1  14137  ltexp2a  14202  expcan  14205  ltexp2  14206  leexp2  14207  leexp2a  14208  zzlesq  14241  expnlbnd2  14269  discr  14275  fi1uzind  14542  ccatsymb  14616  ccat2s1fvw  14672  swrdnd  14688  swrdnnn0nd  14690  swrdswrdlem  14738  swrdswrd  14739  repswswrd  14818  swrd2lsw  14987  2swrd2eqwrdeq  14988  leabs  15334  max0add  15345  absgt0  15359  rlimrege0  15611  iseraltlem2  15715  fsumrecl  15766  o1fsum  15845  cvgcmp  15848  cvgcmpce  15850  geomulcvg  15908  mertenslem2  15917  fprodle  16028  rpnnen2lem4  16249  p1modz1  16293  moddvds  16297  oddge22np1  16382  bitsfzolem  16467  bitsinv1lem  16474  sadcaddlem  16490  nn0rppwr  16594  nn0expgcd  16597  lcmgcdlem  16639  dvdsnprmd  16723  2mulprm  16726  isprm7  16741  qnumgt0  16783  modprm0  16838  qexpz  16934  prmreclem4  16952  4sqlem6  16976  prmgaplem7  17090  gzrngunit  21468  regsumfsum  21470  regsumsupp  21657  fvmptnn04ifd  22874  chfacffsupp  22877  chfacfscmul0  22879  chfacfscmulgsum  22881  chfacfpmmul0  22883  chfacfpmmulgsum  22885  prdsmet  24395  metustexhalf  24584  nlmvscnlem2  24721  nlmvscnlem1  24722  nmo0  24771  blcvx  24833  iihalf1cn  24972  evth  25004  lebnumlem1  25006  lebnumii  25011  htpycc  25025  pcohtpylem  25065  pcoass  25070  pcorevlem  25072  nmoleub2lem3  25161  ipcnlem2  25291  ipcnlem1  25292  rrxcph  25439  rrxmetlem  25454  rrxmet  25455  rrxdstprj1  25456  ehlbase  25462  minveclem3b  25475  minveclem6  25481  pjthlem1  25484  ovolicopnf  25572  ioorcl2  25620  volivth  25655  mbfposr  25700  i1fmulc  25752  itg1mulc  25753  itg1ge0a  25760  mbfi1flim  25772  itg2split  25798  itg2monolem1  25799  itg2monolem3  25801  itg2mono  25802  itg2cnlem2  25811  itgge0  25860  bddiblnc  25891  dvlip  26046  dvlipcn  26047  dveq0  26053  dv11cn  26054  dvlt0  26058  dvfsumge  26076  dgradd2  26322  plydivlem3  26351  mtest  26461  radcnvlem1  26470  radcnv0  26473  radcnvlt1  26475  radcnvle  26477  pserulm  26479  pserdvlem1  26485  pserdv  26487  abelthlem2  26490  abelthlem7  26496  pilem2  26510  pilem3  26511  coseq00topi  26558  tanabsge  26562  cosq34lt1  26583  tanord1  26593  tanord  26594  rplogcl  26660  logdivle  26678  logcnlem3  26700  logcnlem4  26701  dvloglem  26704  logtayl  26716  abscxp2  26749  cxplt  26750  cxple  26751  cxple2a  26755  cxpcn3lem  26804  abscxpbnd  26810  rtprmirr  26817  chordthmlem4  26892  chordthmlem5  26893  asinlem3  26928  atanre  26942  atanlogaddlem  26970  atanlogadd  26971  atanlogsublem  26972  atantan  26980  atans2  26988  efrlim  27026  efrlimOLD  27027  cxp2limlem  27033  cxp2lim  27034  cxploglim2  27036  divsqrtsumlem  27037  jensenlem2  27045  harmonicubnd  27067  fsumharmonic  27069  dmlogdmgm  27081  lgamgulmlem1  27086  lgamgulmlem2  27087  ftalem1  27130  ftalem2  27131  ftalem5  27134  vmacl  27175  chtwordi  27213  ppiwordi  27219  chtrpcl  27232  fsumfldivdiaglem  27246  fsumvma2  27272  chpval2  27276  chpchtsum  27277  chpub  27278  logfacbnd3  27281  logexprlim  27283  mersenne  27285  lgsdilem  27382  lgsne0  27393  gausslemma2dlem1a  27423  lgseisen  27437  lgsquadlem1  27438  lgsquadlem2  27439  2sqmod  27494  2sqnn0  27496  chebbnd1lem2  27528  chebbnd1lem3  27529  chebbnd1  27530  chtppilimlem1  27531  chtppilimlem2  27532  chtppilim  27533  chebbnd2  27535  chto1lb  27536  chpchtlim  27537  chpo1ub  27538  dchrisumlema  27546  dchrisumlem2  27548  dchrisumlem3  27549  dchrmusumlema  27551  dchrvmasumlem2  27556  dchrvmasumiflem1  27559  dchrisum0flblem1  27566  dchrisum0flblem2  27567  dchrisum0re  27571  dchrisum0lema  27572  dchrisum0  27578  dirith2  27586  mulog2sumlem1  27592  vmalogdivsum2  27596  log2sumbnd  27602  selberg2lem  27608  chpdifbndlem1  27611  chpdifbnd  27613  selberg3lem1  27615  pntrmax  27622  pntrsumo1  27623  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntpbnd1a  27643  pntpbnd1  27644  pntpbnd2  27645  pntlemg  27656  pntlemj  27661  pntlemk  27664  pntlem3  27667  pnt2  27671  pnt  27672  ostth2lem1  27676  padicabv  27688  padicabvcxp  27690  ostth2lem3  27693  ostth2lem4  27694  ostth3  27696  trgcgrg  28537  tgcgr4  28553  axsegconlem7  28952  axsegconlem10  28955  axcontlem2  28994  axcontlem4  28996  axcontlem7  28999  axcontlem10  29002  crctcshwlkn0lem3  29841  crctcshwlkn0  29850  clwlkclwwlklem2a2  30021  clwlkclwwlklem2a  30026  wwlksubclwwlk  30086  frgrogt3nreg  30425  friendshipgt3  30426  minvecolem5  30909  minvecolem6  30910  htthlem  30945  pjhthlem1  31419  nndiffz1  32794  bcm1n  32802  fzo0opth  32812  expgt0b  32822  wrdt2ind  32922  cycpmrn  33145  cyc3conja  33159  ccfldextdgrr  33696  constrsslem  33745  pnfneige0  33911  nexple  33989  indf1o  34004  measinb  34201  eulerpartlems  34341  eulerpartlemgc  34343  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemodife  34478  sgnneg  34521  sgnmul  34523  sgnsub  34525  signsply0  34544  signslema  34555  signsvtp  34576  itgexpif  34599  breprexplemc  34625  circlemeth  34633  logdivsqrle  34643  0nn0m1nnn0  35096  cvmliftlem2  35270  dnibndlem9  36468  unbdqndv2lem2  36492  knoppndvlem1  36494  knoppndvlem2  36495  knoppndvlem7  36500  knoppndvlem11  36504  knoppndvlem14  36507  knoppndvlem15  36508  knoppndvlem17  36510  knoppndvlem19  36512  knoppndvlem20  36513  bj-pinftynminfty  37209  poimirlem10  37616  poimirlem11  37617  poimirlem24  37630  poimirlem29  37635  poimirlem31  37637  poimirlem32  37638  poimir  37639  mblfinlem2  37644  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  areacirclem1  37694  areacirclem4  37697  areacirc  37699  geomcau  37745  isbnd3b  37771  prdsbnd  37779  bfp  37810  rrnequiv  37821  resdvopclptsd  42009  lcmineqlem2  42011  lcmineqlem3  42012  lcmineqlem10  42019  lcmineqlem12  42021  lcmineqlem23  42032  3lexlogpow5ineq1  42035  3lexlogpow5ineq2  42036  3lexlogpow5ineq4  42037  3lexlogpow5ineq3  42038  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1lem1  42043  dvrelog2  42045  dvrelog3  42046  dvrelog2b  42047  0nonelalab  42048  dvrelogpow2b  42049  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p2  42058  aks4d1p3  42059  aks4d1p5  42061  aks4d1p6  42062  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8d2  42066  aks4d1p8d3  42067  aks4d1p8  42068  aks4d1p9  42069  posbezout  42081  primrootspoweq0  42087  aks6d1c1  42097  hashscontpow1  42102  aks6d1c2lem4  42108  aks6d1c5lem2  42119  deg1gprod  42121  2np3bcnp1  42125  2ap1caineq  42126  sticksstones7  42133  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  sticksstones22  42149  aks6d1c6lem3  42153  bcled  42159  bcle2d  42160  aks6d1c7lem1  42161  aks6d1c7lem2  42162  aks6d1c7  42165  aks5lem6  42173  unitscyglem5  42180  aks5lem8  42182  metakunt2  42187  metakunt29  42214  sn-1ne2  42278  oexpreposd  42335  posqsqznn  42349  redvmptabs  42368  readvrec  42370  re1m1e0m0  42403  re0m0e0  42408  remul01  42413  remulneg2d  42420  sn-addlt0d  42452  sn-addgt0d  42453  renegmulnnass  42459  zmulcomlem  42461  mulgt0con1dlem  42463  sn-mulgt1d  42471  fimgmcyc  42520  dffltz  42620  3cubeslem1  42671  irrapxlem1  42809  irrapxlem2  42810  irrapxlem3  42811  irrapxlem4  42812  pellexlem6  42821  pell14qrgt0  42846  pell1qrgaplem  42860  pellfundex  42873  pellfundrp  42875  monotoddzzfi  42930  jm2.24  42951  jm2.23  42984  jm2.26lem3  42989  jm3.1lem3  43007  sqrtcvallem1  43620  reabsifneg  43621  reabsifpos  43623  sqrtcval  43630  k0004ss2  44141  imo72b2lem1  44158  dvgrat  44307  hashnzfz2  44316  binomcxplemnn0  44344  binomcxplemnotnn0  44351  neglt  45234  divlt0gt0d  45236  upbdrech2  45258  xralrple2  45303  xralrple3  45323  reclt0d  45336  reclt0  45340  xrpnf  45435  fsumnncl  45527  fsumsupp0  45533  sumnnodd  45585  lptre2pt  45595  limsupubuz  45668  liminfresre  45734  liminf0  45748  dvmptconst  45870  dvdivbd  45878  dvcosax  45881  dvbdfbdioolem1  45883  dvbdfbdioolem2  45884  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvxpaek  45895  dvnxpaek  45897  volioc  45927  volico  45938  stoweidlem1  45956  stoweidlem7  45962  stoweidlem11  45966  stoweidlem25  45980  stoweidlem26  45981  stoweidlem34  45989  stoweidlem36  45991  stoweidlem41  45996  stoweidlem42  45997  stoweidlem44  45999  stoweidlem45  46000  wallispilem3  46022  wallispilem4  46023  wallispi  46025  stirlinglem3  46031  stirlinglem5  46033  stirlinglem6  46034  stirlinglem7  46035  stirlinglem10  46038  stirlinglem11  46039  stirlinglem12  46040  dirkeritg  46057  dirkercncflem2  46059  fourierdlem9  46071  fourierdlem11  46073  fourierdlem12  46074  fourierdlem14  46076  fourierdlem15  46077  fourierdlem19  46081  fourierdlem24  46086  fourierdlem28  46090  fourierdlem30  46092  fourierdlem40  46102  fourierdlem41  46103  fourierdlem43  46105  fourierdlem44  46106  fourierdlem47  46108  fourierdlem50  46111  fourierdlem51  46112  fourierdlem57  46118  fourierdlem60  46121  fourierdlem61  46122  fourierdlem66  46127  fourierdlem68  46129  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem78  46139  fourierdlem79  46140  fourierdlem83  46144  fourierdlem88  46149  fourierdlem92  46153  fourierdlem93  46154  fourierdlem97  46158  fourierdlem103  46164  fourierdlem104  46165  fourierdlem109  46170  fourierdlem111  46172  sqwvfoura  46183  sqwvfourb  46184  fourierswlem  46185  fouriersw  46186  elaa2lem  46188  etransclem4  46193  etransclem18  46207  etransclem19  46208  etransclem23  46212  etransclem27  46216  etransclem31  46220  etransclem32  46221  etransclem35  46224  etransclem41  46230  etransclem46  46235  etransclem48  46237  rrxtopnfi  46242  qndenserrnbllem  46249  salgencntex  46298  sge0tsms  46335  sge0isum  46382  volicorecl  46501  hoiprodcl  46502  ovnlerp  46517  ovnsubaddlem1  46525  hoiprodcl3  46535  volicore  46536  hoidmvcl  46537  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  ovnhoi  46558  hoiqssbllem2  46578  volicorege0  46592  vonhoire  46627  pimrecltpos  46663  pimrecltneg  46679  smfmbfcex  46715  nsssmfmbflem  46733  smfrec  46744  smfmullem3  46748  smfdivdmmbl  46793  sharhght  46820  et-sqrtnegnre  46828  natglobalincr  46830  upwordnul  46833  zm1nn  47251  eluzge0nn0  47261  elfz2z  47264  2ffzoeq  47276  iccpartigtl  47347  iccpartgt  47351  requad01  47545  requad1  47546  requad2  47547  stgrusgra  47861  gpgedgvtx1  47954  expnegico01  48363  m1modmmod  48370  difmodm1lt  48371  regt1loggt0  48385  refdivmptf  48391  elbigolo1  48406  rege1logbrege0  48407  fllog2  48417  dignn0flhalflem1  48464  eenglngeehlnmlem2  48587  line2  48601  line2xlem  48602  line2x  48603  line2y  48604  itsclc0yqsol  48613  2itscp  48630  inlinecirc02plem  48635  amgmwlem  49032