Theorem 0red 11311

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

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

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 2733  ax-1cn 11258  ax-addrcl 11261  ax-rnegex 11271  ax-cnre 11273

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836  df-rex 3088

This theorem is used by:  gt0ne0  11781  add20  11828  subge0  11829  lesub0  11833  mulge0  11834  msqgt0  11836  msqge0  11837  gt0ne0d  11880  addgt0d  11891  sublt0d  11942  prodgt0  12164  mulgt1  12178  lt2msq1  12201  fiminre2  12265  supmul1  12286  supmul  12289  nnne0  12372  0mnnnnn0  12638  nn0negleid  12658  0nn0m1nnn0  12753  neglt  13140  rpgecl  13150  ge0p1rp  13153  ledivge1le  13193  mul2lt0rlt0  13224  mul2lt0rgt0  13225  mul2lt0bi  13228  prodge0rd  13229  max0sub  13326  reltxrnmnf  13473  infmrp1  13475  lincmb01cmp  13626  iccf1o  13627  xov1plusxeqvd  13629  elfz0fzfz0  13767  fz0fzelfz0  13768  elfzo0z  13836  fzofzim  13844  fzo1fzo0n0  13850  elfzodifsumelfzo  13866  ssfzoulel  13895  elfznelfzo  13908  muladdmodid  14053  modltm1p1mod  14066  addmodlteq  14089  expgt1  14243  ltexp2a  14309  expcan  14312  ltexp2  14313  leexp2  14314  leexp2a  14315  zzlesq  14350  expnlbnd2  14378  discr  14384  fi1uzind  14652  ccatsymb  14728  ccat2s1fvw  14786  swrdnd  14804  swrdnnn0nd  14806  swrdswrdlem  14853  swrdswrd  14854  repswswrd  14935  swrd2lsw  15105  2swrd2eqwrdeq  15106  sgnneg  15253  sgnsub  15259  sgnmul  15260  leabs  15466  max0add  15477  absgt0  15492  rlimrege0  15746  iseraltlem2  15850  fsumrecl  15900  o1fsum  15980  cvgcmp  15983  cvgcmpce  15985  geomulcvg  16045  mertenslem2  16054  fprodle  16163  rpnnen2lem4  16385  p1modz1  16429  moddvds  16433  oddge22np1  16519  bitsfzolem  16604  bitsinv1lem  16611  sadcaddlem  16627  nn0rppwr  16735  nn0expgcd  16738  lcmgcdlem  16781  dvdsnprmd  16865  2mulprm  16868  isprm7  16884  qnumgt0  16926  posqsqznn  16936  modprm0  16983  qexpz  17079  prmreclem4  17097  4sqlem6  17121  prmgaplem7  17235  gzrngunit  21739  regsumfsum  21741  regsumsupp  21928  fvmptnn04ifd  23171  chfacffsupp  23174  chfacfscmul0  23176  chfacfscmulgsum  23178  chfacfpmmul0  23180  chfacfpmmulgsum  23182  prdsmet  24689  metustexhalf  24875  nlmvscnlem2  25004  nlmvscnlem1  25005  nmo0  25054  blcvx  25117  iihalf1cn  25253  evth  25280  lebnumlem1  25282  lebnumii  25287  htpycc  25301  pcohtpylem  25340  pcoass  25345  pcorevlem  25347  nmoleub2lem3  25436  ipcnlem2  25565  ipcnlem1  25566  rrxcph  25713  rrxmetlem  25728  rrxmet  25729  rrxdstprj1  25730  ehlbase  25736  minveclem3b  25749  minveclem6  25755  pjthlem1  25758  ovolicopnf  25845  ioorcl2  25893  volivth  25928  mbfposr  25973  i1fmulc  26024  itg1mulc  26025  itg1ge0a  26032  mbfi1flim  26044  itg2split  26070  itg2monolem1  26071  itg2monolem3  26073  itg2mono  26074  itg2cnlem2  26083  itgge0  26131  bddiblnc  26162  dvlip  26313  dvlipcn  26314  dveq0  26320  dv11cn  26321  dvlt0  26325  dvfsumge  26342  dgradd2  26587  plydivlem3  26616  mtest  26731  radcnvlem1  26740  radcnv0  26743  radcnvlt1  26745  radcnvle  26747  pserulm  26749  pserdvlem1  26754  pserdv  26756  abelthlem2  26759  abelthlem7  26765  pilem2  26779  pilem3  26780  coseq00topi  26831  tanabsge  26835  cosq34lt1  26855  tanord1  26865  tanord  26866  rplogcl  26932  logdivle  26950  logcnlem3  26972  logcnlem4  26973  dvloglem  26976  logtayl  26988  abscxp2  27021  cxplt  27022  cxple  27023  cxple2a  27027  cxpcn3lem  27075  abscxpbnd  27081  rtprmirr  27088  chordthmlem4  27163  chordthmlem5  27164  asinlem3  27199  atanre  27213  atanlogaddlem  27241  atanlogadd  27242  atanlogsublem  27243  atantan  27251  atans2  27259  efrlim  27297  cxp2limlem  27303  cxp2lim  27304  cxploglim2  27306  divsqrtsumlem  27307  jensenlem2  27315  harmonicubnd  27337  fsumharmonic  27339  dmlogdmgm  27351  lgamgulmlem1  27356  lgamgulmlem2  27357  ftalem1  27400  ftalem2  27401  ftalem5  27404  vmacl  27445  chtwordi  27483  ppiwordi  27489  chtrpcl  27502  fsumfldivdiaglem  27516  fsumvma2  27541  chpval2  27545  chpchtsum  27546  chpub  27547  logfacbnd3  27550  logexprlim  27552  mersenne  27554  lgsdilem  27651  lgsne0  27662  gausslemma2dlem1a  27692  lgseisen  27706  lgsquadlem1  27707  lgsquadlem2  27708  2sqmod  27763  2sqnn0  27765  chebbnd1lem2  27797  chebbnd1lem3  27798  chebbnd1  27799  chtppilimlem1  27800  chtppilimlem2  27801  chtppilim  27802  chebbnd2  27804  chto1lb  27805  chpchtlim  27806  chpo1ub  27807  dchrisumlema  27815  dchrisumlem2  27817  dchrisumlem3  27818  dchrmusumlema  27820  dchrvmasumlem2  27825  dchrvmasumiflem1  27828  dchrisum0flblem1  27835  dchrisum0flblem2  27836  dchrisum0re  27840  dchrisum0lema  27841  dchrisum0  27847  dirith2  27855  mulog2sumlem1  27861  vmalogdivsum2  27865  log2sumbnd  27871  selberg2lem  27877  chpdifbndlem1  27880  chpdifbnd  27882  selberg3lem1  27884  pntrmax  27891  pntrsumo1  27892  pntrlog2bndlem4  27907  pntrlog2bndlem5  27908  pntpbnd1a  27912  pntpbnd1  27913  pntpbnd2  27914  pntlemg  27925  pntlemj  27930  pntlemk  27933  pntlem3  27936  pnt2  27940  pnt  27941  ostth2lem1  27945  padicabv  27957  padicabvcxp  27959  ostth2lem3  27962  ostth2lem4  27963  ostth3  27965  trgcgrg  28978  tgcgr4  28994  axsegconlem7  29501  axsegconlem10  29504  axcontlem2  29543  axcontlem4  29545  axcontlem7  29548  axcontlem10  29551  crctcshwlkn0lem3  30401  crctcshwlkn0  30410  clwlkclwwlklem2a2  30584  clwlkclwwlklem2a  30589  wwlksubclwwlk  30649  frgrogt3nreg  30998  friendshipgt3  30999  minvecolem5  31483  minvecolem6  31484  htthlem  31519  pjhthlem1  31993  sgnval2  33327  nndiffz1  33378  bcm1n  33387  fzo0opth  33395  expgt0b  33408  nexple  33424  oexpled  33427  indf1o  33431  wrdt2ind  33516  cycpmrn  33704  cyc3conja  33718  ccfldextdgrr  34304  constrsslem  34373  constrresqrtcl  34409  constrsqrtcl  34411  cos9thpiminplylem1  34414  pnfneige0  34583  measinb  34854  eulerpartlems  34992  eulerpartlemgc  34994  ballotlemfc0  35125  ballotlemfcc  35126  ballotlemodife  35130  signsply0  35180  signslema  35191  signsvtp  35212  itgexpif  35235  breprexplemc  35261  circlemeth  35269  logdivsqrle  35279  cvmliftlem2  36051  dnibndlem9  37352  unbdqndv2lem2  37376  knoppndvlem1  37378  knoppndvlem2  37379  knoppndvlem7  37384  knoppndvlem11  37388  knoppndvlem14  37391  knoppndvlem15  37392  knoppndvlem17  37394  knoppndvlem19  37396  knoppndvlem20  37397  bj-pinftynminfty  38149  poimirlem10  38549  poimirlem11  38550  poimirlem24  38563  poimirlem29  38568  poimirlem31  38570  poimirlem32  38571  poimir  38572  mblfinlem2  38577  ftc1anclem7  38618  ftc1anclem8  38619  ftc1anc  38620  areacirclem1  38627  areacirclem4  38630  areacirc  38632  geomcau  38694  isbnd3b  38720  prdsbnd  38728  bfp  38759  rrnequiv  38770  resdvopclptsd  43079  lcmineqlem2  43081  lcmineqlem3  43082  lcmineqlem10  43089  lcmineqlem12  43091  lcmineqlem23  43102  3lexlogpow5ineq1  43105  3lexlogpow5ineq2  43106  3lexlogpow5ineq4  43107  3lexlogpow5ineq3  43108  3lexlogpow2ineq2  43110  3lexlogpow5ineq5  43111  aks4d1lem1  43113  dvrelog2  43115  dvrelog3  43116  dvrelog2b  43117  0nonelalab  43118  dvrelogpow2b  43119  aks4d1p1p3  43120  aks4d1p1p2  43121  aks4d1p1p4  43122  aks4d1p1p6  43124  aks4d1p1p7  43125  aks4d1p1p5  43126  aks4d1p1  43127  aks4d1p2  43128  aks4d1p3  43129  aks4d1p5  43131  aks4d1p6  43132  aks4d1p7d1  43133  aks4d1p7  43134  aks4d1p8d2  43136  aks4d1p8d3  43137  aks4d1p8  43138  aks4d1p9  43139  posbezout  43151  primrootspoweq0  43157  aks6d1c1  43167  hashscontpow1  43172  aks6d1c2lem4  43178  aks6d1c5lem2  43189  deg1gprod  43191  2np3bcnp1  43195  2ap1caineq  43196  sticksstones7  43203  sticksstones10  43206  sticksstones12a  43208  sticksstones12  43209  sticksstones22  43219  aks6d1c6lem3  43223  bcled  43229  bcle2d  43230  aks6d1c7lem1  43231  aks6d1c7lem2  43232  aks6d1c7  43235  aks5lem6  43243  unitscyglem5  43250  aks5lem8  43252  sn-1ne2  43331  oexpreposd  43380  redvmptabs  43412  readvrec  43414  re1m1e0m0  43449  re0m0e0  43454  remul01  43459  sn-remul0ord  43460  remulneg2d  43467  rediveq0d  43501  sn-rediv0d  43505  sn-addlt0d  43523  sn-addgt0d  43524  renegmulnnass  43530  zmulcomlem  43532  mulgt0con1dlem  43534  sn-mulgt1d  43544  mulltgt0d  43547  mullt0b2d  43549  sn-mullt0d  43550  sn-msqgt0d  43551  fimgmcyc  43599  dffltz  43671  3cubeslem1  43695  irrapxlem1  43829  irrapxlem2  43830  irrapxlem3  43831  irrapxlem4  43832  pellexlem6  43841  pell14qrgt0  43866  pell1qrgaplem  43880  pellfundex  43893  pellfundrp  43895  monotoddzzfi  43949  jm2.24  43970  jm2.23  44003  jm2.26lem3  44008  jm3.1lem3  44026  sqrtcvallem1  44631  reabsifneg  44632  reabsifpos  44634  sqrtcval  44641  k0004ss2  45152  imo72b2lem1  45169  dvgrat  45296  hashnzfz2  45305  binomcxplemnn0  45333  binomcxplemnotnn0  45340  divlt0gt0d  46302  upbdrech2  46324  xralrple2  46366  xralrple3  46385  reclt0d  46398  reclt0  46402  xrpnf  46495  fsumnncl  46584  fsumsupp0  46590  sumnnodd  46642  lptre2pt  46650  limsupubuz  46723  liminfresre  46789  liminf0  46803  dvmptconst  46925  dvdivbd  46933  dvcosax  46936  dvbdfbdioolem1  46938  dvbdfbdioolem2  46939  ioodvbdlimc1lem1  46941  ioodvbdlimc1lem2  46942  ioodvbdlimc2lem  46944  dvxpaek  46950  dvnxpaek  46952  volioc  46982  volico  46993  stoweidlem1  47011  stoweidlem7  47017  stoweidlem11  47021  stoweidlem25  47035  stoweidlem26  47036  stoweidlem34  47044  stoweidlem36  47046  stoweidlem41  47051  stoweidlem42  47052  stoweidlem44  47054  stoweidlem45  47055  wallispilem3  47077  wallispilem4  47078  wallispi  47080  stirlinglem3  47086  stirlinglem5  47088  stirlinglem6  47089  stirlinglem7  47090  stirlinglem10  47093  stirlinglem11  47094  stirlinglem12  47095  dirkeritg  47112  dirkercncflem2  47114  fourierdlem9  47126  fourierdlem11  47128  fourierdlem12  47129  fourierdlem14  47131  fourierdlem15  47132  fourierdlem19  47136  fourierdlem24  47141  fourierdlem28  47145  fourierdlem30  47147  fourierdlem40  47157  fourierdlem41  47158  fourierdlem43  47160  fourierdlem44  47161  fourierdlem47  47163  fourierdlem50  47166  fourierdlem51  47167  fourierdlem57  47173  fourierdlem60  47176  fourierdlem61  47177  fourierdlem66  47182  fourierdlem68  47184  fourierdlem73  47189  fourierdlem74  47190  fourierdlem75  47191  fourierdlem78  47194  fourierdlem79  47195  fourierdlem83  47199  fourierdlem88  47204  fourierdlem92  47208  fourierdlem93  47209  fourierdlem97  47213  fourierdlem103  47219  fourierdlem104  47220  fourierdlem109  47225  fourierdlem111  47227  sqwvfoura  47238  sqwvfourb  47239  fourierswlem  47240  fouriersw  47241  elaa2lem  47243  etransclem4  47248  etransclem18  47262  etransclem19  47263  etransclem23  47267  etransclem27  47271  etransclem31  47275  etransclem32  47276  etransclem35  47279  etransclem41  47285  etransclem46  47290  etransclem48  47292  rrxtopnfi  47297  qndenserrnbllem  47304  salgencntex  47353  sge0tsms  47390  sge0isum  47437  volicorecl  47556  hoiprodcl  47557  ovnlerp  47572  ovnsubaddlem1  47580  hoiprodcl3  47590  volicore  47591  hoidmvcl  47592  hoidmvlelem1  47605  hoidmvlelem2  47606  hoidmvlelem3  47607  ovnhoi  47613  hoiqssbllem2  47633  volicorege0  47647  vonhoire  47682  pimrecltpos  47718  pimrecltneg  47734  smfmbfcex  47770  nsssmfmbflem  47788  smfrec  47799  smfmullem3  47803  smfdivdmmbl  47848  sharhght  47875  et-sqrtnegnre  47883  ormkglobd  47887  chnsubseqwl  47889  zm1nn  48372  eluzge0nn0  48382  elfz2z  48385  2ffzoeq  48398  m1modmmod  48434  modm1p1ne  48446  muldvdsfacm1  48457  iccpartigtl  48505  iccpartgt  48509  nprmdvdsfacm1lem4  48708  requad01  48719  requad1  48720  requad2  48721  stgrusgra  49057  gpgedgvtx1  49160  expnegico01  49630  regt1loggt0  49648  refdivmptf  49654  elbigolo1  49669  rege1logbrege0  49670  fllog2  49680  dignn0flhalflem1  49727  eenglngeehlnmlem2  49850  line2  49864  line2xlem  49865  line2x  49866  line2y  49867  itsclc0yqsol  49876  2itscp  49893  inlinecirc02plem  49898  veronesefvcl  50972  veronesev1lem  50973  veronesev2lem  50974  veronesev3lem  50975  veronesev4lem  50976  veronesev5lem  50977  veronesev6lem  50978  amgmwlem  50987