Theorem 0red 10909

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 10801  0cc0 10802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-addrcl 10863  ax-rnegex 10873  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069

This theorem is referenced by:  gt0ne0  11370  add20  11417  subge0  11418  lesub0  11422  mulge0  11423  msqgt0  11425  msqge0  11426  addgt0d  11480  sublt0d  11531  prodgt0  11752  lt2msq1  11789  fiminre2  11853  supmul1  11874  supmul  11877  nnne0  11937  0mnnnnn0  12195  nn0negleid  12215  rpgecl  12687  ge0p1rp  12690  ledivge1le  12730  mul2lt0rlt0  12761  mul2lt0rgt0  12762  mul2lt0bi  12765  prodge0rd  12766  max0sub  12859  reltxrnmnf  13005  infmrp1  13007  lincmb01cmp  13156  iccf1o  13157  xov1plusxeqvd  13159  elfz0fzfz0  13290  fz0fzelfz0  13291  elfzo0z  13357  fzofzim  13362  fzo1fzo0n0  13366  elfzodifsumelfzo  13381  ssfzoulel  13409  elfznelfzo  13420  muladdmodid  13559  modltm1p1mod  13571  addmodlteq  13594  expgt1  13749  ltexp2a  13812  expcan  13815  ltexp2  13816  leexp2  13817  leexp2a  13818  expnlbnd2  13877  discr  13883  fi1uzind  14139  ccatsymb  14215  ccat2s1fvw  14277  ccat2s1fvwOLD  14278  swrdnd  14295  swrdnnn0nd  14297  swrdswrdlem  14345  swrdswrd  14346  repswswrd  14425  swrd2lsw  14593  2swrd2eqwrdeq  14594  leabs  14939  max0add  14950  absgt0  14964  rlimrege0  15216  iseraltlem2  15322  fsumrecl  15374  o1fsum  15453  cvgcmp  15456  cvgcmpce  15458  geomulcvg  15516  mertenslem2  15525  fprodle  15634  rpnnen2lem4  15854  p1modz1  15898  moddvds  15902  oddge22np1  15986  bitsfzolem  16069  bitsinv1lem  16076  sadcaddlem  16092  lcmgcdlem  16239  dvdsnprmd  16323  2mulprm  16326  isprm7  16341  qnumgt0  16382  modprm0  16434  qexpz  16530  prmreclem4  16548  4sqlem6  16572  prmgaplem7  16686  gzrngunit  20576  regsumfsum  20578  regsumsupp  20739  fvmptnn04ifd  21910  chfacffsupp  21913  chfacfscmul0  21915  chfacfscmulgsum  21917  chfacfpmmul0  21919  chfacfpmmulgsum  21921  prdsmet  23431  metustexhalf  23618  nlmvscnlem2  23755  nlmvscnlem1  23756  nmo0  23805  blcvx  23867  evth  24028  lebnumlem1  24030  lebnumii  24035  htpycc  24049  pcohtpylem  24088  pcoass  24093  pcorevlem  24095  nmoleub2lem3  24184  ipcnlem2  24313  ipcnlem1  24314  rrxcph  24461  rrxmetlem  24476  rrxmet  24477  rrxdstprj1  24478  ehlbase  24484  minveclem3b  24497  minveclem6  24503  pjthlem1  24506  ovolicopnf  24593  ioorcl2  24641  volivth  24676  mbfposr  24721  i1fmulc  24773  itg1mulc  24774  itg1ge0a  24781  mbfi1flim  24793  itg2split  24819  itg2monolem1  24820  itg2monolem3  24822  itg2mono  24823  itg2cnlem2  24832  itgge0  24880  bddiblnc  24911  dvlip  25062  dvlipcn  25063  dveq0  25069  dv11cn  25070  dvlt0  25074  dvfsumge  25091  dgradd2  25334  plydivlem3  25360  mtest  25468  radcnvlem1  25477  radcnv0  25480  radcnvlt1  25482  radcnvle  25484  pserulm  25486  pserdvlem1  25491  pserdv  25493  abelthlem2  25496  abelthlem7  25502  pilem2  25516  pilem3  25517  coseq00topi  25564  tanabsge  25568  cosq34lt1  25588  tanord1  25598  tanord  25599  rplogcl  25664  logdivle  25682  logcnlem3  25704  logcnlem4  25705  dvloglem  25708  logtayl  25720  abscxp2  25753  cxplt  25754  cxple  25755  cxple2a  25759  cxpcn3lem  25805  abscxpbnd  25811  chordthmlem4  25890  chordthmlem5  25891  asinlem3  25926  atanre  25940  atanlogaddlem  25968  atanlogadd  25969  atanlogsublem  25970  atantan  25978  atans2  25986  efrlim  26024  cxp2limlem  26030  cxp2lim  26031  cxploglim2  26033  divsqrtsumlem  26034  jensenlem2  26042  harmonicubnd  26064  fsumharmonic  26066  dmlogdmgm  26078  lgamgulmlem1  26083  lgamgulmlem2  26084  ftalem1  26127  ftalem2  26128  ftalem5  26131  vmacl  26172  chtwordi  26210  ppiwordi  26216  chtrpcl  26229  fsumfldivdiaglem  26243  fsumvma2  26267  chpval2  26271  chpchtsum  26272  chpub  26273  logfacbnd3  26276  logexprlim  26278  mersenne  26280  lgsdilem  26377  lgsne0  26388  gausslemma2dlem1a  26418  lgseisen  26432  lgsquadlem1  26433  lgsquadlem2  26434  2sqmod  26489  2sqnn0  26491  chebbnd1lem2  26523  chebbnd1lem3  26524  chebbnd1  26525  chtppilimlem1  26526  chtppilimlem2  26527  chtppilim  26528  chebbnd2  26530  chto1lb  26531  chpchtlim  26532  chpo1ub  26533  dchrisumlema  26541  dchrisumlem2  26543  dchrisumlem3  26544  dchrmusumlema  26546  dchrvmasumlem2  26551  dchrvmasumiflem1  26554  dchrisum0flblem1  26561  dchrisum0flblem2  26562  dchrisum0re  26566  dchrisum0lema  26567  dchrisum0  26573  dirith2  26581  mulog2sumlem1  26587  vmalogdivsum2  26591  log2sumbnd  26597  selberg2lem  26603  chpdifbndlem1  26606  chpdifbnd  26608  selberg3lem1  26610  pntrmax  26617  pntrsumo1  26618  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntpbnd1a  26638  pntpbnd1  26639  pntpbnd2  26640  pntlemg  26651  pntlemj  26656  pntlemk  26659  pntlem3  26662  pnt2  26666  pnt  26667  ostth2lem1  26671  padicabv  26683  padicabvcxp  26685  ostth2lem3  26688  ostth2lem4  26689  ostth3  26691  trgcgrg  26780  tgcgr4  26796  axsegconlem7  27194  axsegconlem10  27197  axcontlem2  27236  axcontlem4  27238  axcontlem7  27241  axcontlem10  27244  crctcshwlkn0lem3  28078  crctcshwlkn0  28087  clwlkclwwlklem2a2  28258  clwlkclwwlklem2a  28263  wwlksubclwwlk  28323  frgrogt3nreg  28662  friendshipgt3  28663  minvecolem5  29144  minvecolem6  29145  htthlem  29180  pjhthlem1  29654  nndiffz1  31009  bcm1n  31018  wrdt2ind  31127  cycpmrn  31312  cyc3conja  31326  ccfldextdgrr  31644  pnfneige0  31803  nexple  31877  indf1o  31892  measinb  32089  eulerpartlems  32227  eulerpartlemgc  32229  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemodife  32364  sgnneg  32407  sgnmul  32409  sgnsub  32411  signsply0  32430  signslema  32441  signsvtp  32462  itgexpif  32486  breprexplemc  32512  circlemeth  32520  logdivsqrle  32530  0nn0m1nnn0  32971  cvmliftlem2  33148  dnibndlem9  34593  unbdqndv2lem2  34617  knoppndvlem1  34619  knoppndvlem2  34620  knoppndvlem7  34625  knoppndvlem11  34629  knoppndvlem14  34632  knoppndvlem15  34633  knoppndvlem17  34635  knoppndvlem19  34637  knoppndvlem20  34638  bj-pinftynminfty  35325  poimirlem10  35714  poimirlem11  35715  poimirlem24  35728  poimirlem29  35733  poimirlem31  35735  poimirlem32  35736  poimir  35737  mblfinlem2  35742  ftc1anclem7  35783  ftc1anclem8  35784  ftc1anc  35785  areacirclem1  35792  areacirclem4  35795  areacirc  35797  geomcau  35844  isbnd3b  35870  prdsbnd  35878  bfp  35909  rrnequiv  35920  resdvopclptsd  39964  lcmineqlem2  39966  lcmineqlem3  39967  lcmineqlem10  39974  lcmineqlem12  39976  lcmineqlem23  39987  3lexlogpow5ineq1  39990  3lexlogpow5ineq2  39991  3lexlogpow5ineq4  39992  3lexlogpow5ineq3  39993  3lexlogpow2ineq2  39995  3lexlogpow5ineq5  39996  aks4d1lem1  39998  dvrelog2  40000  dvrelog3  40001  dvrelog2b  40002  0nonelalab  40003  dvrelogpow2b  40004  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1p6  40009  aks4d1p1p7  40010  aks4d1p1p5  40011  aks4d1p1  40012  aks4d1p2  40013  aks4d1p3  40014  aks4d1p5  40016  aks4d1p6  40017  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8d2  40021  aks4d1p8d3  40022  aks4d1p8  40023  aks4d1p9  40024  2np3bcnp1  40028  2ap1caineq  40029  sticksstones7  40036  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  sticksstones22  40052  metakunt2  40054  metakunt29  40081  sn-1ne2  40216  oexpreposd  40242  nn0rppwr  40254  nn0expgcd  40256  posqsqznn  40264  rtprmirr  40268  re1m1e0m0  40301  re0m0e0  40306  remul01  40311  mulgt0con1dlem  40348  mulgt0b2d  40351  dffltz  40387  3cubeslem1  40422  irrapxlem1  40560  irrapxlem2  40561  irrapxlem3  40562  irrapxlem4  40563  pellexlem6  40572  pell14qrgt0  40597  pell1qrgaplem  40611  pellfundex  40624  pellfundrp  40626  monotoddzzfi  40680  jm2.24  40701  jm2.23  40734  jm2.26lem3  40739  jm3.1lem3  40757  sqrtcvallem1  41128  reabsifneg  41129  reabsifpos  41131  sqrtcval  41138  k0004ss2  41651  imo72b2lem1  41669  dvgrat  41819  hashnzfz2  41828  binomcxplemnn0  41856  binomcxplemnotnn0  41863  neglt  42712  divlt0gt0d  42714  upbdrech2  42737  xralrple2  42783  xralrple3  42803  reclt0d  42816  reclt0  42821  xrpnf  42916  fsumnncl  43003  fsumsupp0  43009  sumnnodd  43061  lptre2pt  43071  limsupubuz  43144  liminfresre  43210  liminf0  43224  dvmptconst  43346  dvdivbd  43354  dvcosax  43357  dvbdfbdioolem1  43359  dvbdfbdioolem2  43360  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvxpaek  43371  dvnxpaek  43373  volioc  43403  volico  43414  stoweidlem1  43432  stoweidlem7  43438  stoweidlem11  43442  stoweidlem25  43456  stoweidlem26  43457  stoweidlem34  43465  stoweidlem36  43467  stoweidlem41  43472  stoweidlem42  43473  stoweidlem44  43475  stoweidlem45  43476  wallispilem3  43498  wallispilem4  43499  wallispi  43501  stirlinglem3  43507  stirlinglem5  43509  stirlinglem6  43510  stirlinglem7  43511  stirlinglem10  43514  stirlinglem11  43515  stirlinglem12  43516  dirkeritg  43533  dirkercncflem2  43535  fourierdlem9  43547  fourierdlem11  43549  fourierdlem12  43550  fourierdlem14  43552  fourierdlem15  43553  fourierdlem19  43557  fourierdlem24  43562  fourierdlem28  43566  fourierdlem30  43568  fourierdlem40  43578  fourierdlem41  43579  fourierdlem43  43581  fourierdlem44  43582  fourierdlem47  43584  fourierdlem50  43587  fourierdlem51  43588  fourierdlem57  43594  fourierdlem60  43597  fourierdlem61  43598  fourierdlem66  43603  fourierdlem68  43605  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem78  43615  fourierdlem79  43616  fourierdlem83  43620  fourierdlem88  43625  fourierdlem92  43629  fourierdlem93  43630  fourierdlem97  43634  fourierdlem103  43640  fourierdlem104  43641  fourierdlem109  43646  fourierdlem111  43648  sqwvfoura  43659  sqwvfourb  43660  fourierswlem  43661  fouriersw  43662  elaa2lem  43664  etransclem4  43669  etransclem18  43683  etransclem19  43684  etransclem23  43688  etransclem27  43692  etransclem31  43696  etransclem32  43697  etransclem35  43700  etransclem41  43706  etransclem46  43711  etransclem48  43713  rrxtopnfi  43718  qndenserrnbllem  43725  salgencntex  43772  sge0tsms  43808  sge0isum  43855  volicorecl  43974  hoiprodcl  43975  ovnlerp  43990  ovnsubaddlem1  43998  hoiprodcl3  44008  volicore  44009  hoidmvcl  44010  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  ovnhoi  44031  hoiqssbllem2  44051  volicorege0  44065  vonhoire  44100  pimrecltpos  44133  pimrecltneg  44147  smfmbfcex  44182  nsssmfmbflem  44200  smfrec  44210  smfmullem3  44214  sharhght  44268  zm1nn  44682  eluzge0nn0  44692  elfz2z  44695  2ffzoeq  44708  iccpartigtl  44763  iccpartgt  44767  requad01  44961  requad1  44962  requad2  44963  expnegico01  45747  m1modmmod  45755  difmodm1lt  45756  regt1loggt0  45770  refdivmptf  45776  elbigolo1  45791  rege1logbrege0  45792  fllog2  45802  dignn0flhalflem1  45849  eenglngeehlnmlem2  45972  line2  45986  line2xlem  45987  line2x  45988  line2y  45989  itsclc0yqsol  45998  2itscp  46015  inlinecirc02plem  46020  amgmwlem  46392