Theorem 0red 11137

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11027  0cc0 11028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11086  ax-addrcl 11089  ax-rnegex 11099  ax-cnre 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803  df-rex 3054

This theorem is referenced by:  gt0ne0  11603  add20  11650  subge0  11651  lesub0  11655  mulge0  11656  msqgt0  11658  msqge0  11659  gt0ne0d  11702  addgt0d  11713  sublt0d  11764  prodgt0  11989  mulgt1  12004  lt2msq1  12027  fiminre2  12091  supmul1  12112  supmul  12115  nnne0  12180  0mnnnnn0  12434  nn0negleid  12454  neglt  12931  rpgecl  12941  ge0p1rp  12944  ledivge1le  12984  mul2lt0rlt0  13015  mul2lt0rgt0  13016  mul2lt0bi  13019  prodge0rd  13020  max0sub  13116  reltxrnmnf  13263  infmrp1  13265  lincmb01cmp  13416  iccf1o  13417  xov1plusxeqvd  13419  elfz0fzfz0  13554  fz0fzelfz0  13555  elfzo0z  13622  fzofzim  13630  fzo1fzo0n0  13636  elfzodifsumelfzo  13652  ssfzoulel  13681  elfznelfzo  13693  muladdmodid  13835  modltm1p1mod  13848  addmodlteq  13871  expgt1  14025  ltexp2a  14091  expcan  14094  ltexp2  14095  leexp2  14096  leexp2a  14097  zzlesq  14131  expnlbnd2  14159  discr  14165  fi1uzind  14432  ccatsymb  14507  ccat2s1fvw  14563  swrdnd  14579  swrdnnn0nd  14581  swrdswrdlem  14628  swrdswrd  14629  repswswrd  14708  swrd2lsw  14877  2swrd2eqwrdeq  14878  leabs  15224  max0add  15235  absgt0  15250  rlimrege0  15504  iseraltlem2  15608  fsumrecl  15659  o1fsum  15738  cvgcmp  15741  cvgcmpce  15743  geomulcvg  15801  mertenslem2  15810  fprodle  15921  rpnnen2lem4  16144  p1modz1  16188  moddvds  16192  oddge22np1  16278  bitsfzolem  16363  bitsinv1lem  16370  sadcaddlem  16386  nn0rppwr  16490  nn0expgcd  16493  lcmgcdlem  16535  dvdsnprmd  16619  2mulprm  16622  isprm7  16637  qnumgt0  16679  modprm0  16735  qexpz  16831  prmreclem4  16849  4sqlem6  16873  prmgaplem7  16987  gzrngunit  21358  regsumfsum  21360  regsumsupp  21547  fvmptnn04ifd  22756  chfacffsupp  22759  chfacfscmul0  22761  chfacfscmulgsum  22763  chfacfpmmul0  22765  chfacfpmmulgsum  22767  prdsmet  24274  metustexhalf  24460  nlmvscnlem2  24589  nlmvscnlem1  24590  nmo0  24639  blcvx  24702  iihalf1cn  24842  evth  24874  lebnumlem1  24876  lebnumii  24881  htpycc  24895  pcohtpylem  24935  pcoass  24940  pcorevlem  24942  nmoleub2lem3  25031  ipcnlem2  25160  ipcnlem1  25161  rrxcph  25308  rrxmetlem  25323  rrxmet  25324  rrxdstprj1  25325  ehlbase  25331  minveclem3b  25344  minveclem6  25350  pjthlem1  25353  ovolicopnf  25441  ioorcl2  25489  volivth  25524  mbfposr  25569  i1fmulc  25620  itg1mulc  25621  itg1ge0a  25628  mbfi1flim  25640  itg2split  25666  itg2monolem1  25667  itg2monolem3  25669  itg2mono  25670  itg2cnlem2  25679  itgge0  25728  bddiblnc  25759  dvlip  25914  dvlipcn  25915  dveq0  25921  dv11cn  25922  dvlt0  25926  dvfsumge  25944  dgradd2  26190  plydivlem3  26219  mtest  26329  radcnvlem1  26338  radcnv0  26341  radcnvlt1  26343  radcnvle  26345  pserulm  26347  pserdvlem1  26353  pserdv  26355  abelthlem2  26358  abelthlem7  26364  pilem2  26378  pilem3  26379  coseq00topi  26427  tanabsge  26431  cosq34lt1  26452  tanord1  26462  tanord  26463  rplogcl  26529  logdivle  26547  logcnlem3  26569  logcnlem4  26570  dvloglem  26573  logtayl  26585  abscxp2  26618  cxplt  26619  cxple  26620  cxple2a  26624  cxpcn3lem  26673  abscxpbnd  26679  rtprmirr  26686  chordthmlem4  26761  chordthmlem5  26762  asinlem3  26797  atanre  26811  atanlogaddlem  26839  atanlogadd  26840  atanlogsublem  26841  atantan  26849  atans2  26857  efrlim  26895  efrlimOLD  26896  cxp2limlem  26902  cxp2lim  26903  cxploglim2  26905  divsqrtsumlem  26906  jensenlem2  26914  harmonicubnd  26936  fsumharmonic  26938  dmlogdmgm  26950  lgamgulmlem1  26955  lgamgulmlem2  26956  ftalem1  26999  ftalem2  27000  ftalem5  27003  vmacl  27044  chtwordi  27082  ppiwordi  27088  chtrpcl  27101  fsumfldivdiaglem  27115  fsumvma2  27141  chpval2  27145  chpchtsum  27146  chpub  27147  logfacbnd3  27150  logexprlim  27152  mersenne  27154  lgsdilem  27251  lgsne0  27262  gausslemma2dlem1a  27292  lgseisen  27306  lgsquadlem1  27307  lgsquadlem2  27308  2sqmod  27363  2sqnn0  27365  chebbnd1lem2  27397  chebbnd1lem3  27398  chebbnd1  27399  chtppilimlem1  27400  chtppilimlem2  27401  chtppilim  27402  chebbnd2  27404  chto1lb  27405  chpchtlim  27406  chpo1ub  27407  dchrisumlema  27415  dchrisumlem2  27417  dchrisumlem3  27418  dchrmusumlema  27420  dchrvmasumlem2  27425  dchrvmasumiflem1  27428  dchrisum0flblem1  27435  dchrisum0flblem2  27436  dchrisum0re  27440  dchrisum0lema  27441  dchrisum0  27447  dirith2  27455  mulog2sumlem1  27461  vmalogdivsum2  27465  log2sumbnd  27471  selberg2lem  27477  chpdifbndlem1  27480  chpdifbnd  27482  selberg3lem1  27484  pntrmax  27491  pntrsumo1  27492  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  pntpbnd1a  27512  pntpbnd1  27513  pntpbnd2  27514  pntlemg  27525  pntlemj  27530  pntlemk  27533  pntlem3  27536  pnt2  27540  pnt  27541  ostth2lem1  27545  padicabv  27557  padicabvcxp  27559  ostth2lem3  27562  ostth2lem4  27563  ostth3  27565  trgcgrg  28478  tgcgr4  28494  axsegconlem7  28886  axsegconlem10  28889  axcontlem2  28928  axcontlem4  28930  axcontlem7  28933  axcontlem10  28936  crctcshwlkn0lem3  29775  crctcshwlkn0  29784  clwlkclwwlklem2a2  29955  clwlkclwwlklem2a  29960  wwlksubclwwlk  30020  frgrogt3nreg  30359  friendshipgt3  30360  minvecolem5  30843  minvecolem6  30844  htthlem  30879  pjhthlem1  31353  sgnval2  32691  nndiffz1  32742  bcm1n  32751  fzo0opth  32761  expgt0b  32774  sgnneg  32791  sgnmul  32793  sgnsub  32795  nexple  32802  oexpled  32805  indf1o  32820  wrdt2ind  32908  cycpmrn  33098  cyc3conja  33112  ccfldextdgrr  33643  constrsslem  33707  constrresqrtcl  33743  constrsqrtcl  33745  cos9thpiminplylem1  33748  pnfneige0  33917  measinb  34187  eulerpartlems  34327  eulerpartlemgc  34329  ballotlemfc0  34460  ballotlemfcc  34461  ballotlemodife  34465  signsply0  34518  signslema  34529  signsvtp  34550  itgexpif  34573  breprexplemc  34599  circlemeth  34607  logdivsqrle  34617  0nn0m1nnn0  35085  cvmliftlem2  35258  dnibndlem9  36459  unbdqndv2lem2  36483  knoppndvlem1  36485  knoppndvlem2  36486  knoppndvlem7  36491  knoppndvlem11  36495  knoppndvlem14  36498  knoppndvlem15  36499  knoppndvlem17  36501  knoppndvlem19  36503  knoppndvlem20  36504  bj-pinftynminfty  37200  poimirlem10  37609  poimirlem11  37610  poimirlem24  37623  poimirlem29  37628  poimirlem31  37630  poimirlem32  37631  poimir  37632  mblfinlem2  37637  ftc1anclem7  37678  ftc1anclem8  37679  ftc1anc  37680  areacirclem1  37687  areacirclem4  37690  areacirc  37692  geomcau  37738  isbnd3b  37764  prdsbnd  37772  bfp  37803  rrnequiv  37814  resdvopclptsd  42001  lcmineqlem2  42003  lcmineqlem3  42004  lcmineqlem10  42011  lcmineqlem12  42013  lcmineqlem23  42024  3lexlogpow5ineq1  42027  3lexlogpow5ineq2  42028  3lexlogpow5ineq4  42029  3lexlogpow5ineq3  42030  3lexlogpow2ineq2  42032  3lexlogpow5ineq5  42033  aks4d1lem1  42035  dvrelog2  42037  dvrelog3  42038  dvrelog2b  42039  0nonelalab  42040  dvrelogpow2b  42041  aks4d1p1p3  42042  aks4d1p1p2  42043  aks4d1p1p4  42044  aks4d1p1p6  42046  aks4d1p1p7  42047  aks4d1p1p5  42048  aks4d1p1  42049  aks4d1p2  42050  aks4d1p3  42051  aks4d1p5  42053  aks4d1p6  42054  aks4d1p7d1  42055  aks4d1p7  42056  aks4d1p8d2  42058  aks4d1p8d3  42059  aks4d1p8  42060  aks4d1p9  42061  posbezout  42073  primrootspoweq0  42079  aks6d1c1  42089  hashscontpow1  42094  aks6d1c2lem4  42100  aks6d1c5lem2  42111  deg1gprod  42113  2np3bcnp1  42117  2ap1caineq  42118  sticksstones7  42125  sticksstones10  42128  sticksstones12a  42130  sticksstones12  42131  sticksstones22  42141  aks6d1c6lem3  42145  bcled  42151  bcle2d  42152  aks6d1c7lem1  42153  aks6d1c7lem2  42154  aks6d1c7  42157  aks5lem6  42165  unitscyglem5  42172  aks5lem8  42174  sn-1ne2  42238  oexpreposd  42295  posqsqznn  42309  redvmptabs  42333  readvrec  42335  re1m1e0m0  42370  re0m0e0  42375  remul01  42380  sn-remul0ord  42381  remulneg2d  42388  sn-addlt0d  42431  sn-addgt0d  42432  renegmulnnass  42438  zmulcomlem  42440  mulgt0con1dlem  42442  sn-mulgt1d  42452  mulltgt0d  42455  mullt0b2d  42457  sn-mullt0d  42458  sn-msqgt0d  42459  fimgmcyc  42507  dffltz  42607  3cubeslem1  42657  irrapxlem1  42795  irrapxlem2  42796  irrapxlem3  42797  irrapxlem4  42798  pellexlem6  42807  pell14qrgt0  42832  pell1qrgaplem  42846  pellfundex  42859  pellfundrp  42861  monotoddzzfi  42915  jm2.24  42936  jm2.23  42969  jm2.26lem3  42974  jm3.1lem3  42992  sqrtcvallem1  43604  reabsifneg  43605  reabsifpos  43607  sqrtcval  43614  k0004ss2  44125  imo72b2lem1  44142  dvgrat  44285  hashnzfz2  44294  binomcxplemnn0  44322  binomcxplemnotnn0  44329  divlt0gt0d  45268  upbdrech2  45290  xralrple2  45334  xralrple3  45354  reclt0d  45367  reclt0  45371  xrpnf  45465  fsumnncl  45554  fsumsupp0  45560  sumnnodd  45612  lptre2pt  45622  limsupubuz  45695  liminfresre  45761  liminf0  45775  dvmptconst  45897  dvdivbd  45905  dvcosax  45908  dvbdfbdioolem1  45910  dvbdfbdioolem2  45911  ioodvbdlimc1lem1  45913  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  dvxpaek  45922  dvnxpaek  45924  volioc  45954  volico  45965  stoweidlem1  45983  stoweidlem7  45989  stoweidlem11  45993  stoweidlem25  46007  stoweidlem26  46008  stoweidlem34  46016  stoweidlem36  46018  stoweidlem41  46023  stoweidlem42  46024  stoweidlem44  46026  stoweidlem45  46027  wallispilem3  46049  wallispilem4  46050  wallispi  46052  stirlinglem3  46058  stirlinglem5  46060  stirlinglem6  46061  stirlinglem7  46062  stirlinglem10  46065  stirlinglem11  46066  stirlinglem12  46067  dirkeritg  46084  dirkercncflem2  46086  fourierdlem9  46098  fourierdlem11  46100  fourierdlem12  46101  fourierdlem14  46103  fourierdlem15  46104  fourierdlem19  46108  fourierdlem24  46113  fourierdlem28  46117  fourierdlem30  46119  fourierdlem40  46129  fourierdlem41  46130  fourierdlem43  46132  fourierdlem44  46133  fourierdlem47  46135  fourierdlem50  46138  fourierdlem51  46139  fourierdlem57  46145  fourierdlem60  46148  fourierdlem61  46149  fourierdlem66  46154  fourierdlem68  46156  fourierdlem73  46161  fourierdlem74  46162  fourierdlem75  46163  fourierdlem78  46166  fourierdlem79  46167  fourierdlem83  46171  fourierdlem88  46176  fourierdlem92  46180  fourierdlem93  46181  fourierdlem97  46185  fourierdlem103  46191  fourierdlem104  46192  fourierdlem109  46197  fourierdlem111  46199  sqwvfoura  46210  sqwvfourb  46211  fourierswlem  46212  fouriersw  46213  elaa2lem  46215  etransclem4  46220  etransclem18  46234  etransclem19  46235  etransclem23  46239  etransclem27  46243  etransclem31  46247  etransclem32  46248  etransclem35  46251  etransclem41  46257  etransclem46  46262  etransclem48  46264  rrxtopnfi  46269  qndenserrnbllem  46276  salgencntex  46325  sge0tsms  46362  sge0isum  46409  volicorecl  46528  hoiprodcl  46529  ovnlerp  46544  ovnsubaddlem1  46552  hoiprodcl3  46562  volicore  46563  hoidmvcl  46564  hoidmvlelem1  46577  hoidmvlelem2  46578  hoidmvlelem3  46579  ovnhoi  46585  hoiqssbllem2  46605  volicorege0  46619  vonhoire  46654  pimrecltpos  46690  pimrecltneg  46706  smfmbfcex  46742  nsssmfmbflem  46760  smfrec  46771  smfmullem3  46775  smfdivdmmbl  46820  sharhght  46847  et-sqrtnegnre  46855  ormkglobd  46857  natglobalincr  46859  upwordnul  46862  zm1nn  47287  eluzge0nn0  47297  elfz2z  47300  2ffzoeq  47312  m1modmmod  47343  modm1p1ne  47355  iccpartigtl  47408  iccpartgt  47412  requad01  47606  requad1  47607  requad2  47608  stgrusgra  47944  gpgedgvtx1  48047  expnegico01  48504  regt1loggt0  48522  refdivmptf  48528  elbigolo1  48543  rege1logbrege0  48544  fllog2  48554  dignn0flhalflem1  48601  eenglngeehlnmlem2  48724  line2  48738  line2xlem  48739  line2x  48740  line2y  48741  itsclc0yqsol  48750  2itscp  48767  inlinecirc02plem  48772  amgmwlem  49788