Theorem 0red 11217

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11109  0cc0 11110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168  ax-addrcl 11171  ax-rnegex 11181  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-clel 2811  df-rex 3072

This theorem is referenced by:  gt0ne0  11679  add20  11726  subge0  11727  lesub0  11731  mulge0  11732  msqgt0  11734  msqge0  11735  addgt0d  11789  sublt0d  11840  prodgt0  12061  lt2msq1  12098  fiminre2  12162  supmul1  12183  supmul  12186  nnne0  12246  0mnnnnn0  12504  nn0negleid  12524  rpgecl  13002  ge0p1rp  13005  ledivge1le  13045  mul2lt0rlt0  13076  mul2lt0rgt0  13077  mul2lt0bi  13080  prodge0rd  13081  max0sub  13175  reltxrnmnf  13321  infmrp1  13323  lincmb01cmp  13472  iccf1o  13473  xov1plusxeqvd  13475  elfz0fzfz0  13606  fz0fzelfz0  13607  elfzo0z  13674  fzofzim  13679  fzo1fzo0n0  13683  elfzodifsumelfzo  13698  ssfzoulel  13726  elfznelfzo  13737  muladdmodid  13876  modltm1p1mod  13888  addmodlteq  13911  expgt1  14066  ltexp2a  14131  expcan  14134  ltexp2  14135  leexp2  14136  leexp2a  14137  zzlesq  14170  expnlbnd2  14197  discr  14203  fi1uzind  14458  ccatsymb  14532  ccat2s1fvw  14588  swrdnd  14604  swrdnnn0nd  14606  swrdswrdlem  14654  swrdswrd  14655  repswswrd  14734  swrd2lsw  14903  2swrd2eqwrdeq  14904  leabs  15246  max0add  15257  absgt0  15271  rlimrege0  15523  iseraltlem2  15629  fsumrecl  15680  o1fsum  15759  cvgcmp  15762  cvgcmpce  15764  geomulcvg  15822  mertenslem2  15831  fprodle  15940  rpnnen2lem4  16160  p1modz1  16204  moddvds  16208  oddge22np1  16292  bitsfzolem  16375  bitsinv1lem  16382  sadcaddlem  16398  lcmgcdlem  16543  dvdsnprmd  16627  2mulprm  16630  isprm7  16645  qnumgt0  16686  modprm0  16738  qexpz  16834  prmreclem4  16852  4sqlem6  16876  prmgaplem7  16990  gzrngunit  21011  regsumfsum  21013  regsumsupp  21175  fvmptnn04ifd  22355  chfacffsupp  22358  chfacfscmul0  22360  chfacfscmulgsum  22362  chfacfpmmul0  22364  chfacfpmmulgsum  22366  prdsmet  23876  metustexhalf  24065  nlmvscnlem2  24202  nlmvscnlem1  24203  nmo0  24252  blcvx  24314  evth  24475  lebnumlem1  24477  lebnumii  24482  htpycc  24496  pcohtpylem  24535  pcoass  24540  pcorevlem  24542  nmoleub2lem3  24631  ipcnlem2  24761  ipcnlem1  24762  rrxcph  24909  rrxmetlem  24924  rrxmet  24925  rrxdstprj1  24926  ehlbase  24932  minveclem3b  24945  minveclem6  24951  pjthlem1  24954  ovolicopnf  25041  ioorcl2  25089  volivth  25124  mbfposr  25169  i1fmulc  25221  itg1mulc  25222  itg1ge0a  25229  mbfi1flim  25241  itg2split  25267  itg2monolem1  25268  itg2monolem3  25270  itg2mono  25271  itg2cnlem2  25280  itgge0  25328  bddiblnc  25359  dvlip  25510  dvlipcn  25511  dveq0  25517  dv11cn  25518  dvlt0  25522  dvfsumge  25539  dgradd2  25782  plydivlem3  25808  mtest  25916  radcnvlem1  25925  radcnv0  25928  radcnvlt1  25930  radcnvle  25932  pserulm  25934  pserdvlem1  25939  pserdv  25941  abelthlem2  25944  abelthlem7  25950  pilem2  25964  pilem3  25965  coseq00topi  26012  tanabsge  26016  cosq34lt1  26036  tanord1  26046  tanord  26047  rplogcl  26112  logdivle  26130  logcnlem3  26152  logcnlem4  26153  dvloglem  26156  logtayl  26168  abscxp2  26201  cxplt  26202  cxple  26203  cxple2a  26207  cxpcn3lem  26255  abscxpbnd  26261  chordthmlem4  26340  chordthmlem5  26341  asinlem3  26376  atanre  26390  atanlogaddlem  26418  atanlogadd  26419  atanlogsublem  26420  atantan  26428  atans2  26436  efrlim  26474  cxp2limlem  26480  cxp2lim  26481  cxploglim2  26483  divsqrtsumlem  26484  jensenlem2  26492  harmonicubnd  26514  fsumharmonic  26516  dmlogdmgm  26528  lgamgulmlem1  26533  lgamgulmlem2  26534  ftalem1  26577  ftalem2  26578  ftalem5  26581  vmacl  26622  chtwordi  26660  ppiwordi  26666  chtrpcl  26679  fsumfldivdiaglem  26693  fsumvma2  26717  chpval2  26721  chpchtsum  26722  chpub  26723  logfacbnd3  26726  logexprlim  26728  mersenne  26730  lgsdilem  26827  lgsne0  26838  gausslemma2dlem1a  26868  lgseisen  26882  lgsquadlem1  26883  lgsquadlem2  26884  2sqmod  26939  2sqnn0  26941  chebbnd1lem2  26973  chebbnd1lem3  26974  chebbnd1  26975  chtppilimlem1  26976  chtppilimlem2  26977  chtppilim  26978  chebbnd2  26980  chto1lb  26981  chpchtlim  26982  chpo1ub  26983  dchrisumlema  26991  dchrisumlem2  26993  dchrisumlem3  26994  dchrmusumlema  26996  dchrvmasumlem2  27001  dchrvmasumiflem1  27004  dchrisum0flblem1  27011  dchrisum0flblem2  27012  dchrisum0re  27016  dchrisum0lema  27017  dchrisum0  27023  dirith2  27031  mulog2sumlem1  27037  vmalogdivsum2  27041  log2sumbnd  27047  selberg2lem  27053  chpdifbndlem1  27056  chpdifbnd  27058  selberg3lem1  27060  pntrmax  27067  pntrsumo1  27068  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntpbnd1a  27088  pntpbnd1  27089  pntpbnd2  27090  pntlemg  27101  pntlemj  27106  pntlemk  27109  pntlem3  27112  pnt2  27116  pnt  27117  ostth2lem1  27121  padicabv  27133  padicabvcxp  27135  ostth2lem3  27138  ostth2lem4  27139  ostth3  27141  trgcgrg  27766  tgcgr4  27782  axsegconlem7  28181  axsegconlem10  28184  axcontlem2  28223  axcontlem4  28225  axcontlem7  28228  axcontlem10  28231  crctcshwlkn0lem3  29066  crctcshwlkn0  29075  clwlkclwwlklem2a2  29246  clwlkclwwlklem2a  29251  wwlksubclwwlk  29311  frgrogt3nreg  29650  friendshipgt3  29651  minvecolem5  30134  minvecolem6  30135  htthlem  30170  pjhthlem1  30644  nndiffz1  31997  bcm1n  32006  wrdt2ind  32117  cycpmrn  32302  cyc3conja  32316  ccfldextdgrr  32746  pnfneige0  32931  nexple  33007  indf1o  33022  measinb  33219  eulerpartlems  33359  eulerpartlemgc  33361  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemodife  33496  sgnneg  33539  sgnmul  33541  sgnsub  33543  signsply0  33562  signslema  33573  signsvtp  33594  itgexpif  33618  breprexplemc  33644  circlemeth  33652  logdivsqrle  33662  0nn0m1nnn0  34102  cvmliftlem2  34277  dnibndlem9  35362  unbdqndv2lem2  35386  knoppndvlem1  35388  knoppndvlem2  35389  knoppndvlem7  35394  knoppndvlem11  35398  knoppndvlem14  35401  knoppndvlem15  35402  knoppndvlem17  35404  knoppndvlem19  35406  knoppndvlem20  35407  bj-pinftynminfty  36108  poimirlem10  36498  poimirlem11  36499  poimirlem24  36512  poimirlem29  36517  poimirlem31  36519  poimirlem32  36520  poimir  36521  mblfinlem2  36526  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  areacirclem1  36576  areacirclem4  36579  areacirc  36581  geomcau  36627  isbnd3b  36653  prdsbnd  36661  bfp  36692  rrnequiv  36703  resdvopclptsd  40893  lcmineqlem2  40895  lcmineqlem3  40896  lcmineqlem10  40903  lcmineqlem12  40905  lcmineqlem23  40916  3lexlogpow5ineq1  40919  3lexlogpow5ineq2  40920  3lexlogpow5ineq4  40921  3lexlogpow5ineq3  40922  3lexlogpow2ineq2  40924  3lexlogpow5ineq5  40925  aks4d1lem1  40927  dvrelog2  40929  dvrelog3  40930  dvrelog2b  40931  0nonelalab  40932  dvrelogpow2b  40933  aks4d1p1p3  40934  aks4d1p1p2  40935  aks4d1p1p4  40936  aks4d1p1p6  40938  aks4d1p1p7  40939  aks4d1p1p5  40940  aks4d1p1  40941  aks4d1p2  40942  aks4d1p3  40943  aks4d1p5  40945  aks4d1p6  40946  aks4d1p7d1  40947  aks4d1p7  40948  aks4d1p8d2  40950  aks4d1p8d3  40951  aks4d1p8  40952  aks4d1p9  40953  2np3bcnp1  40960  2ap1caineq  40961  sticksstones7  40968  sticksstones10  40971  sticksstones12a  40973  sticksstones12  40974  sticksstones22  40984  metakunt2  40986  metakunt29  41013  sn-1ne2  41179  oexpreposd  41212  nn0rppwr  41224  nn0expgcd  41226  posqsqznn  41234  rtprmirr  41237  re1m1e0m0  41270  re0m0e0  41275  remul01  41280  remulneg2d  41287  sn-addlt0d  41319  sn-addgt0d  41320  renegmulnnass  41326  zmulcomlem  41328  mulgt0con1dlem  41330  dffltz  41376  3cubeslem1  41422  irrapxlem1  41560  irrapxlem2  41561  irrapxlem3  41562  irrapxlem4  41563  pellexlem6  41572  pell14qrgt0  41597  pell1qrgaplem  41611  pellfundex  41624  pellfundrp  41626  monotoddzzfi  41681  jm2.24  41702  jm2.23  41735  jm2.26lem3  41740  jm3.1lem3  41758  sqrtcvallem1  42382  reabsifneg  42383  reabsifpos  42385  sqrtcval  42392  k0004ss2  42903  imo72b2lem1  42921  dvgrat  43071  hashnzfz2  43080  binomcxplemnn0  43108  binomcxplemnotnn0  43115  neglt  43994  divlt0gt0d  43996  upbdrech2  44018  xralrple2  44064  xralrple3  44084  reclt0d  44097  reclt0  44101  xrpnf  44196  fsumnncl  44288  fsumsupp0  44294  sumnnodd  44346  lptre2pt  44356  limsupubuz  44429  liminfresre  44495  liminf0  44509  dvmptconst  44631  dvdivbd  44639  dvcosax  44642  dvbdfbdioolem1  44644  dvbdfbdioolem2  44645  ioodvbdlimc1lem1  44647  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvxpaek  44656  dvnxpaek  44658  volioc  44688  volico  44699  stoweidlem1  44717  stoweidlem7  44723  stoweidlem11  44727  stoweidlem25  44741  stoweidlem26  44742  stoweidlem34  44750  stoweidlem36  44752  stoweidlem41  44757  stoweidlem42  44758  stoweidlem44  44760  stoweidlem45  44761  wallispilem3  44783  wallispilem4  44784  wallispi  44786  stirlinglem3  44792  stirlinglem5  44794  stirlinglem6  44795  stirlinglem7  44796  stirlinglem10  44799  stirlinglem11  44800  stirlinglem12  44801  dirkeritg  44818  dirkercncflem2  44820  fourierdlem9  44832  fourierdlem11  44834  fourierdlem12  44835  fourierdlem14  44837  fourierdlem15  44838  fourierdlem19  44842  fourierdlem24  44847  fourierdlem28  44851  fourierdlem30  44853  fourierdlem40  44863  fourierdlem41  44864  fourierdlem43  44866  fourierdlem44  44867  fourierdlem47  44869  fourierdlem50  44872  fourierdlem51  44873  fourierdlem57  44879  fourierdlem60  44882  fourierdlem61  44883  fourierdlem66  44888  fourierdlem68  44890  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem78  44900  fourierdlem79  44901  fourierdlem83  44905  fourierdlem88  44910  fourierdlem92  44914  fourierdlem93  44915  fourierdlem97  44919  fourierdlem103  44925  fourierdlem104  44926  fourierdlem109  44931  fourierdlem111  44933  sqwvfoura  44944  sqwvfourb  44945  fourierswlem  44946  fouriersw  44947  elaa2lem  44949  etransclem4  44954  etransclem18  44968  etransclem19  44969  etransclem23  44973  etransclem27  44977  etransclem31  44981  etransclem32  44982  etransclem35  44985  etransclem41  44991  etransclem46  44996  etransclem48  44998  rrxtopnfi  45003  qndenserrnbllem  45010  salgencntex  45059  sge0tsms  45096  sge0isum  45143  volicorecl  45262  hoiprodcl  45263  ovnlerp  45278  ovnsubaddlem1  45286  hoiprodcl3  45296  volicore  45297  hoidmvcl  45298  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem3  45313  ovnhoi  45319  hoiqssbllem2  45339  volicorege0  45353  vonhoire  45388  pimrecltpos  45424  pimrecltneg  45440  smfmbfcex  45476  nsssmfmbflem  45494  smfrec  45505  smfmullem3  45509  smfdivdmmbl  45554  sharhght  45581  et-sqrtnegnre  45589  natglobalincr  45591  upwordnul  45594  zm1nn  46010  eluzge0nn0  46020  elfz2z  46023  2ffzoeq  46036  iccpartigtl  46091  iccpartgt  46095  requad01  46289  requad1  46290  requad2  46291  expnegico01  47199  m1modmmod  47207  difmodm1lt  47208  regt1loggt0  47222  refdivmptf  47228  elbigolo1  47243  rege1logbrege0  47244  fllog2  47254  dignn0flhalflem1  47301  eenglngeehlnmlem2  47424  line2  47438  line2xlem  47439  line2x  47440  line2y  47441  itsclc0yqsol  47450  2itscp  47467  inlinecirc02plem  47472  amgmwlem  47849