Theorem 1red 9632

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

Assertion

Ref	Expression
1red

Proof of Theorem 1red

Step	Hyp	Ref	Expression
1		1re 9616	. 2
2	1	a1i 11	1

Syntax hints:  ->wi 4  e.wcel 1818  cr 9512  1c1 9514

This theorem is referenced by:  recgt0  10411  ltrec  10451  nn0p1gt0  10850  nn0ge2m1nn  10886  suprzcl  10967  qbtwnre  11427  iccf1o  11693  xov1plusxeqvd  11695  fznatpl1  11763  elfz1b  11777  fzonn0p1p1  11894  elfzom1p1elfzo  11895  elfznelfzo  11915  elfznelfzob  11916  fladdz  11958  flhalf  11962  ltdifltdiv  11966  modltm1p1mod  12039  ltexp2a  12217  expcan  12218  ltexp2  12219  leexp2  12220  leexp2a  12221  leexp2r  12223  nnlesq  12271  bernneq3  12294  expnbnd  12295  expnlbnd2  12297  fzsdom2  12486  wrdlenge2n0  12577  lswccatn0lsw  12607  swrdn0  12655  swrd2lsw  12890  2swrd2eqwrdeq  12891  rddif  13173  reccn2  13419  rlimo1  13439  o1fsum  13627  abscvgcvg  13633  climcndslem1  13661  flo1  13666  harmonic  13670  geomulcvg  13685  fprodrecl  13760  efcllem  13813  efgt1  13851  tanhlt1  13895  sinltx  13924  eirrlem  13937  bitsfzolem  14084  bitsfzo  14085  bitsmod  14086  bitscmp  14088  bitsinv1lem  14091  smuval2  14132  prmind2  14228  isprm5  14253  divdenle  14282  zsqrtelqelz  14291  fermltl  14314  odzdvds  14322  modprm0  14330  iserodd  14359  pcfaclem  14417  prmreclem1  14434  4sqlem11  14473  4sqlem12  14474  ramub1lem1  14544  2expltfac  14577  pgpfaclem2  17133  znidomb  18600  chfacfisf  19355  chfacfisfcpmat  19356  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  nrginvrcnlem  21199  nmoid  21249  xrsmopn  21317  metnrmlem1a  21362  iccpnfhmeo  21445  htpycc  21480  pcohtpylem  21519  pcoass  21524  pcorevlem  21526  nmhmcn  21603  cncmet  21761  ovoliunlem1  21913  dyadmaxlem  22006  vitalilem2  22018  mbfi1fseqlem6  22127  itg2mulc  22154  itg2monolem1  22157  itg2monolem3  22159  dveflem  22380  mvth  22393  dvlipcn  22395  lhop1lem  22414  dvfsumlem1  22427  dvfsumlem2  22428  dvfsumlem3  22429  dvfsumlem4  22430  dvfsum2  22435  fta1glem2  22567  plyeq0lem  22607  fta1lem  22703  vieta1lem2  22707  aalioulem3  22730  aalioulem4  22731  radcnvlem1  22808  radcnvlem2  22809  dvradcnv  22816  abelthlem2  22827  abelthlem5  22830  abelthlem7  22833  abelth2  22837  cosne0  22917  rplogcl  22989  logdivlti  23005  logno1  23017  advlog  23035  logtayllem  23040  cxplt  23075  cxple  23076  cxpaddlelem  23125  cxpaddle  23126  isosctrlem1  23152  isosctrlem2  23153  heron  23169  atanlogaddlem  23244  bndatandm  23260  leibpi  23273  log2tlbnd  23276  birthdaylem3  23283  rlimcnp  23295  rlimcnp2  23296  efrlim  23299  cxp2limlem  23305  divsqrtsumo1  23313  jensenlem2  23317  logdiflbnd  23324  fsumharmonic  23341  wilthlem2  23343  ftalem2  23347  basellem9  23362  vma1  23440  ppieq0  23450  mumullem2  23454  fsumfldivdiaglem  23465  chpeq0  23483  chtub  23487  chpval2  23493  chpchtsum  23494  chpub  23495  logfacrlim  23499  logexprlim  23500  mersenne  23502  dchrelbas4  23518  bcmono  23552  bposlem1  23559  bposlem2  23560  lgslem3  23573  lgslem4  23574  lgsmod  23596  lgsdir2lem4  23601  lgsdirprm  23604  lgsquadlem2  23630  2sqlem8  23647  chebbnd1lem1  23654  chebbnd1lem2  23655  chtppilimlem1  23658  chebbnd2  23662  chto1lb  23663  chpchtlim  23664  chpo1ubb  23666  vmadivsum  23667  rplogsumlem1  23669  rpvmasumlem  23672  dchrisumlem3  23676  dchrmusumlema  23678  dchrmusum2  23679  dchrvmasumlem2  23683  dchrvmasumlem3  23684  dchrvmasumiflem1  23686  dchrvmasumiflem2  23687  dchrisum0flblem1  23693  dchrisum0fno1  23696  dchrisum0re  23698  dchrisum0lema  23699  dchrisum0lem1b  23700  dchrisum0lem2a  23702  dchrisum0lem2  23703  dchrisum0lem3  23704  rplogsum  23712  dirith2  23713  mudivsum  23715  mulogsumlem  23716  mulogsum  23717  mulog2sumlem1  23719  mulog2sumlem2  23720  vmalogdivsum2  23723  vmalogdivsum  23724  2vmadivsumlem  23725  log2sumbnd  23729  selberglem2  23731  selberg2lem  23735  chpdifbnd  23740  selberg3lem1  23742  selberg3  23744  selberg4lem1  23745  selberg4  23746  pntrmax  23749  pntrsumo1  23750  pntrsumbnd  23751  selberg3r  23754  selberg4r  23755  selberg34r  23756  pntrlog2bndlem1  23762  pntrlog2bndlem2  23763  pntrlog2bndlem3  23764  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  pntrlog2bndlem6  23768  pntrlog2bnd  23769  pntpbnd1  23771  pntibndlem2a  23775  pntibndlem2  23776  pntibnd  23778  pntlemc  23780  pntlemg  23783  pntlemr  23787  pntlemk  23791  qabvle  23810  ostth2lem3  23820  ostth2  23822  trgcgrg  23906  ttgcontlem1  24188  axpaschlem  24243  axlowdimlem16  24260  axcontlem2  24268  axcontlem7  24273  wwlkm1edg  24735  wwlkextproplem1  24741  wwlkextproplem2  24742  clwlkisclwwlklem2fv1  24782  clwlkisclwwlklem2fv2  24783  clwlkisclwwlklem1  24787  clwlkisclwwlk2  24790  clwwlkf1  24796  clwwlkext2edg  24802  clwwisshclwwlem  24806  usg2cwwkdifex  24821  extwwlkfablem2  25078  numclwwlkovf2ex  25086  numclwlk1lem2f1  25094  numclwwlk7  25114  frgrareggt1  25116  frgraregord013  25118  frgraogt3nreg  25120  smcnlem  25607  nmoub3i  25688  blocnilem  25719  ubthlem2  25787  minvecolem4  25796  htthlem  25834  nmcexi  26945  nmopcoi  27014  cdj1i  27352  nn0sqeq1  27562  nndiffz1  27596  fzsplit3  27599  unitdivcld  27883  sqsscirc1  27890  nexple  28005  indf1o  28037  esumdivc  28089  dya2ub  28241  dya2iocress  28245  dya2iocbrsiga  28246  dya2icobrsiga  28247  dya2icoseg  28248  dya2iocucvr  28255  sxbrsigalem2  28257  fibp1  28340  probmeasb  28369  dstrvprob  28410  dstfrvunirn  28413  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemsgt1  28449  ballotlemsel1i  28451  ballotlemfrcn0  28468  signsply0  28508  lgamgulmlem2  28572  lgamgulmlem3  28573  lgamgulmlem4  28574  lgamgulmlem5  28575  lgamgulmlem6  28576  lgamcvg2  28597  regamcl  28603  subfaclim  28632  cvmliftlem2  28731  cvmliftlem13  28741  snmlff  28774  faclim  29171  bpoly4  29821  itg2addnclem2  30067  itg2addnclem3  30068  areacirclem1  30107  areacirclem4  30110  nn0prpwlem  30140  incsequz  30241  totbndbnd  30285  bfplem2  30319  lzenom  30703  irrapxlem1  30758  irrapxlem2  30759  irrapxlem4  30761  irrapxlem5  30762  pellexlem2  30766  pell1qrge1  30806  pell1qr1  30807  elpell1qr2  30808  pell14qrgapw  30812  pellfundgt1  30819  pellfundglb  30821  pellfundex  30822  pellfundrp  30824  pellfundne1  30825  rmspecnonsq  30843  rmspecfund  30845  rmspecpos  30852  monotoddzzfi  30878  rmygeid  30902  areaquad  31184  isprm7  31192  cvgdvgrat  31194  radcnvrat  31195  hashnzfzclim  31227  lhe4.4ex1a  31234  binomcxplemnn0  31254  binomcxplemdvbinom  31258  binomcxplemnotnn0  31261  oddfl  31459  abscosbd  31460  zltlesub  31468  abssinbd  31490  monoords  31496  fzisoeu  31500  fzdifsuc2  31512  fmul01  31574  fmul01lt1lem1  31578  fmul01lt1lem2  31579  fprodle  31604  climsuselem1  31613  sumnnodd  31636  0ellimcdiv  31655  dvmptidg  31712  dvcosax  31723  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvxpaek  31737  dvnmul  31740  iblspltprt  31772  itgspltprt  31778  stoweidlem5  31787  stoweidlem7  31789  stoweidlem10  31792  stoweidlem11  31793  stoweidlem12  31794  stoweidlem13  31795  stoweidlem14  31796  stoweidlem16  31798  stoweidlem18  31800  stoweidlem20  31802  stoweidlem24  31806  stoweidlem25  31807  stoweidlem34  31816  stoweidlem36  31818  stoweidlem38  31820  stoweidlem40  31822  stoweidlem41  31823  stoweidlem42  31824  stoweidlem45  31827  stoweidlem51  31833  stoweidlem60  31842  wallispilem3  31849  wallispilem4  31850  wallispilem5  31851  wallispi  31852  wallispi2lem1  31853  wallispi2lem2  31854  wallispi2  31855  stirlinglem1  31856  stirlinglem3  31858  stirlinglem5  31860  stirlinglem6  31861  stirlinglem7  31862  stirlinglem8  31863  stirlinglem10  31865  stirlinglem11  31866  stirlinglem12  31867  stirlinglem13  31868  stirlinglem15  31870  dirker2re  31874  dirkerval2  31876  dirkerre  31877  dirkertrigeqlem1  31880  dirkertrigeqlem3  31882  dirkeritg  31884  dirkercncflem1  31885  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem5  31894  fourierdlem6  31895  fourierdlem11  31900  fourierdlem15  31904  fourierdlem19  31908  fourierdlem20  31909  fourierdlem24  31913  fourierdlem26  31915  fourierdlem28  31917  fourierdlem30  31919  fourierdlem39  31928  fourierdlem41  31930  fourierdlem43  31932  fourierdlem47  31936  fourierdlem48  31937  fourierdlem56  31945  fourierdlem60  31949  fourierdlem61  31950  fourierdlem62  31951  fourierdlem64  31953  fourierdlem65  31954  fourierdlem66  31955  fourierdlem68  31957  fourierdlem73  31962  fourierdlem78  31967  fourierdlem79  31968  fourierdlem87  31976  fourierdlem103  31992  fourierdlem104  31993  sqwvfoura  32011  fouriersw  32014  etransclem4  32021  etransclem23  32040  etransclem24  32041  etransclem31  32048  etransclem32  32049  etransclem35  32052  etransclem41  32058  etransclem46  32063  etransclem48  32065  etransc  32066  sigaradd  32083  p1lep2  32322  zm1nn  32325  cznnring  32764  nn0le2is012  32956  reseccl  33147  recsccl  33148  imo72b2lem0  37982  imo72b2lem1  37988  imo72b2  37993

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-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  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