Theorem 0red 11138

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11028  0cc0 11029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11087  ax-addrcl 11090  ax-rnegex 11100  ax-cnre 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812  df-rex 3063

This theorem is referenced by:  gt0ne0  11606  add20  11653  subge0  11654  lesub0  11658  mulge0  11659  msqgt0  11661  msqge0  11662  gt0ne0d  11705  addgt0d  11716  sublt0d  11767  prodgt0  11993  mulgt1  12008  lt2msq1  12031  fiminre2  12095  supmul1  12116  supmul  12119  nnne0  12202  0mnnnnn0  12460  nn0negleid  12480  neglt  12953  rpgecl  12963  ge0p1rp  12966  ledivge1le  13006  mul2lt0rlt0  13037  mul2lt0rgt0  13038  mul2lt0bi  13041  prodge0rd  13042  max0sub  13139  reltxrnmnf  13286  infmrp1  13288  lincmb01cmp  13439  iccf1o  13440  xov1plusxeqvd  13442  elfz0fzfz0  13578  fz0fzelfz0  13579  elfzo0z  13647  fzofzim  13655  fzo1fzo0n0  13661  elfzodifsumelfzo  13677  ssfzoulel  13706  elfznelfzo  13719  muladdmodid  13863  modltm1p1mod  13876  addmodlteq  13899  expgt1  14053  ltexp2a  14119  expcan  14122  ltexp2  14123  leexp2  14124  leexp2a  14125  zzlesq  14159  expnlbnd2  14187  discr  14193  fi1uzind  14460  ccatsymb  14536  ccat2s1fvw  14592  swrdnd  14608  swrdnnn0nd  14610  swrdswrdlem  14657  swrdswrd  14658  repswswrd  14737  swrd2lsw  14905  2swrd2eqwrdeq  14906  leabs  15252  max0add  15263  absgt0  15278  rlimrege0  15532  iseraltlem2  15636  fsumrecl  15687  o1fsum  15767  cvgcmp  15770  cvgcmpce  15772  geomulcvg  15832  mertenslem2  15841  fprodle  15952  rpnnen2lem4  16175  p1modz1  16219  moddvds  16223  oddge22np1  16309  bitsfzolem  16394  bitsinv1lem  16401  sadcaddlem  16417  nn0rppwr  16521  nn0expgcd  16524  lcmgcdlem  16566  dvdsnprmd  16650  2mulprm  16653  isprm7  16669  qnumgt0  16711  modprm0  16767  qexpz  16863  prmreclem4  16881  4sqlem6  16905  prmgaplem7  17019  gzrngunit  21423  regsumfsum  21425  regsumsupp  21612  fvmptnn04ifd  22828  chfacffsupp  22831  chfacfscmul0  22833  chfacfscmulgsum  22835  chfacfpmmul0  22837  chfacfpmmulgsum  22839  prdsmet  24345  metustexhalf  24531  nlmvscnlem2  24660  nlmvscnlem1  24661  nmo0  24710  blcvx  24773  iihalf1cn  24909  evth  24936  lebnumlem1  24938  lebnumii  24943  htpycc  24957  pcohtpylem  24996  pcoass  25001  pcorevlem  25003  nmoleub2lem3  25092  ipcnlem2  25221  ipcnlem1  25222  rrxcph  25369  rrxmetlem  25384  rrxmet  25385  rrxdstprj1  25386  ehlbase  25392  minveclem3b  25405  minveclem6  25411  pjthlem1  25414  ovolicopnf  25501  ioorcl2  25549  volivth  25584  mbfposr  25629  i1fmulc  25680  itg1mulc  25681  itg1ge0a  25688  mbfi1flim  25700  itg2split  25726  itg2monolem1  25727  itg2monolem3  25729  itg2mono  25730  itg2cnlem2  25739  itgge0  25788  bddiblnc  25819  dvlip  25970  dvlipcn  25971  dveq0  25977  dv11cn  25978  dvlt0  25982  dvfsumge  25999  dgradd2  26243  plydivlem3  26272  mtest  26382  radcnvlem1  26391  radcnv0  26394  radcnvlt1  26396  radcnvle  26398  pserulm  26400  pserdvlem1  26405  pserdv  26407  abelthlem2  26410  abelthlem7  26416  pilem2  26430  pilem3  26431  coseq00topi  26479  tanabsge  26483  cosq34lt1  26504  tanord1  26514  tanord  26515  rplogcl  26581  logdivle  26599  logcnlem3  26621  logcnlem4  26622  dvloglem  26625  logtayl  26637  abscxp2  26670  cxplt  26671  cxple  26672  cxple2a  26676  cxpcn3lem  26724  abscxpbnd  26730  rtprmirr  26737  chordthmlem4  26812  chordthmlem5  26813  asinlem3  26848  atanre  26862  atanlogaddlem  26890  atanlogadd  26891  atanlogsublem  26892  atantan  26900  atans2  26908  efrlim  26946  efrlimOLD  26947  cxp2limlem  26953  cxp2lim  26954  cxploglim2  26956  divsqrtsumlem  26957  jensenlem2  26965  harmonicubnd  26987  fsumharmonic  26989  dmlogdmgm  27001  lgamgulmlem1  27006  lgamgulmlem2  27007  ftalem1  27050  ftalem2  27051  ftalem5  27054  vmacl  27095  chtwordi  27133  ppiwordi  27139  chtrpcl  27152  fsumfldivdiaglem  27166  fsumvma2  27191  chpval2  27195  chpchtsum  27196  chpub  27197  logfacbnd3  27200  logexprlim  27202  mersenne  27204  lgsdilem  27301  lgsne0  27312  gausslemma2dlem1a  27342  lgseisen  27356  lgsquadlem1  27357  lgsquadlem2  27358  2sqmod  27413  2sqnn0  27415  chebbnd1lem2  27447  chebbnd1lem3  27448  chebbnd1  27449  chtppilimlem1  27450  chtppilimlem2  27451  chtppilim  27452  chebbnd2  27454  chto1lb  27455  chpchtlim  27456  chpo1ub  27457  dchrisumlema  27465  dchrisumlem2  27467  dchrisumlem3  27468  dchrmusumlema  27470  dchrvmasumlem2  27475  dchrvmasumiflem1  27478  dchrisum0flblem1  27485  dchrisum0flblem2  27486  dchrisum0re  27490  dchrisum0lema  27491  dchrisum0  27497  dirith2  27505  mulog2sumlem1  27511  vmalogdivsum2  27515  log2sumbnd  27521  selberg2lem  27527  chpdifbndlem1  27530  chpdifbnd  27532  selberg3lem1  27534  pntrmax  27541  pntrsumo1  27542  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  pntpbnd1a  27562  pntpbnd1  27563  pntpbnd2  27564  pntlemg  27575  pntlemj  27580  pntlemk  27583  pntlem3  27586  pnt2  27590  pnt  27591  ostth2lem1  27595  padicabv  27607  padicabvcxp  27609  ostth2lem3  27612  ostth2lem4  27613  ostth3  27615  trgcgrg  28597  tgcgr4  28613  axsegconlem7  29006  axsegconlem10  29009  axcontlem2  29048  axcontlem4  29050  axcontlem7  29053  axcontlem10  29056  crctcshwlkn0lem3  29895  crctcshwlkn0  29904  clwlkclwwlklem2a2  30078  clwlkclwwlklem2a  30083  wwlksubclwwlk  30143  frgrogt3nreg  30482  friendshipgt3  30483  minvecolem5  30967  minvecolem6  30968  htthlem  31003  pjhthlem1  31477  sgnval2  32823  nndiffz1  32874  bcm1n  32883  fzo0opth  32891  expgt0b  32905  sgnneg  32921  sgnmul  32923  sgnsub  32925  nexple  32932  oexpled  32935  indf1o  32939  wrdt2ind  33028  cycpmrn  33219  cyc3conja  33233  ccfldextdgrr  33832  constrsslem  33901  constrresqrtcl  33937  constrsqrtcl  33939  cos9thpiminplylem1  33942  pnfneige0  34111  measinb  34381  eulerpartlems  34520  eulerpartlemgc  34522  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemodife  34658  signsply0  34711  signslema  34722  signsvtp  34743  itgexpif  34766  breprexplemc  34792  circlemeth  34800  logdivsqrle  34810  0nn0m1nnn0  35311  cvmliftlem2  35484  dnibndlem9  36762  unbdqndv2lem2  36786  knoppndvlem1  36788  knoppndvlem2  36789  knoppndvlem7  36794  knoppndvlem11  36798  knoppndvlem14  36801  knoppndvlem15  36802  knoppndvlem17  36804  knoppndvlem19  36806  knoppndvlem20  36807  bj-pinftynminfty  37557  poimirlem10  37965  poimirlem11  37966  poimirlem24  37979  poimirlem29  37984  poimirlem31  37986  poimirlem32  37987  poimir  37988  mblfinlem2  37993  ftc1anclem7  38034  ftc1anclem8  38035  ftc1anc  38036  areacirclem1  38043  areacirclem4  38046  areacirc  38048  geomcau  38094  isbnd3b  38120  prdsbnd  38128  bfp  38159  rrnequiv  38170  resdvopclptsd  42481  lcmineqlem2  42483  lcmineqlem3  42484  lcmineqlem10  42491  lcmineqlem12  42493  lcmineqlem23  42504  3lexlogpow5ineq1  42507  3lexlogpow5ineq2  42508  3lexlogpow5ineq4  42509  3lexlogpow5ineq3  42510  3lexlogpow2ineq2  42512  3lexlogpow5ineq5  42513  aks4d1lem1  42515  dvrelog2  42517  dvrelog3  42518  dvrelog2b  42519  0nonelalab  42520  dvrelogpow2b  42521  aks4d1p1p3  42522  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p1p6  42526  aks4d1p1p7  42527  aks4d1p1p5  42528  aks4d1p1  42529  aks4d1p2  42530  aks4d1p3  42531  aks4d1p5  42533  aks4d1p6  42534  aks4d1p7d1  42535  aks4d1p7  42536  aks4d1p8d2  42538  aks4d1p8d3  42539  aks4d1p8  42540  aks4d1p9  42541  posbezout  42553  primrootspoweq0  42559  aks6d1c1  42569  hashscontpow1  42574  aks6d1c2lem4  42580  aks6d1c5lem2  42591  deg1gprod  42593  2np3bcnp1  42597  2ap1caineq  42598  sticksstones7  42605  sticksstones10  42608  sticksstones12a  42610  sticksstones12  42611  sticksstones22  42621  aks6d1c6lem3  42625  bcled  42631  bcle2d  42632  aks6d1c7lem1  42633  aks6d1c7lem2  42634  aks6d1c7  42637  aks5lem6  42645  unitscyglem5  42652  aks5lem8  42654  sn-1ne2  42717  oexpreposd  42768  posqsqznn  42782  redvmptabs  42806  readvrec  42808  re1m1e0m0  42843  re0m0e0  42848  remul01  42853  sn-remul0ord  42854  remulneg2d  42861  rediveq0d  42895  sn-rediv0d  42899  sn-addlt0d  42917  sn-addgt0d  42918  renegmulnnass  42924  zmulcomlem  42926  mulgt0con1dlem  42928  sn-mulgt1d  42938  mulltgt0d  42941  mullt0b2d  42943  sn-mullt0d  42944  sn-msqgt0d  42945  fimgmcyc  42993  dffltz  43081  3cubeslem1  43130  irrapxlem1  43268  irrapxlem2  43269  irrapxlem3  43270  irrapxlem4  43271  pellexlem6  43280  pell14qrgt0  43305  pell1qrgaplem  43319  pellfundex  43332  pellfundrp  43334  monotoddzzfi  43388  jm2.24  43409  jm2.23  43442  jm2.26lem3  43447  jm3.1lem3  43465  sqrtcvallem1  44076  reabsifneg  44077  reabsifpos  44079  sqrtcval  44086  k0004ss2  44597  imo72b2lem1  44614  dvgrat  44757  hashnzfz2  44766  binomcxplemnn0  44794  binomcxplemnotnn0  44801  divlt0gt0d  45737  upbdrech2  45759  xralrple2  45802  xralrple3  45821  reclt0d  45834  reclt0  45838  xrpnf  45931  fsumnncl  46020  fsumsupp0  46026  sumnnodd  46078  lptre2pt  46086  limsupubuz  46159  liminfresre  46225  liminf0  46239  dvmptconst  46361  dvdivbd  46369  dvcosax  46372  dvbdfbdioolem1  46374  dvbdfbdioolem2  46375  ioodvbdlimc1lem1  46377  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvxpaek  46386  dvnxpaek  46388  volioc  46418  volico  46429  stoweidlem1  46447  stoweidlem7  46453  stoweidlem11  46457  stoweidlem25  46471  stoweidlem26  46472  stoweidlem34  46480  stoweidlem36  46482  stoweidlem41  46487  stoweidlem42  46488  stoweidlem44  46490  stoweidlem45  46491  wallispilem3  46513  wallispilem4  46514  wallispi  46516  stirlinglem3  46522  stirlinglem5  46524  stirlinglem6  46525  stirlinglem7  46526  stirlinglem10  46529  stirlinglem11  46530  stirlinglem12  46531  dirkeritg  46548  dirkercncflem2  46550  fourierdlem9  46562  fourierdlem11  46564  fourierdlem12  46565  fourierdlem14  46567  fourierdlem15  46568  fourierdlem19  46572  fourierdlem24  46577  fourierdlem28  46581  fourierdlem30  46583  fourierdlem40  46593  fourierdlem41  46594  fourierdlem43  46596  fourierdlem44  46597  fourierdlem47  46599  fourierdlem50  46602  fourierdlem51  46603  fourierdlem57  46609  fourierdlem60  46612  fourierdlem61  46613  fourierdlem66  46618  fourierdlem68  46620  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem78  46630  fourierdlem79  46631  fourierdlem83  46635  fourierdlem88  46640  fourierdlem92  46644  fourierdlem93  46645  fourierdlem97  46649  fourierdlem103  46655  fourierdlem104  46656  fourierdlem109  46661  fourierdlem111  46663  sqwvfoura  46674  sqwvfourb  46675  fourierswlem  46676  fouriersw  46677  elaa2lem  46679  etransclem4  46684  etransclem18  46698  etransclem19  46699  etransclem23  46703  etransclem27  46707  etransclem31  46711  etransclem32  46712  etransclem35  46715  etransclem41  46721  etransclem46  46726  etransclem48  46728  rrxtopnfi  46733  qndenserrnbllem  46740  salgencntex  46789  sge0tsms  46826  sge0isum  46873  volicorecl  46992  hoiprodcl  46993  ovnlerp  47008  ovnsubaddlem1  47016  hoiprodcl3  47026  volicore  47027  hoidmvcl  47028  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  ovnhoi  47049  hoiqssbllem2  47069  volicorege0  47083  vonhoire  47118  pimrecltpos  47154  pimrecltneg  47170  smfmbfcex  47206  nsssmfmbflem  47224  smfrec  47235  smfmullem3  47239  smfdivdmmbl  47284  sharhght  47311  et-sqrtnegnre  47319  ormkglobd  47321  natglobalincr  47323  chnsubseqwl  47325  zm1nn  47762  eluzge0nn0  47772  elfz2z  47775  2ffzoeq  47788  m1modmmod  47824  modm1p1ne  47836  muldvdsfacm1  47847  iccpartigtl  47895  iccpartgt  47899  nprmdvdsfacm1lem4  48098  requad01  48109  requad1  48110  requad2  48111  stgrusgra  48447  gpgedgvtx1  48550  expnegico01  49006  regt1loggt0  49024  refdivmptf  49030  elbigolo1  49045  rege1logbrege0  49046  fllog2  49056  dignn0flhalflem1  49103  eenglngeehlnmlem2  49226  line2  49240  line2xlem  49241  line2x  49242  line2y  49243  itsclc0yqsol  49252  2itscp  49269  inlinecirc02plem  49274  amgmwlem  50289