Theorem 0red 11239

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11127  0cc0 11128

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-1cn 11186  ax-addrcl 11189  ax-rnegex 11199  ax-cnre 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-clel 2837  df-rex 3089

This theorem is used by:  gt0ne0  11707  add20  11754  subge0  11755  lesub0  11759  mulge0  11760  msqgt0  11762  msqge0  11763  gt0ne0d  11806  addgt0d  11817  sublt0d  11868  prodgt0  12090  mulgt1  12104  lt2msq1  12127  fiminre2  12191  supmul1  12212  supmul  12215  nnne0  12298  0mnnnnn0  12564  nn0negleid  12584  0nn0m1nnn0  12679  neglt  13066  rpgecl  13076  ge0p1rp  13079  ledivge1le  13119  mul2lt0rlt0  13150  mul2lt0rgt0  13151  mul2lt0bi  13154  prodge0rd  13155  max0sub  13252  reltxrnmnf  13399  infmrp1  13401  lincmb01cmp  13552  iccf1o  13553  xov1plusxeqvd  13555  elfz0fzfz0  13692  fz0fzelfz0  13693  elfzo0z  13761  fzofzim  13769  fzo1fzo0n0  13775  elfzodifsumelfzo  13791  ssfzoulel  13820  elfznelfzo  13833  muladdmodid  13978  modltm1p1mod  13991  addmodlteq  14014  expgt1  14168  ltexp2a  14234  expcan  14237  ltexp2  14238  leexp2  14239  leexp2a  14240  zzlesq  14274  expnlbnd2  14302  discr  14308  fi1uzind  14576  ccatsymb  14652  ccat2s1fvw  14710  swrdnd  14728  swrdnnn0nd  14730  swrdswrdlem  14777  swrdswrd  14778  repswswrd  14859  swrd2lsw  15029  2swrd2eqwrdeq  15030  sgnneg  15177  sgnsub  15183  sgnmul  15184  leabs  15390  max0add  15401  absgt0  15416  rlimrege0  15670  iseraltlem2  15774  fsumrecl  15824  o1fsum  15904  cvgcmp  15907  cvgcmpce  15909  geomulcvg  15969  mertenslem2  15978  fprodle  16089  rpnnen2lem4  16311  p1modz1  16355  moddvds  16359  oddge22np1  16445  bitsfzolem  16530  bitsinv1lem  16537  sadcaddlem  16553  nn0rppwr  16657  nn0expgcd  16660  lcmgcdlem  16702  dvdsnprmd  16786  2mulprm  16789  isprm7  16805  qnumgt0  16847  modprm0  16903  qexpz  16999  prmreclem4  17017  4sqlem6  17041  prmgaplem7  17155  gzrngunit  21652  regsumfsum  21654  regsumsupp  21841  fvmptnn04ifd  23084  chfacffsupp  23087  chfacfscmul0  23089  chfacfscmulgsum  23091  chfacfpmmul0  23093  chfacfpmmulgsum  23095  prdsmet  24602  metustexhalf  24788  nlmvscnlem2  24917  nlmvscnlem1  24918  nmo0  24967  blcvx  25030  iihalf1cn  25166  evth  25193  lebnumlem1  25195  lebnumii  25200  htpycc  25214  pcohtpylem  25253  pcoass  25258  pcorevlem  25260  nmoleub2lem3  25349  ipcnlem2  25478  ipcnlem1  25479  rrxcph  25626  rrxmetlem  25641  rrxmet  25642  rrxdstprj1  25643  ehlbase  25649  minveclem3b  25662  minveclem6  25668  pjthlem1  25671  ovolicopnf  25758  ioorcl2  25806  volivth  25841  mbfposr  25886  i1fmulc  25937  itg1mulc  25938  itg1ge0a  25945  mbfi1flim  25957  itg2split  25983  itg2monolem1  25984  itg2monolem3  25986  itg2mono  25987  itg2cnlem2  25996  itgge0  26045  bddiblnc  26076  dvlip  26227  dvlipcn  26228  dveq0  26234  dv11cn  26235  dvlt0  26239  dvfsumge  26256  dgradd2  26501  plydivlem3  26532  mtest  26647  radcnvlem1  26656  radcnv0  26659  radcnvlt1  26661  radcnvle  26663  pserulm  26665  pserdvlem1  26670  pserdv  26672  abelthlem2  26675  abelthlem7  26681  pilem2  26695  pilem3  26696  coseq00topi  26747  tanabsge  26751  cosq34lt1  26772  tanord1  26782  tanord  26783  rplogcl  26849  logdivle  26867  logcnlem3  26889  logcnlem4  26890  dvloglem  26893  logtayl  26905  abscxp2  26938  cxplt  26939  cxple  26940  cxple2a  26944  cxpcn3lem  26992  abscxpbnd  26998  rtprmirr  27005  chordthmlem4  27080  chordthmlem5  27081  asinlem3  27116  atanre  27130  atanlogaddlem  27158  atanlogadd  27159  atanlogsublem  27160  atantan  27168  atans2  27176  efrlim  27214  cxp2limlem  27220  cxp2lim  27221  cxploglim2  27223  divsqrtsumlem  27224  jensenlem2  27232  harmonicubnd  27254  fsumharmonic  27256  dmlogdmgm  27268  lgamgulmlem1  27273  lgamgulmlem2  27274  ftalem1  27317  ftalem2  27318  ftalem5  27321  vmacl  27362  chtwordi  27400  ppiwordi  27406  chtrpcl  27419  fsumfldivdiaglem  27433  fsumvma2  27458  chpval2  27462  chpchtsum  27463  chpub  27464  logfacbnd3  27467  logexprlim  27469  mersenne  27471  lgsdilem  27568  lgsne0  27579  gausslemma2dlem1a  27609  lgseisen  27623  lgsquadlem1  27624  lgsquadlem2  27625  2sqmod  27680  2sqnn0  27682  chebbnd1lem2  27714  chebbnd1lem3  27715  chebbnd1  27716  chtppilimlem1  27717  chtppilimlem2  27718  chtppilim  27719  chebbnd2  27721  chto1lb  27722  chpchtlim  27723  chpo1ub  27724  dchrisumlema  27732  dchrisumlem2  27734  dchrisumlem3  27735  dchrmusumlema  27737  dchrvmasumlem2  27742  dchrvmasumiflem1  27745  dchrisum0flblem1  27752  dchrisum0flblem2  27753  dchrisum0re  27757  dchrisum0lema  27758  dchrisum0  27764  dirith2  27772  mulog2sumlem1  27778  vmalogdivsum2  27782  log2sumbnd  27788  selberg2lem  27794  chpdifbndlem1  27797  chpdifbnd  27799  selberg3lem1  27801  pntrmax  27808  pntrsumo1  27809  pntrlog2bndlem4  27824  pntrlog2bndlem5  27825  pntpbnd1a  27829  pntpbnd1  27830  pntpbnd2  27831  pntlemg  27842  pntlemj  27847  pntlemk  27850  pntlem3  27853  pnt2  27857  pnt  27858  ostth2lem1  27862  padicabv  27874  padicabvcxp  27876  ostth2lem3  27879  ostth2lem4  27880  ostth3  27882  trgcgrg  28865  tgcgr4  28881  axsegconlem7  29388  axsegconlem10  29391  axcontlem2  29430  axcontlem4  29432  axcontlem7  29435  axcontlem10  29438  crctcshwlkn0lem3  30288  crctcshwlkn0  30297  clwlkclwwlklem2a2  30471  clwlkclwwlklem2a  30476  wwlksubclwwlk  30536  frgrogt3nreg  30885  friendshipgt3  30886  minvecolem5  31370  minvecolem6  31371  htthlem  31406  pjhthlem1  31880  sgnval2  33214  nndiffz1  33265  bcm1n  33274  fzo0opth  33282  expgt0b  33295  nexple  33311  oexpled  33314  indf1o  33318  wrdt2ind  33403  cycpmrn  33591  cyc3conja  33605  ccfldextdgrr  34190  constrsslem  34259  constrresqrtcl  34295  constrsqrtcl  34297  cos9thpiminplylem1  34300  pnfneige0  34469  measinb  34740  eulerpartlems  34879  eulerpartlemgc  34881  ballotlemfc0  35012  ballotlemfcc  35013  ballotlemodife  35017  signsply0  35067  signslema  35078  signsvtp  35099  itgexpif  35122  breprexplemc  35148  circlemeth  35156  logdivsqrle  35166  cvmliftlem2  35873  dnibndlem9  37191  unbdqndv2lem2  37215  knoppndvlem1  37217  knoppndvlem2  37218  knoppndvlem7  37223  knoppndvlem11  37227  knoppndvlem14  37230  knoppndvlem15  37231  knoppndvlem17  37233  knoppndvlem19  37235  knoppndvlem20  37236  bj-pinftynminfty  37987  poimirlem10  38387  poimirlem11  38388  poimirlem24  38401  poimirlem29  38406  poimirlem31  38408  poimirlem32  38409  poimir  38410  mblfinlem2  38415  ftc1anclem7  38456  ftc1anclem8  38457  ftc1anc  38458  areacirclem1  38465  areacirclem4  38468  areacirc  38470  geomcau  38517  isbnd3b  38543  prdsbnd  38551  bfp  38582  rrnequiv  38593  resdvopclptsd  42902  lcmineqlem2  42904  lcmineqlem3  42905  lcmineqlem10  42912  lcmineqlem12  42914  lcmineqlem23  42925  3lexlogpow5ineq1  42928  3lexlogpow5ineq2  42929  3lexlogpow5ineq4  42930  3lexlogpow5ineq3  42931  3lexlogpow2ineq2  42933  3lexlogpow5ineq5  42934  aks4d1lem1  42936  dvrelog2  42938  dvrelog3  42939  dvrelog2b  42940  0nonelalab  42941  dvrelogpow2b  42942  aks4d1p1p3  42943  aks4d1p1p2  42944  aks4d1p1p4  42945  aks4d1p1p6  42947  aks4d1p1p7  42948  aks4d1p1p5  42949  aks4d1p1  42950  aks4d1p2  42951  aks4d1p3  42952  aks4d1p5  42954  aks4d1p6  42955  aks4d1p7d1  42956  aks4d1p7  42957  aks4d1p8d2  42959  aks4d1p8d3  42960  aks4d1p8  42961  aks4d1p9  42962  posbezout  42974  primrootspoweq0  42980  aks6d1c1  42990  hashscontpow1  42995  aks6d1c2lem4  43001  aks6d1c5lem2  43012  deg1gprod  43014  2np3bcnp1  43018  2ap1caineq  43019  sticksstones7  43026  sticksstones10  43029  sticksstones12a  43031  sticksstones12  43032  sticksstones22  43042  aks6d1c6lem3  43046  bcled  43052  bcle2d  43053  aks6d1c7lem1  43054  aks6d1c7lem2  43055  aks6d1c7  43058  aks5lem6  43066  unitscyglem5  43073  aks5lem8  43075  sn-1ne2  43154  oexpreposd  43205  posqsqznn  43219  redvmptabs  43243  readvrec  43245  re1m1e0m0  43280  re0m0e0  43285  remul01  43290  sn-remul0ord  43291  remulneg2d  43298  rediveq0d  43332  sn-rediv0d  43336  sn-addlt0d  43354  sn-addgt0d  43355  renegmulnnass  43361  zmulcomlem  43363  mulgt0con1dlem  43365  sn-mulgt1d  43375  mulltgt0d  43378  mullt0b2d  43380  sn-mullt0d  43381  sn-msqgt0d  43382  fimgmcyc  43424  dffltz  43488  3cubeslem1  43537  irrapxlem1  43671  irrapxlem2  43672  irrapxlem3  43673  irrapxlem4  43674  pellexlem6  43683  pell14qrgt0  43708  pell1qrgaplem  43722  pellfundex  43735  pellfundrp  43737  monotoddzzfi  43791  jm2.24  43812  jm2.23  43845  jm2.26lem3  43850  jm3.1lem3  43868  sqrtcvallem1  44479  reabsifneg  44480  reabsifpos  44482  sqrtcval  44489  k0004ss2  45000  imo72b2lem1  45017  dvgrat  45144  hashnzfz2  45153  binomcxplemnn0  45181  binomcxplemnotnn0  45188  divlt0gt0d  46127  upbdrech2  46149  xralrple2  46192  xralrple3  46211  reclt0d  46224  reclt0  46228  xrpnf  46321  fsumnncl  46410  fsumsupp0  46416  sumnnodd  46468  lptre2pt  46476  limsupubuz  46549  liminfresre  46615  liminf0  46629  dvmptconst  46751  dvdivbd  46759  dvcosax  46762  dvbdfbdioolem1  46764  dvbdfbdioolem2  46765  ioodvbdlimc1lem1  46767  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  dvxpaek  46776  dvnxpaek  46778  volioc  46808  volico  46819  stoweidlem1  46837  stoweidlem7  46843  stoweidlem11  46847  stoweidlem25  46861  stoweidlem26  46862  stoweidlem34  46870  stoweidlem36  46872  stoweidlem41  46877  stoweidlem42  46878  stoweidlem44  46880  stoweidlem45  46881  wallispilem3  46903  wallispilem4  46904  wallispi  46906  stirlinglem3  46912  stirlinglem5  46914  stirlinglem6  46915  stirlinglem7  46916  stirlinglem10  46919  stirlinglem11  46920  stirlinglem12  46921  dirkeritg  46938  dirkercncflem2  46940  fourierdlem9  46952  fourierdlem11  46954  fourierdlem12  46955  fourierdlem14  46957  fourierdlem15  46958  fourierdlem19  46962  fourierdlem24  46967  fourierdlem28  46971  fourierdlem30  46973  fourierdlem40  46983  fourierdlem41  46984  fourierdlem43  46986  fourierdlem44  46987  fourierdlem47  46989  fourierdlem50  46992  fourierdlem51  46993  fourierdlem57  46999  fourierdlem60  47002  fourierdlem61  47003  fourierdlem66  47008  fourierdlem68  47010  fourierdlem73  47015  fourierdlem74  47016  fourierdlem75  47017  fourierdlem78  47020  fourierdlem79  47021  fourierdlem83  47025  fourierdlem88  47030  fourierdlem92  47034  fourierdlem93  47035  fourierdlem97  47039  fourierdlem103  47045  fourierdlem104  47046  fourierdlem109  47051  fourierdlem111  47053  sqwvfoura  47064  sqwvfourb  47065  fourierswlem  47066  fouriersw  47067  elaa2lem  47069  etransclem4  47074  etransclem18  47088  etransclem19  47089  etransclem23  47093  etransclem27  47097  etransclem31  47101  etransclem32  47102  etransclem35  47105  etransclem41  47111  etransclem46  47116  etransclem48  47118  rrxtopnfi  47123  qndenserrnbllem  47130  salgencntex  47179  sge0tsms  47216  sge0isum  47263  volicorecl  47382  hoiprodcl  47383  ovnlerp  47398  ovnsubaddlem1  47406  hoiprodcl3  47416  volicore  47417  hoidmvcl  47418  hoidmvlelem1  47431  hoidmvlelem2  47432  hoidmvlelem3  47433  ovnhoi  47439  hoiqssbllem2  47459  volicorege0  47473  vonhoire  47508  pimrecltpos  47544  pimrecltneg  47560  smfmbfcex  47596  nsssmfmbflem  47614  smfrec  47625  smfmullem3  47629  smfdivdmmbl  47674  sharhght  47701  et-sqrtnegnre  47709  ormkglobd  47713  chnsubseqwl  47715  zm1nn  48198  eluzge0nn0  48208  elfz2z  48211  2ffzoeq  48224  m1modmmod  48260  modm1p1ne  48272  muldvdsfacm1  48283  iccpartigtl  48331  iccpartgt  48335  nprmdvdsfacm1lem4  48534  requad01  48545  requad1  48546  requad2  48547  stgrusgra  48883  gpgedgvtx1  48986  expnegico01  49456  regt1loggt0  49474  refdivmptf  49480  elbigolo1  49495  rege1logbrege0  49496  fllog2  49506  dignn0flhalflem1  49553  eenglngeehlnmlem2  49676  line2  49690  line2xlem  49691  line2x  49692  line2y  49693  itsclc0yqsol  49702  2itscp  49719  inlinecirc02plem  49724  veronesefvcl  50813  veronesev1lem  50814  veronesev2lem  50815  veronesev3lem  50816  veronesev4lem  50817  veronesev5lem  50818  veronesev6lem  50819  amgmwlem  50828