Theorem 0red 10497

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

Syntax hints:   → wi 4   ∈ wcel 2083  ℝcr 10389  0cc0 10390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-ext 2771  ax-1cn 10448  ax-addrcl 10451  ax-rnegex 10461  ax-cnre 10463

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-cleq 2790  df-clel 2865  df-ral 3112  df-rex 3113

This theorem is referenced by:  gt0ne0  10959  add20  11006  subge0  11007  lesub0  11011  mulge0  11012  msqgt0  11014  msqge0  11015  addgt0d  11069  sublt0d  11120  prodgt0  11341  lt2msq1  11378  supmul1  11464  supmul  11467  nnne0  11525  0mnnnnn0  11783  nn0negleid  11803  rpgecl  12271  ge0p1rp  12274  ledivge1le  12314  mul2lt0rlt0  12345  mul2lt0rgt0  12346  mul2lt0bi  12349  prodge0rd  12350  max0sub  12443  reltxrnmnf  12589  infmrp1  12591  lincmb01cmp  12735  iccf1o  12736  xov1plusxeqvd  12738  elfz0fzfz0  12866  fz0fzelfz0  12867  elfzo0z  12933  fzofzim  12938  fzo1fzo0n0  12942  elfzodifsumelfzo  12957  ssfzoulel  12985  elfznelfzo  12996  muladdmodid  13133  modltm1p1mod  13145  addmodlteq  13168  expgt1  13321  ltexp2a  13384  expcan  13387  ltexp2  13388  leexp2  13389  leexp2a  13390  expnlbnd2  13449  discr  13455  fi1uzind  13705  ccatsymb  13784  ccat2s1fvw  13840  swrdnd  13856  swrdnnn0nd  13858  swrdswrdlem  13906  swrdswrd  13907  swrdccatin2  13931  pfxccatin12lem3  13934  repswswrd  13986  swrd2lsw  14154  2swrd2eqwrdeq  14155  leabs  14497  max0add  14508  absgt0  14522  rlimrege0  14774  iseraltlem2  14877  fsumrecl  14928  o1fsum  15005  cvgcmp  15008  cvgcmpce  15010  geomulcvg  15069  mertenslem2  15078  fprodle  15187  rpnnen2lem4  15407  p1modz1  15451  moddvds  15455  oddge22np1  15535  bitsfzolem  15620  bitsinv1lem  15627  sadcaddlem  15643  lcmgcdlem  15783  dvdsnprmd  15867  2mulprm  15870  isprm7  15885  qnumgt0  15923  modprm0  15975  qexpz  16070  prmreclem4  16088  4sqlem6  16112  prmgaplem7  16226  gzrngunit  20297  regsumfsum  20299  regsumsupp  20452  fvmptnn04ifd  21149  chfacffsupp  21152  chfacfscmul0  21154  chfacfscmulgsum  21156  chfacfpmmul0  21158  chfacfpmmulgsum  21160  prdsmet  22667  metustexhalf  22853  nlmvscnlem2  22981  nlmvscnlem1  22982  nmo0  23031  blcvx  23093  evth  23250  lebnumlem1  23252  lebnumii  23257  htpycc  23271  pcohtpylem  23310  pcoass  23315  pcorevlem  23317  nmoleub2lem3  23406  ipcnlem2  23534  ipcnlem1  23535  rrxcph  23682  rrxmetlem  23697  rrxmet  23698  rrxdstprj1  23699  ehlbase  23705  minveclem3b  23718  minveclem6  23724  pjthlem1  23727  ovolicopnf  23812  ioorcl2  23860  volivth  23895  mbfposr  23940  i1fmulc  23991  itg1mulc  23992  itg1ge0a  23999  mbfi1flim  24011  itg2split  24037  itg2monolem1  24038  itg2monolem3  24040  itg2mono  24041  itg2cnlem2  24050  itgge0  24098  dvlip  24277  dvlipcn  24278  dveq0  24284  dv11cn  24285  dvlt0  24289  dvfsumge  24306  dgradd2  24545  plydivlem3  24571  mtest  24679  radcnvlem1  24688  radcnv0  24691  radcnvlt1  24693  radcnvle  24695  pserulm  24697  pserdvlem1  24702  pserdv  24704  abelthlem2  24707  abelthlem7  24713  pilem2  24727  pilem3  24728  coseq00topi  24775  tanabsge  24779  tanord1  24806  tanord  24807  rplogcl  24872  logdivle  24890  logcnlem3  24912  logcnlem4  24913  dvloglem  24916  logtayl  24928  abscxp2  24961  cxplt  24962  cxple  24963  cxple2a  24967  cxpcn3lem  25013  abscxpbnd  25019  chordthmlem4  25098  chordthmlem5  25099  asinlem3  25134  atanre  25148  atanlogaddlem  25176  atanlogadd  25177  atanlogsublem  25178  atantan  25186  atans2  25194  efrlim  25233  cxp2limlem  25239  cxp2lim  25240  cxploglim2  25242  divsqrtsumlem  25243  jensenlem2  25251  harmonicubnd  25273  fsumharmonic  25275  dmlogdmgm  25287  lgamgulmlem1  25292  lgamgulmlem2  25293  ftalem1  25336  ftalem2  25337  ftalem5  25340  vmacl  25381  chtwordi  25419  ppiwordi  25425  chtrpcl  25438  fsumfldivdiaglem  25452  fsumvma2  25476  chpval2  25480  chpchtsum  25481  chpub  25482  logfacbnd3  25485  logexprlim  25487  mersenne  25489  lgsdilem  25586  lgsne0  25597  gausslemma2dlem1a  25627  lgseisen  25641  lgsquadlem1  25642  lgsquadlem2  25643  2sqmod  25698  2sqnn0  25700  chebbnd1lem2  25732  chebbnd1lem3  25733  chebbnd1  25734  chtppilimlem1  25735  chtppilimlem2  25736  chtppilim  25737  chebbnd2  25739  chto1lb  25740  chpchtlim  25741  chpo1ub  25742  dchrisumlema  25750  dchrisumlem2  25752  dchrisumlem3  25753  dchrmusumlema  25755  dchrvmasumlem2  25760  dchrvmasumiflem1  25763  dchrisum0flblem1  25770  dchrisum0flblem2  25771  dchrisum0re  25775  dchrisum0lema  25776  dchrisum0  25782  dirith2  25790  mulog2sumlem1  25796  vmalogdivsum2  25800  log2sumbnd  25806  selberg2lem  25812  chpdifbndlem1  25815  chpdifbnd  25817  selberg3lem1  25819  pntrmax  25826  pntrsumo1  25827  pntrlog2bndlem4  25842  pntrlog2bndlem5  25843  pntpbnd1a  25847  pntpbnd1  25848  pntpbnd2  25849  pntlemg  25860  pntlemj  25865  pntlemk  25868  pntlem3  25871  pnt2  25875  pnt  25876  ostth2lem1  25880  padicabv  25892  padicabvcxp  25894  ostth2lem3  25897  ostth2lem4  25898  ostth3  25900  trgcgrg  25987  tgcgr4  26003  axsegconlem7  26396  axsegconlem10  26399  axcontlem2  26438  axcontlem4  26440  axcontlem7  26443  axcontlem10  26446  crctcshwlkn0lem3  27276  crctcshwlkn0  27285  clwlkclwwlklem2a2  27457  clwlkclwwlklem2a  27462  wwlksubclwwlk  27523  frgrogt3nreg  27864  friendshipgt3  27865  minvecolem5  28345  minvecolem6  28346  htthlem  28381  pjhthlem1  28855  nndiffz1  30193  bcm1n  30200  wrdt2ind  30302  cycpmrn  30418  cyc3conja  30433  ccfldextdgrr  30657  pnfneige0  30807  nexple  30881  indf1o  30896  measinb  31093  eulerpartlems  31231  eulerpartlemgc  31233  ballotlemfc0  31363  ballotlemfcc  31364  ballotlemodife  31368  sgnneg  31411  sgnmul  31413  sgnsub  31415  signsply0  31434  signslema  31445  signsvtp  31466  signshf  31471  itgexpif  31490  breprexplemc  31516  circlemeth  31524  logdivsqrle  31534  0nn0m1nnn0  31961  cvmliftlem2  32143  dnibndlem9  33436  unbdqndv2lem2  33460  knoppndvlem1  33462  knoppndvlem2  33463  knoppndvlem7  33468  knoppndvlem11  33472  knoppndvlem14  33475  knoppndvlem15  33476  knoppndvlem17  33478  knoppndvlem19  33480  knoppndvlem20  33481  bj-pinftynminfty  34088  poimirlem10  34454  poimirlem11  34455  poimirlem24  34468  poimirlem29  34473  poimirlem31  34475  poimirlem32  34476  poimir  34477  mblfinlem2  34482  bddiblnc  34514  ftc1anclem7  34525  ftc1anclem8  34526  ftc1anc  34527  areacirclem1  34534  areacirclem4  34537  areacirc  34539  geomcau  34587  isbnd3b  34616  prdsbnd  34624  bfp  34655  rrnequiv  34666  oexpreposd  38722  nn0rppwr  38725  nn0expgcd  38727  rtprmirr  38737  dffltz  38789  irrapxlem1  38925  irrapxlem2  38926  irrapxlem3  38927  irrapxlem4  38928  pellexlem6  38937  pell14qrgt0  38962  pell1qrgaplem  38976  pellfundex  38989  pellfundrp  38991  monotoddzzfi  39045  jm2.24  39066  jm2.23  39099  jm2.26lem3  39104  jm3.1lem3  39122  k0004ss2  40008  imo72b2lem1  40028  dvgrat  40203  hashnzfz2  40212  binomcxplemnn0  40240  binomcxplemnotnn0  40247  neglt  41112  divlt0gt0d  41114  upbdrech2  41137  xralrple2  41184  xralrple3  41204  fiminre2  41208  reclt0d  41220  reclt0  41225  xrpnf  41325  fsumnncl  41415  fsumsupp0  41422  sumnnodd  41474  lptre2pt  41484  limsupubuz  41557  liminfresre  41623  liminf0  41637  dvmptconst  41762  dvdivbd  41771  dvcosax  41774  dvbdfbdioolem1  41776  dvbdfbdioolem2  41777  ioodvbdlimc1lem1  41779  ioodvbdlimc1lem2  41780  ioodvbdlimc2lem  41782  dvxpaek  41788  dvnxpaek  41790  volioc  41820  volico  41832  stoweidlem1  41850  stoweidlem7  41856  stoweidlem11  41860  stoweidlem25  41874  stoweidlem26  41875  stoweidlem34  41883  stoweidlem36  41885  stoweidlem41  41890  stoweidlem42  41891  stoweidlem44  41893  stoweidlem45  41894  wallispilem3  41916  wallispilem4  41917  wallispi  41919  stirlinglem3  41925  stirlinglem5  41927  stirlinglem6  41928  stirlinglem7  41929  stirlinglem10  41932  stirlinglem11  41933  stirlinglem12  41934  dirkeritg  41951  dirkercncflem2  41953  fourierdlem9  41965  fourierdlem11  41967  fourierdlem12  41968  fourierdlem14  41970  fourierdlem15  41971  fourierdlem19  41975  fourierdlem24  41980  fourierdlem28  41984  fourierdlem30  41986  fourierdlem40  41996  fourierdlem41  41997  fourierdlem43  41999  fourierdlem44  42000  fourierdlem47  42002  fourierdlem50  42005  fourierdlem51  42006  fourierdlem57  42012  fourierdlem60  42015  fourierdlem61  42016  fourierdlem66  42021  fourierdlem68  42023  fourierdlem73  42028  fourierdlem74  42029  fourierdlem75  42030  fourierdlem78  42033  fourierdlem79  42034  fourierdlem83  42038  fourierdlem88  42043  fourierdlem92  42047  fourierdlem93  42048  fourierdlem97  42052  fourierdlem103  42058  fourierdlem104  42059  fourierdlem109  42064  fourierdlem111  42066  sqwvfoura  42077  sqwvfourb  42078  fourierswlem  42079  fouriersw  42080  elaa2lem  42082  etransclem4  42087  etransclem18  42101  etransclem19  42102  etransclem23  42106  etransclem27  42110  etransclem31  42114  etransclem32  42115  etransclem35  42118  etransclem41  42124  etransclem46  42129  etransclem48  42131  rrxtopnfi  42136  qndenserrnbllem  42143  salgencntex  42190  sge0tsms  42226  sge0isum  42273  volicorecl  42392  hoiprodcl  42393  ovnlerp  42408  ovnsubaddlem1  42416  hoiprodcl3  42426  volicore  42427  hoidmvcl  42428  hoidmvlelem1  42441  hoidmvlelem2  42442  hoidmvlelem3  42443  ovnhoi  42449  hoiqssbllem2  42469  volicorege0  42483  vonhoire  42518  pimrecltpos  42551  pimrecltneg  42565  smfmbfcex  42600  nsssmfmbflem  42618  smfrec  42628  smfmullem3  42632  sharhght  42686  zm1nn  43040  eluzge0nn0  43050  elfz2z  43053  2ffzoeq  43066  iccpartigtl  43087  iccpartgt  43091  requad01  43290  requad1  43291  requad2  43292  expnegico01  44076  m1modmmod  44084  difmodm1lt  44085  regt1loggt0  44099  refdivmptf  44105  elbigolo1  44120  rege1logbrege0  44121  fllog2  44131  dignn0flhalflem1  44178  eenglngeehlnmlem2  44228  line2  44242  line2xlem  44243  line2x  44244  line2y  44245  itsclc0yqsol  44254  2itscp  44271  inlinecirc02plem  44276  amgmwlem  44405