Theorem 0red 11145

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℝcr 11035  0cc0 11036

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-1cn 11094  ax-addrcl 11097  ax-rnegex 11107  ax-cnre 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-clel 2815  df-rex 3065

This theorem is referenced by:  gt0ne0  11613  add20  11660  subge0  11661  lesub0  11665  mulge0  11666  msqgt0  11668  msqge0  11669  gt0ne0d  11712  addgt0d  11723  sublt0d  11774  prodgt0  12000  mulgt1  12015  lt2msq1  12038  fiminre2  12102  supmul1  12123  supmul  12126  nnne0  12209  0mnnnnn0  12467  nn0negleid  12487  neglt  12960  rpgecl  12970  ge0p1rp  12973  ledivge1le  13013  mul2lt0rlt0  13044  mul2lt0rgt0  13045  mul2lt0bi  13048  prodge0rd  13049  max0sub  13146  reltxrnmnf  13293  infmrp1  13295  lincmb01cmp  13446  iccf1o  13447  xov1plusxeqvd  13449  elfz0fzfz0  13585  fz0fzelfz0  13586  elfzo0z  13654  fzofzim  13662  fzo1fzo0n0  13668  elfzodifsumelfzo  13684  ssfzoulel  13713  elfznelfzo  13726  muladdmodid  13870  modltm1p1mod  13883  addmodlteq  13906  expgt1  14060  ltexp2a  14126  expcan  14129  ltexp2  14130  leexp2  14131  leexp2a  14132  zzlesq  14166  expnlbnd2  14194  discr  14200  fi1uzind  14467  ccatsymb  14543  ccat2s1fvw  14599  swrdnd  14615  swrdnnn0nd  14617  swrdswrdlem  14664  swrdswrd  14665  repswswrd  14744  swrd2lsw  14912  2swrd2eqwrdeq  14913  leabs  15259  max0add  15270  absgt0  15285  rlimrege0  15539  iseraltlem2  15643  fsumrecl  15694  o1fsum  15774  cvgcmp  15777  cvgcmpce  15779  geomulcvg  15839  mertenslem2  15848  fprodle  15959  rpnnen2lem4  16182  p1modz1  16226  moddvds  16230  oddge22np1  16316  bitsfzolem  16401  bitsinv1lem  16408  sadcaddlem  16424  nn0rppwr  16528  nn0expgcd  16531  lcmgcdlem  16573  dvdsnprmd  16657  2mulprm  16660  isprm7  16676  qnumgt0  16718  modprm0  16774  qexpz  16870  prmreclem4  16888  4sqlem6  16912  prmgaplem7  17026  gzrngunit  21415  regsumfsum  21417  regsumsupp  21604  fvmptnn04ifd  22843  chfacffsupp  22846  chfacfscmul0  22848  chfacfscmulgsum  22850  chfacfpmmul0  22852  chfacfpmmulgsum  22854  prdsmet  24360  metustexhalf  24546  nlmvscnlem2  24675  nlmvscnlem1  24676  nmo0  24725  blcvx  24788  iihalf1cn  24924  evth  24951  lebnumlem1  24953  lebnumii  24958  htpycc  24972  pcohtpylem  25011  pcoass  25016  pcorevlem  25018  nmoleub2lem3  25107  ipcnlem2  25236  ipcnlem1  25237  rrxcph  25384  rrxmetlem  25399  rrxmet  25400  rrxdstprj1  25401  ehlbase  25407  minveclem3b  25420  minveclem6  25426  pjthlem1  25429  ovolicopnf  25516  ioorcl2  25564  volivth  25599  mbfposr  25644  i1fmulc  25695  itg1mulc  25696  itg1ge0a  25703  mbfi1flim  25715  itg2split  25741  itg2monolem1  25742  itg2monolem3  25744  itg2mono  25745  itg2cnlem2  25754  itgge0  25803  bddiblnc  25834  dvlip  25985  dvlipcn  25986  dveq0  25992  dv11cn  25993  dvlt0  25997  dvfsumge  26014  dgradd2  26258  plydivlem3  26286  mtest  26394  radcnvlem1  26403  radcnv0  26406  radcnvlt1  26408  radcnvle  26410  pserulm  26412  pserdvlem1  26417  pserdv  26419  abelthlem2  26422  abelthlem7  26428  pilem2  26442  pilem3  26443  coseq00topi  26491  tanabsge  26495  cosq34lt1  26516  tanord1  26526  tanord  26527  rplogcl  26593  logdivle  26611  logcnlem3  26633  logcnlem4  26634  dvloglem  26637  logtayl  26649  abscxp2  26682  cxplt  26683  cxple  26684  cxple2a  26688  cxpcn3lem  26736  abscxpbnd  26742  rtprmirr  26749  chordthmlem4  26824  chordthmlem5  26825  asinlem3  26860  atanre  26874  atanlogaddlem  26902  atanlogadd  26903  atanlogsublem  26904  atantan  26912  atans2  26920  efrlim  26958  cxp2limlem  26964  cxp2lim  26965  cxploglim2  26967  divsqrtsumlem  26968  jensenlem2  26976  harmonicubnd  26998  fsumharmonic  27000  dmlogdmgm  27012  lgamgulmlem1  27017  lgamgulmlem2  27018  ftalem1  27061  ftalem2  27062  ftalem5  27065  vmacl  27106  chtwordi  27144  ppiwordi  27150  chtrpcl  27163  fsumfldivdiaglem  27177  fsumvma2  27202  chpval2  27206  chpchtsum  27207  chpub  27208  logfacbnd3  27211  logexprlim  27213  mersenne  27215  lgsdilem  27312  lgsne0  27323  gausslemma2dlem1a  27353  lgseisen  27367  lgsquadlem1  27368  lgsquadlem2  27369  2sqmod  27424  2sqnn0  27426  chebbnd1lem2  27458  chebbnd1lem3  27459  chebbnd1  27460  chtppilimlem1  27461  chtppilimlem2  27462  chtppilim  27463  chebbnd2  27465  chto1lb  27466  chpchtlim  27467  chpo1ub  27468  dchrisumlema  27476  dchrisumlem2  27478  dchrisumlem3  27479  dchrmusumlema  27481  dchrvmasumlem2  27486  dchrvmasumiflem1  27489  dchrisum0flblem1  27496  dchrisum0flblem2  27497  dchrisum0re  27501  dchrisum0lema  27502  dchrisum0  27508  dirith2  27516  mulog2sumlem1  27522  vmalogdivsum2  27526  log2sumbnd  27532  selberg2lem  27538  chpdifbndlem1  27541  chpdifbnd  27543  selberg3lem1  27545  pntrmax  27552  pntrsumo1  27553  pntrlog2bndlem4  27568  pntrlog2bndlem5  27569  pntpbnd1a  27573  pntpbnd1  27574  pntpbnd2  27575  pntlemg  27586  pntlemj  27591  pntlemk  27594  pntlem3  27597  pnt2  27601  pnt  27602  ostth2lem1  27606  padicabv  27618  padicabvcxp  27620  ostth2lem3  27623  ostth2lem4  27624  ostth3  27626  trgcgrg  28608  tgcgr4  28624  axsegconlem7  29017  axsegconlem10  29020  axcontlem2  29059  axcontlem4  29061  axcontlem7  29064  axcontlem10  29067  crctcshwlkn0lem3  29905  crctcshwlkn0  29914  clwlkclwwlklem2a2  30088  clwlkclwwlklem2a  30093  wwlksubclwwlk  30153  frgrogt3nreg  30492  friendshipgt3  30493  minvecolem5  30977  minvecolem6  30978  htthlem  31013  pjhthlem1  31487  sgnval2  32834  nndiffz1  32885  bcm1n  32894  fzo0opth  32902  expgt0b  32916  sgnneg  32932  sgnmul  32934  sgnsub  32936  nexple  32943  oexpled  32946  indf1o  32950  wrdt2ind  33039  cycpmrn  33231  cyc3conja  33245  ccfldextdgrr  33863  constrsslem  33932  constrresqrtcl  33968  constrsqrtcl  33970  cos9thpiminplylem1  33973  pnfneige0  34142  measinb  34412  eulerpartlems  34551  eulerpartlemgc  34553  ballotlemfc0  34684  ballotlemfcc  34685  ballotlemodife  34689  signsply0  34742  signslema  34753  signsvtp  34774  itgexpif  34797  breprexplemc  34823  circlemeth  34831  logdivsqrle  34841  0nn0m1nnn0  35348  cvmliftlem2  35521  dnibndlem9  36799  unbdqndv2lem2  36823  knoppndvlem1  36825  knoppndvlem2  36826  knoppndvlem7  36831  knoppndvlem11  36835  knoppndvlem14  36838  knoppndvlem15  36839  knoppndvlem17  36841  knoppndvlem19  36843  knoppndvlem20  36844  bj-pinftynminfty  37594  poimirlem10  38004  poimirlem11  38005  poimirlem24  38018  poimirlem29  38023  poimirlem31  38025  poimirlem32  38026  poimir  38027  mblfinlem2  38032  ftc1anclem7  38073  ftc1anclem8  38074  ftc1anc  38075  areacirclem1  38082  areacirclem4  38085  areacirc  38087  geomcau  38133  isbnd3b  38159  prdsbnd  38167  bfp  38198  rrnequiv  38209  resdvopclptsd  42520  lcmineqlem2  42522  lcmineqlem3  42523  lcmineqlem10  42530  lcmineqlem12  42532  lcmineqlem23  42543  3lexlogpow5ineq1  42546  3lexlogpow5ineq2  42547  3lexlogpow5ineq4  42548  3lexlogpow5ineq3  42549  3lexlogpow2ineq2  42551  3lexlogpow5ineq5  42552  aks4d1lem1  42554  dvrelog2  42556  dvrelog3  42557  dvrelog2b  42558  0nonelalab  42559  dvrelogpow2b  42560  aks4d1p1p3  42561  aks4d1p1p2  42562  aks4d1p1p4  42563  aks4d1p1p6  42565  aks4d1p1p7  42566  aks4d1p1p5  42567  aks4d1p1  42568  aks4d1p2  42569  aks4d1p3  42570  aks4d1p5  42572  aks4d1p6  42573  aks4d1p7d1  42574  aks4d1p7  42575  aks4d1p8d2  42577  aks4d1p8d3  42578  aks4d1p8  42579  aks4d1p9  42580  posbezout  42592  primrootspoweq0  42598  aks6d1c1  42608  hashscontpow1  42613  aks6d1c2lem4  42619  aks6d1c5lem2  42630  deg1gprod  42632  2np3bcnp1  42636  2ap1caineq  42637  sticksstones7  42644  sticksstones10  42647  sticksstones12a  42649  sticksstones12  42650  sticksstones22  42660  aks6d1c6lem3  42664  bcled  42670  bcle2d  42671  aks6d1c7lem1  42672  aks6d1c7lem2  42673  aks6d1c7  42676  aks5lem6  42684  unitscyglem5  42691  aks5lem8  42693  sn-1ne2  42755  oexpreposd  42806  posqsqznn  42820  redvmptabs  42844  readvrec  42846  re1m1e0m0  42881  re0m0e0  42886  remul01  42891  sn-remul0ord  42892  remulneg2d  42899  rediveq0d  42933  sn-rediv0d  42937  sn-addlt0d  42955  sn-addgt0d  42956  renegmulnnass  42962  zmulcomlem  42964  mulgt0con1dlem  42966  sn-mulgt1d  42976  mulltgt0d  42979  mullt0b2d  42981  sn-mullt0d  42982  sn-msqgt0d  42983  fimgmcyc  43027  dffltz  43091  3cubeslem1  43140  irrapxlem1  43274  irrapxlem2  43275  irrapxlem3  43276  irrapxlem4  43277  pellexlem6  43286  pell14qrgt0  43311  pell1qrgaplem  43325  pellfundex  43338  pellfundrp  43340  monotoddzzfi  43394  jm2.24  43415  jm2.23  43448  jm2.26lem3  43453  jm3.1lem3  43471  sqrtcvallem1  44082  reabsifneg  44083  reabsifpos  44085  sqrtcval  44092  k0004ss2  44603  imo72b2lem1  44620  dvgrat  44763  hashnzfz2  44772  binomcxplemnn0  44800  binomcxplemnotnn0  44807  divlt0gt0d  45741  upbdrech2  45763  xralrple2  45806  xralrple3  45825  reclt0d  45838  reclt0  45842  xrpnf  45935  fsumnncl  46024  fsumsupp0  46030  sumnnodd  46082  lptre2pt  46090  limsupubuz  46163  liminfresre  46229  liminf0  46243  dvmptconst  46365  dvdivbd  46373  dvcosax  46376  dvbdfbdioolem1  46378  dvbdfbdioolem2  46379  ioodvbdlimc1lem1  46381  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvxpaek  46390  dvnxpaek  46392  volioc  46422  volico  46433  stoweidlem1  46451  stoweidlem7  46457  stoweidlem11  46461  stoweidlem25  46475  stoweidlem26  46476  stoweidlem34  46484  stoweidlem36  46486  stoweidlem41  46491  stoweidlem42  46492  stoweidlem44  46494  stoweidlem45  46495  wallispilem3  46517  wallispilem4  46518  wallispi  46520  stirlinglem3  46526  stirlinglem5  46528  stirlinglem6  46529  stirlinglem7  46530  stirlinglem10  46533  stirlinglem11  46534  stirlinglem12  46535  dirkeritg  46552  dirkercncflem2  46554  fourierdlem9  46566  fourierdlem11  46568  fourierdlem12  46569  fourierdlem14  46571  fourierdlem15  46572  fourierdlem19  46576  fourierdlem24  46581  fourierdlem28  46585  fourierdlem30  46587  fourierdlem40  46597  fourierdlem41  46598  fourierdlem43  46600  fourierdlem44  46601  fourierdlem47  46603  fourierdlem50  46606  fourierdlem51  46607  fourierdlem57  46613  fourierdlem60  46616  fourierdlem61  46617  fourierdlem66  46622  fourierdlem68  46624  fourierdlem73  46629  fourierdlem74  46630  fourierdlem75  46631  fourierdlem78  46634  fourierdlem79  46635  fourierdlem83  46639  fourierdlem88  46644  fourierdlem92  46648  fourierdlem93  46649  fourierdlem97  46653  fourierdlem103  46659  fourierdlem104  46660  fourierdlem109  46665  fourierdlem111  46667  sqwvfoura  46678  sqwvfourb  46679  fourierswlem  46680  fouriersw  46681  elaa2lem  46683  etransclem4  46688  etransclem18  46702  etransclem19  46703  etransclem23  46707  etransclem27  46711  etransclem31  46715  etransclem32  46716  etransclem35  46719  etransclem41  46725  etransclem46  46730  etransclem48  46732  rrxtopnfi  46737  qndenserrnbllem  46744  salgencntex  46793  sge0tsms  46830  sge0isum  46877  volicorecl  46996  hoiprodcl  46997  ovnlerp  47012  ovnsubaddlem1  47020  hoiprodcl3  47030  volicore  47031  hoidmvcl  47032  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  ovnhoi  47053  hoiqssbllem2  47073  volicorege0  47087  vonhoire  47122  pimrecltpos  47158  pimrecltneg  47174  smfmbfcex  47210  nsssmfmbflem  47228  smfrec  47239  smfmullem3  47243  smfdivdmmbl  47288  sharhght  47315  et-sqrtnegnre  47323  ormkglobd  47327  natglobalincr  47329  chnsubseqwl  47331  zm1nn  47772  eluzge0nn0  47782  elfz2z  47785  2ffzoeq  47798  m1modmmod  47834  modm1p1ne  47846  muldvdsfacm1  47857  iccpartigtl  47905  iccpartgt  47909  nprmdvdsfacm1lem4  48108  requad01  48119  requad1  48120  requad2  48121  stgrusgra  48457  gpgedgvtx1  48560  expnegico01  49016  regt1loggt0  49034  refdivmptf  49040  elbigolo1  49055  rege1logbrege0  49056  fllog2  49066  dignn0flhalflem1  49113  eenglngeehlnmlem2  49236  line2  49250  line2xlem  49251  line2x  49252  line2y  49253  itsclc0yqsol  49262  2itscp  49279  inlinecirc02plem  49284  amgmwlem  50299