Theorem 0red 9618

Description: is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
0red

Proof of Theorem 0red

Step	Hyp	Ref	Expression
1		0re 9617	. 2
2	1	a1i 11	1

Syntax hints:  ->wi 4  e.wcel 1818  cr 9512  0cc0 9513

This theorem is referenced by:  gt0ne0  10042  add20  10089  subge0  10090  lesub0  10094  mulge0  10095  msqgt0  10098  msqge0  10099  addgt0d  10152  prodgt0  10412  prodge0  10414  lt2msq1  10453  supmul1  10533  supmul  10536  0mnnnnn0  10853  rpgecl  11274  ge0p1rp  11277  max0sub  11424  iccf1o  11693  xov1plusxeqvd  11695  elfz1b  11777  elfz0fzfz0  11808  fz0fzelfz0  11809  fzo1fzo0n0  11864  elfzo0z  11865  fzofzim  11869  elfzodifsumelfzo  11882  ssfzoulel  11906  elfznelfzo  11915  modltm1p1mod  12039  expgt1  12204  ltexp2a  12217  expcan  12218  ltexp2  12219  leexp2  12220  leexp2a  12221  expnlbnd2  12297  discr  12303  brfi1uzind  12532  ccatsymb  12600  swrdnd  12657  swrdvalodm2  12664  swrdswrdlem  12684  swrdswrd  12685  swrdccatin2  12712  swrdccatin12lem3  12715  repswswrd  12756  swrd2lsw  12890  2swrd2eqwrdeq  12891  leabs  13132  max0add  13143  absgt0  13157  rlimrege0  13402  iseraltlem2  13505  fsumrecl  13556  o1fsum  13627  cvgcmp  13630  cvgcmpce  13632  geomulcvg  13685  mertenslem2  13694  rpnnen2lem4  13951  moddvds  13993  bitsfzolem  14084  bitsinv1lem  14091  sadcaddlem  14107  qnumgt0  14283  modprm0  14330  qexpz  14420  prmreclem4  14437  4sqlem6  14461  gzrngunit  18483  regsumsupp  18658  fvmptnn04ifd  19354  chfacffsupp  19357  chfacfscmul0  19359  chfacfscmulgsum  19361  chfacfpmmul0  19363  chfacfpmmulgsum  19365  prdsmet  20873  metustexhalf  21067  nlmvscnlem2  21194  nlmvscnlem1  21195  nmo0  21242  evth  21459  lebnumlem1  21461  lebnumii  21466  htpycc  21480  pcohtpylem  21519  pcoass  21524  pcorevlem  21526  nmoleub2lem3  21598  ipcnlem2  21684  ipcnlem1  21685  rrxcph  21824  rrxmetlem  21834  rrxmet  21835  rrxdstprj1  21836  ehlbase  21838  minveclem3b  21843  minveclem6  21849  pjthlem1  21852  ovolicopnf  21935  ioorcl2  21981  volivth  22016  mbfposr  22059  i1fmulc  22110  itg1mulc  22111  itg1ge0a  22118  mbfi1flim  22130  itg2split  22156  itg2monolem1  22157  itg2monolem3  22159  itg2mono  22160  itg2cnlem2  22169  itgge0  22217  dvlip  22394  dvlipcn  22395  dveq0  22401  dv11cn  22402  dvlt0  22406  dvfsumge  22423  dgradd2  22665  plydivlem3  22691  mtest  22799  radcnvlem1  22808  radcnv0  22811  radcnvlt1  22813  radcnvle  22815  pserulm  22817  pserdvlem1  22822  pserdv  22824  abelthlem2  22827  abelthlem7  22833  pilem2  22847  coseq00topi  22895  tanabsge  22899  tanord1  22924  tanord  22925  logne0  22987  rplogcl  22989  logdivle  23007  logcnlem3  23025  logcnlem4  23026  dvloglem  23029  logtayl  23041  abscxp2  23074  cxplt  23075  cxple  23076  cxple2a  23080  cxpcn3lem  23121  abscxpbnd  23127  chordthmlem5  23167  asinlem3  23202  atanre  23216  atanlogaddlem  23244  atanlogadd  23245  atanlogsublem  23246  atantan  23254  atans2  23262  efrlim  23299  cxp2limlem  23305  cxp2lim  23306  cxploglim2  23308  divsqrtsumlem  23309  jensenlem2  23317  harmonicubnd  23339  fsumharmonic  23341  ftalem1  23346  ftalem2  23347  ftalem5  23350  vmacl  23392  chtwordi  23430  ppiwordi  23436  chtrpcl  23449  fsumfldivdiaglem  23465  fsumvma2  23489  chpval2  23493  chpchtsum  23494  chpub  23495  logfacbnd3  23498  logexprlim  23500  mersenne  23502  lgslem4  23574  lgsdilem  23597  lgsne0  23608  lgseisen  23628  lgsquadlem1  23629  lgsquadlem2  23630  chebbnd1lem2  23655  chebbnd1lem3  23656  chebbnd1  23657  chtppilimlem1  23658  chtppilimlem2  23659  chtppilim  23660  chebbnd2  23662  chto1lb  23663  chpchtlim  23664  chpo1ub  23665  dchrisumlema  23673  dchrisumlem2  23675  dchrisumlem3  23676  dchrmusumlema  23678  dchrvmasumlem2  23683  dchrvmasumiflem1  23686  dchrisum0flblem1  23693  dchrisum0flblem2  23694  dchrisum0re  23698  dchrisum0lema  23699  dchrisum0  23705  dirith2  23713  mulog2sumlem1  23719  vmalogdivsum2  23723  log2sumbnd  23729  selberg2lem  23735  chpdifbndlem1  23738  chpdifbndlem2  23739  chpdifbnd  23740  selberg3lem1  23742  pntrmax  23749  pntrsumo1  23750  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  pntpbnd1a  23770  pntpbnd1  23771  pntpbnd2  23772  pntlemg  23783  pntlemj  23788  pntlemk  23791  pntlem3  23794  pntleml  23796  pnt2  23798  pnt  23799  ostth2lem1  23803  padicabv  23815  padicabvcxp  23817  ostth2lem3  23820  ostth2lem4  23821  ostth3  23823  trgcgrg  23906  axsegconlem7  24226  axsegconlem10  24229  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  axcontlem10  24276  nvnencycllem  24643  clwwlkn0  24774  clwlkisclwwlklem2a2  24780  clwlkisclwwlklem2a  24785  wwlksubclwwlk  24804  frgraogt3nreg  25120  friendshipgt3  25121  minvecolem5  25797  minvecolem6  25798  htthlem  25834  pjhthlem1  26309  mul2lt0rlt0  27565  mul2lt0rgt0  27566  mul2lt0bi  27569  nndiffz1  27596  bcm1n  27600  2sqmod  27636  regsumfsum  27772  pnfneige0  27933  nexple  28005  indf1o  28037  measinb  28192  eulerpartlems  28299  eulerpartlemgc  28301  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemodife  28436  sgnneg  28479  sgnmul  28481  sgnsub  28483  signsply0  28508  signslema  28519  signsvtp  28540  signshf  28545  dmlogdmgm  28566  lgamgulmlem1  28571  lgamgulmlem2  28572  cvmliftlem2  28731  bddiblnc  30085  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  areacirclem1  30107  areacirclem4  30110  areacirc  30112  geomcau  30252  isbnd3b  30281  prdsbnd  30289  bfp  30320  rrnequiv  30331  irrapxlem1  30758  irrapxlem2  30759  irrapxlem3  30760  irrapxlem4  30761  pellexlem6  30770  pell14qrgt0  30795  pell1qrgaplem  30809  pellfundex  30822  pellfundrp  30824  monotoddzzfi  30878  jm2.24  30901  jm2.23  30938  jm2.26lem3  30943  jm3.1lem3  30961  isprm7  31192  dvgrat  31193  lcmgcdlem  31212  hashnzfz2  31226  binomcxplemnn0  31254  binomcxplemnotnn0  31261  neglt  31467  divlt0gt0d  31469  sublt0d  31495  upbdrech2  31508  fsumnncl  31572  fprodle  31604  sumnnodd  31636  lptre2pt  31646  dvmptconst  31710  dvdivbd  31720  dvcosax  31723  dvbdfbdioolem1  31725  dvbdfbdioolem2  31726  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvxpaek  31737  dvnxpaek  31739  volioc  31771  stoweidlem1  31783  stoweidlem7  31789  stoweidlem11  31793  stoweidlem25  31807  stoweidlem26  31808  stoweidlem34  31816  stoweidlem36  31818  stoweidlem41  31823  stoweidlem42  31824  stoweidlem44  31826  stoweidlem45  31827  wallispilem3  31849  wallispilem4  31850  wallispi  31852  stirlinglem3  31858  stirlinglem5  31860  stirlinglem6  31861  stirlinglem7  31862  stirlinglem10  31865  stirlinglem11  31866  stirlinglem12  31867  dirkeritg  31884  dirkercncflem2  31886  fourierdlem9  31898  fourierdlem11  31900  fourierdlem12  31901  fourierdlem14  31903  fourierdlem15  31904  fourierdlem19  31908  fourierdlem24  31913  fourierdlem28  31917  fourierdlem30  31919  fourierdlem40  31929  fourierdlem41  31930  fourierdlem43  31932  fourierdlem44  31933  fourierdlem47  31936  fourierdlem50  31939  fourierdlem51  31940  fourierdlem57  31946  fourierdlem60  31949  fourierdlem61  31950  fourierdlem66  31955  fourierdlem68  31957  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem78  31967  fourierdlem79  31968  fourierdlem83  31972  fourierdlem88  31977  fourierdlem92  31981  fourierdlem93  31982  fourierdlem97  31986  fourierdlem103  31992  fourierdlem104  31993  fourierdlem109  31998  fourierdlem111  32000  sqwvfoura  32011  sqwvfourb  32012  fourierswlem  32013  fouriersw  32014  elaa2lem  32016  etransclem4  32021  etransclem18  32035  etransclem19  32036  etransclem23  32040  etransclem27  32044  etransclem31  32048  etransclem32  32049  etransclem35  32052  etransclem41  32058  etransclem46  32063  etransclem48  32065  sharhght  32082  zm1nn  32325  eluzge0nn0  32329  elfz2z  32331  2ffzoeq  32341  bj-pinftynminfty  34630  imo72b2lem1  37988

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299