Theorem 0red 10644

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 10536  0cc0 10537

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2793  ax-1cn 10595  ax-addrcl 10598  ax-rnegex 10608  ax-cnre 10610

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-clel 2893  df-ral 3143  df-rex 3144

This theorem is referenced by:  gt0ne0  11105  add20  11152  subge0  11153  lesub0  11157  mulge0  11158  msqgt0  11160  msqge0  11161  addgt0d  11215  sublt0d  11266  prodgt0  11487  lt2msq1  11524  supmul1  11610  supmul  11613  nnne0  11672  0mnnnnn0  11930  nn0negleid  11950  rpgecl  12418  ge0p1rp  12421  ledivge1le  12461  mul2lt0rlt0  12492  mul2lt0rgt0  12493  mul2lt0bi  12496  prodge0rd  12497  max0sub  12590  reltxrnmnf  12736  infmrp1  12738  lincmb01cmp  12882  iccf1o  12883  xov1plusxeqvd  12885  elfz0fzfz0  13013  fz0fzelfz0  13014  elfzo0z  13080  fzofzim  13085  fzo1fzo0n0  13089  elfzodifsumelfzo  13104  ssfzoulel  13132  elfznelfzo  13143  muladdmodid  13280  modltm1p1mod  13292  addmodlteq  13315  expgt1  13468  ltexp2a  13531  expcan  13534  ltexp2  13535  leexp2  13536  leexp2a  13537  expnlbnd2  13596  discr  13602  fi1uzind  13856  ccatsymb  13936  ccat2s1fvw  13998  ccat2s1fvwOLD  13999  swrdnd  14016  swrdnnn0nd  14018  swrdswrdlem  14066  swrdswrd  14067  repswswrd  14146  swrd2lsw  14314  2swrd2eqwrdeq  14315  leabs  14659  max0add  14670  absgt0  14684  rlimrege0  14936  iseraltlem2  15039  fsumrecl  15091  o1fsum  15168  cvgcmp  15171  cvgcmpce  15173  geomulcvg  15232  mertenslem2  15241  fprodle  15350  rpnnen2lem4  15570  p1modz1  15614  moddvds  15618  oddge22np1  15698  bitsfzolem  15783  bitsinv1lem  15790  sadcaddlem  15806  lcmgcdlem  15950  dvdsnprmd  16034  2mulprm  16037  isprm7  16052  qnumgt0  16090  modprm0  16142  qexpz  16237  prmreclem4  16255  4sqlem6  16279  prmgaplem7  16393  gzrngunit  20611  regsumfsum  20613  regsumsupp  20766  fvmptnn04ifd  21461  chfacffsupp  21464  chfacfscmul0  21466  chfacfscmulgsum  21468  chfacfpmmul0  21470  chfacfpmmulgsum  21472  prdsmet  22980  metustexhalf  23166  nlmvscnlem2  23294  nlmvscnlem1  23295  nmo0  23344  blcvx  23406  evth  23563  lebnumlem1  23565  lebnumii  23570  htpycc  23584  pcohtpylem  23623  pcoass  23628  pcorevlem  23630  nmoleub2lem3  23719  ipcnlem2  23847  ipcnlem1  23848  rrxcph  23995  rrxmetlem  24010  rrxmet  24011  rrxdstprj1  24012  ehlbase  24018  minveclem3b  24031  minveclem6  24037  pjthlem1  24040  ovolicopnf  24125  ioorcl2  24173  volivth  24208  mbfposr  24253  i1fmulc  24304  itg1mulc  24305  itg1ge0a  24312  mbfi1flim  24324  itg2split  24350  itg2monolem1  24351  itg2monolem3  24353  itg2mono  24354  itg2cnlem2  24363  itgge0  24411  dvlip  24590  dvlipcn  24591  dveq0  24597  dv11cn  24598  dvlt0  24602  dvfsumge  24619  dgradd2  24858  plydivlem3  24884  mtest  24992  radcnvlem1  25001  radcnv0  25004  radcnvlt1  25006  radcnvle  25008  pserulm  25010  pserdvlem1  25015  pserdv  25017  abelthlem2  25020  abelthlem7  25026  pilem2  25040  pilem3  25041  coseq00topi  25088  tanabsge  25092  cosq34lt1  25112  tanord1  25121  tanord  25122  rplogcl  25187  logdivle  25205  logcnlem3  25227  logcnlem4  25228  dvloglem  25231  logtayl  25243  abscxp2  25276  cxplt  25277  cxple  25278  cxple2a  25282  cxpcn3lem  25328  abscxpbnd  25334  chordthmlem4  25413  chordthmlem5  25414  asinlem3  25449  atanre  25463  atanlogaddlem  25491  atanlogadd  25492  atanlogsublem  25493  atantan  25501  atans2  25509  efrlim  25547  cxp2limlem  25553  cxp2lim  25554  cxploglim2  25556  divsqrtsumlem  25557  jensenlem2  25565  harmonicubnd  25587  fsumharmonic  25589  dmlogdmgm  25601  lgamgulmlem1  25606  lgamgulmlem2  25607  ftalem1  25650  ftalem2  25651  ftalem5  25654  vmacl  25695  chtwordi  25733  ppiwordi  25739  chtrpcl  25752  fsumfldivdiaglem  25766  fsumvma2  25790  chpval2  25794  chpchtsum  25795  chpub  25796  logfacbnd3  25799  logexprlim  25801  mersenne  25803  lgsdilem  25900  lgsne0  25911  gausslemma2dlem1a  25941  lgseisen  25955  lgsquadlem1  25956  lgsquadlem2  25957  2sqmod  26012  2sqnn0  26014  chebbnd1lem2  26046  chebbnd1lem3  26047  chebbnd1  26048  chtppilimlem1  26049  chtppilimlem2  26050  chtppilim  26051  chebbnd2  26053  chto1lb  26054  chpchtlim  26055  chpo1ub  26056  dchrisumlema  26064  dchrisumlem2  26066  dchrisumlem3  26067  dchrmusumlema  26069  dchrvmasumlem2  26074  dchrvmasumiflem1  26077  dchrisum0flblem1  26084  dchrisum0flblem2  26085  dchrisum0re  26089  dchrisum0lema  26090  dchrisum0  26096  dirith2  26104  mulog2sumlem1  26110  vmalogdivsum2  26114  log2sumbnd  26120  selberg2lem  26126  chpdifbndlem1  26129  chpdifbnd  26131  selberg3lem1  26133  pntrmax  26140  pntrsumo1  26141  pntrlog2bndlem4  26156  pntrlog2bndlem5  26157  pntpbnd1a  26161  pntpbnd1  26162  pntpbnd2  26163  pntlemg  26174  pntlemj  26179  pntlemk  26182  pntlem3  26185  pnt2  26189  pnt  26190  ostth2lem1  26194  padicabv  26206  padicabvcxp  26208  ostth2lem3  26211  ostth2lem4  26212  ostth3  26214  trgcgrg  26301  tgcgr4  26317  axsegconlem7  26709  axsegconlem10  26712  axcontlem2  26751  axcontlem4  26753  axcontlem7  26756  axcontlem10  26759  crctcshwlkn0lem3  27590  crctcshwlkn0  27599  clwlkclwwlklem2a2  27771  clwlkclwwlklem2a  27776  wwlksubclwwlk  27837  frgrogt3nreg  28176  friendshipgt3  28177  minvecolem5  28658  minvecolem6  28659  htthlem  28694  pjhthlem1  29168  nndiffz1  30509  bcm1n  30518  wrdt2ind  30627  cycpmrn  30785  cyc3conja  30799  ccfldextdgrr  31057  pnfneige0  31194  nexple  31268  indf1o  31283  measinb  31480  eulerpartlems  31618  eulerpartlemgc  31620  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemodife  31755  sgnneg  31798  sgnmul  31800  sgnsub  31802  signsply0  31821  signslema  31832  signsvtp  31853  itgexpif  31877  breprexplemc  31903  circlemeth  31911  logdivsqrle  31921  0nn0m1nnn0  32351  cvmliftlem2  32533  dnibndlem9  33825  unbdqndv2lem2  33849  knoppndvlem1  33851  knoppndvlem2  33852  knoppndvlem7  33857  knoppndvlem11  33861  knoppndvlem14  33864  knoppndvlem15  33865  knoppndvlem17  33867  knoppndvlem19  33869  knoppndvlem20  33870  bj-pinftynminfty  34512  poimirlem10  34917  poimirlem11  34918  poimirlem24  34931  poimirlem29  34936  poimirlem31  34938  poimirlem32  34939  poimir  34940  mblfinlem2  34945  bddiblnc  34977  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  areacirclem1  34997  areacirclem4  35000  areacirc  35002  geomcau  35049  isbnd3b  35078  prdsbnd  35086  bfp  35117  rrnequiv  35128  sn-1ne2  39178  oexpreposd  39199  nn0rppwr  39202  nn0expgcd  39204  rtprmirr  39214  re1m1e0m0  39247  re0m0e0  39252  remul01  39257  dffltz  39291  3cubeslem1  39301  irrapxlem1  39439  irrapxlem2  39440  irrapxlem3  39441  irrapxlem4  39442  pellexlem6  39451  pell14qrgt0  39476  pell1qrgaplem  39490  pellfundex  39503  pellfundrp  39505  monotoddzzfi  39559  jm2.24  39580  jm2.23  39613  jm2.26lem3  39618  jm3.1lem3  39636  k0004ss2  40522  imo72b2lem1  40541  dvgrat  40664  hashnzfz2  40673  binomcxplemnn0  40701  binomcxplemnotnn0  40708  neglt  41570  divlt0gt0d  41572  upbdrech2  41595  xralrple2  41642  xralrple3  41662  fiminre2  41666  reclt0d  41678  reclt0  41683  xrpnf  41782  fsumnncl  41872  fsumsupp0  41879  sumnnodd  41931  lptre2pt  41941  limsupubuz  42014  liminfresre  42080  liminf0  42094  dvmptconst  42219  dvdivbd  42228  dvcosax  42231  dvbdfbdioolem1  42233  dvbdfbdioolem2  42234  ioodvbdlimc1lem1  42236  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  dvxpaek  42245  dvnxpaek  42247  volioc  42277  volico  42288  stoweidlem1  42306  stoweidlem7  42312  stoweidlem11  42316  stoweidlem25  42330  stoweidlem26  42331  stoweidlem34  42339  stoweidlem36  42341  stoweidlem41  42346  stoweidlem42  42347  stoweidlem44  42349  stoweidlem45  42350  wallispilem3  42372  wallispilem4  42373  wallispi  42375  stirlinglem3  42381  stirlinglem5  42383  stirlinglem6  42384  stirlinglem7  42385  stirlinglem10  42388  stirlinglem11  42389  stirlinglem12  42390  dirkeritg  42407  dirkercncflem2  42409  fourierdlem9  42421  fourierdlem11  42423  fourierdlem12  42424  fourierdlem14  42426  fourierdlem15  42427  fourierdlem19  42431  fourierdlem24  42436  fourierdlem28  42440  fourierdlem30  42442  fourierdlem40  42452  fourierdlem41  42453  fourierdlem43  42455  fourierdlem44  42456  fourierdlem47  42458  fourierdlem50  42461  fourierdlem51  42462  fourierdlem57  42468  fourierdlem60  42471  fourierdlem61  42472  fourierdlem66  42477  fourierdlem68  42479  fourierdlem73  42484  fourierdlem74  42485  fourierdlem75  42486  fourierdlem78  42489  fourierdlem79  42490  fourierdlem83  42494  fourierdlem88  42499  fourierdlem92  42503  fourierdlem93  42504  fourierdlem97  42508  fourierdlem103  42514  fourierdlem104  42515  fourierdlem109  42520  fourierdlem111  42522  sqwvfoura  42533  sqwvfourb  42534  fourierswlem  42535  fouriersw  42536  elaa2lem  42538  etransclem4  42543  etransclem18  42557  etransclem19  42558  etransclem23  42562  etransclem27  42566  etransclem31  42570  etransclem32  42571  etransclem35  42574  etransclem41  42580  etransclem46  42585  etransclem48  42587  rrxtopnfi  42592  qndenserrnbllem  42599  salgencntex  42646  sge0tsms  42682  sge0isum  42729  volicorecl  42848  hoiprodcl  42849  ovnlerp  42864  ovnsubaddlem1  42872  hoiprodcl3  42882  volicore  42883  hoidmvcl  42884  hoidmvlelem1  42897  hoidmvlelem2  42898  hoidmvlelem3  42899  ovnhoi  42905  hoiqssbllem2  42925  volicorege0  42939  vonhoire  42974  pimrecltpos  43007  pimrecltneg  43021  smfmbfcex  43056  nsssmfmbflem  43074  smfrec  43084  smfmullem3  43088  sharhght  43142  zm1nn  43522  eluzge0nn0  43532  elfz2z  43535  2ffzoeq  43548  iccpartigtl  43603  iccpartgt  43607  requad01  43806  requad1  43807  requad2  43808  expnegico01  44593  m1modmmod  44601  difmodm1lt  44602  regt1loggt0  44616  refdivmptf  44622  elbigolo1  44637  rege1logbrege0  44638  fllog2  44648  dignn0flhalflem1  44695  eenglngeehlnmlem2  44745  line2  44759  line2xlem  44760  line2x  44761  line2y  44762  itsclc0yqsol  44771  2itscp  44788  inlinecirc02plem  44793  amgmwlem  44923