Theorem 1red 9934

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

Assertion

Ref	Expression
1red	⊢ (𝜑 → 1 ∈ ℝ)

Proof of Theorem 1red

Step	Hyp	Ref	Expression
1		1re 9918	. 2 ⊢ 1 ∈ ℝ
2	1	a1i 11	1 ⊢ (𝜑 → 1 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1977  ℝcr 9814  1c1 9816

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-mulcl 9877  ax-mulrcl 9878  ax-i2m1 9883  ax-1ne0 9884  ax-rrecex 9887  ax-cnre 9888

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552

This theorem is referenced by:  recgt0  10746  ltrec  10784  nn0p1gt0  11199  nn0ge2m1nn  11237  suprzcl  11333  ledivge1le  11777  qbtwnre  11904  iccf1o  12187  xov1plusxeqvd  12189  zltaddlt1le  12195  fznatpl1  12265  elfz1b  12279  fzonn0p1p1  12413  elfzom1p1elfzo  12414  elfznelfzo  12439  elfznelfzob  12440  fladdz  12488  2tnp1ge0ge0  12492  flhalf  12493  ltdifltdiv  12497  fldiv4lem1div2uz2  12499  mulp1mod1  12573  m1modge3gt1  12579  modltm1p1mod  12584  addmodlteq  12607  ltexp2a  12774  expcan  12775  ltexp2  12776  leexp2  12777  leexp2a  12778  leexp2r  12780  nnlesq  12830  bernneq3  12854  expnbnd  12855  expnlbnd2  12857  fzsdom2  13075  wrdlenge2n0  13196  swrd2lsw  13543  2swrd2eqwrdeq  13544  rddif  13928  reccn2  14175  rlimo1  14195  o1fsum  14386  abscvgcvg  14392  climcndslem1  14420  flo1  14425  harmonic  14430  geomulcvg  14446  fprodrecl  14522  fprodle  14566  bpoly4  14629  efcllem  14647  efgt1  14685  tanhlt1  14729  sinltx  14758  eirrlem  14771  mod2eq1n2dvds  14909  oddge22np1  14911  ltoddhalfle  14923  nn0o1gt2  14935  nno  14936  nn0oddm1d2  14939  nnoddm1d2  14940  bitsfzolem  14994  bitsfzo  14995  bitsmod  14996  bitscmp  14998  bitsinv1lem  15001  smuval2  15042  coprmgcdb  15200  prmind2  15236  dvdsnprmd  15241  isprm5  15257  isprm7  15258  divdenle  15295  zsqrtelqelz  15304  fermltl  15327  odzdvds  15338  modprm0  15348  iserodd  15378  difsqpwdvds  15429  pcfaclem  15440  prmreclem1  15458  4sqlem11  15497  4sqlem12  15498  ramub1lem1  15568  prmgaplem8  15600  2expltfac  15637  pgpfaclem2  18304  znidomb  19729  chfacfisf  20478  chfacfisfcpmat  20479  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  nrginvrcnlem  22305  nmoid  22356  xrsmopn  22423  metnrmlem1a  22469  iccpnfhmeo  22552  htpycc  22587  pcohtpylem  22627  pcoass  22632  pcorevlem  22634  nmhmcn  22728  cncmet  22927  ovoliunlem1  23077  dyadmaxlem  23171  vitalilem2  23184  mbfi1fseqlem6  23293  itg2mulc  23320  itg2monolem1  23323  itg2monolem3  23325  dveflem  23546  mvth  23559  dvlipcn  23561  lhop1lem  23580  dvfsumlem1  23593  dvfsumlem2  23594  dvfsumlem3  23595  dvfsumlem4  23596  dvfsum2  23601  fta1glem2  23730  plyeq0lem  23770  fta1lem  23866  vieta1lem2  23870  aalioulem3  23893  aalioulem4  23894  radcnvlem1  23971  radcnvlem2  23972  dvradcnv  23979  abelthlem2  23990  abelthlem5  23993  abelthlem7  23996  abelth2  24000  cosne0  24080  rplogcl  24154  logdivlti  24170  logno1  24182  advlog  24200  logtayllem  24205  cxplt  24240  cxple  24241  cxpaddlelem  24292  cxpaddle  24293  relogbf  24329  isosctrlem1  24348  isosctrlem2  24349  heron  24365  atanlogaddlem  24440  bndatandm  24456  leibpi  24469  log2tlbnd  24472  birthdaylem3  24480  rlimcnp  24492  rlimcnp2  24493  efrlim  24496  cxp2limlem  24502  divsqrtsumo1  24510  jensenlem2  24514  logdiflbnd  24521  fsumharmonic  24538  lgamgulmlem2  24556  lgamgulmlem3  24557  lgamgulmlem4  24558  lgamgulmlem5  24559  lgamgulmlem6  24560  lgamcvg2  24581  regamcl  24587  wilthlem2  24595  ftalem2  24600  basellem9  24615  vma1  24692  ppieq0  24702  mumullem2  24706  fsumfldivdiaglem  24715  chpeq0  24733  chtub  24737  chpval2  24743  chpchtsum  24744  chpub  24745  logfacrlim  24749  logexprlim  24750  mersenne  24752  perfectlem2  24755  dchrelbas4  24768  bcmono  24802  bposlem1  24809  bposlem2  24810  zabsle1  24821  lgslem3  24824  lgslem4  24825  lgsmod  24848  lgsdir2lem4  24853  lgsdirprm  24856  gausslemma2dlem1a  24890  gausslemma2d  24899  lgsquadlem2  24906  2sqlem8  24951  chebbnd1lem1  24958  chebbnd1lem2  24959  chtppilimlem1  24962  chebbnd2  24966  chto1lb  24967  chpchtlim  24968  chpo1ubb  24970  vmadivsum  24971  rplogsumlem1  24973  rpvmasumlem  24976  dchrisumlem3  24980  dchrmusumlema  24982  dchrmusum2  24983  dchrvmasumlem2  24987  dchrvmasumlem3  24988  dchrvmasumiflem1  24990  dchrvmasumiflem2  24991  dchrisum0flblem1  24997  dchrisum0flblem2  24998  dchrisum0fno1  25000  dchrisum0re  25002  dchrisum0lema  25003  dchrisum0lem1b  25004  dchrisum0lem2a  25006  dchrisum0lem2  25007  dchrisum0lem3  25008  rplogsum  25016  dirith2  25017  mudivsum  25019  mulogsumlem  25020  mulogsum  25021  mulog2sumlem1  25023  mulog2sumlem2  25024  vmalogdivsum2  25027  vmalogdivsum  25028  2vmadivsumlem  25029  log2sumbnd  25033  selberglem2  25035  selberg2lem  25039  chpdifbnd  25044  selberg3lem1  25046  selberg3  25048  selberg4lem1  25049  selberg4  25050  pntrmax  25053  pntrsumo1  25054  pntrsumbnd  25055  selberg3r  25058  selberg4r  25059  selberg34r  25060  pntrlog2bndlem1  25066  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  pntrlog2bnd  25073  pntpbnd1a  25074  pntpbnd1  25075  pntibndlem2a  25079  pntibndlem2  25080  pntibnd  25082  pntlemc  25084  pntlemg  25087  pntlemr  25091  pntlemk  25095  qabvle  25114  ostth2lem3  25124  ostth2  25126  trgcgrg  25210  tgcgr4  25226  ttgcontlem1  25565  axpaschlem  25620  axlowdimlem16  25637  axcontlem2  25645  axcontlem7  25650  wwlkm1edg  26263  wwlkextproplem1  26269  wwlkextproplem2  26270  clwlkisclwwlklem2fv1  26310  clwlkisclwwlklem2fv2  26311  clwlkisclwwlklem1  26315  clwlkisclwwlk2  26318  clwwlkf1  26324  clwwlkext2edg  26330  clwwisshclwwlem  26334  usg2cwwkdifex  26349  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwlk1lem2f1  26621  numclwwlk7  26641  frgrareggt1  26643  frgraregord013  26645  frgraogt3nreg  26647  smcnlem  26936  nmoub3i  27012  blocnilem  27043  ubthlem2  27111  minvecolem4  27120  htthlem  27158  nmcexi  28269  nmopcoi  28338  stadd3i  28491  cdj1i  28676  nn0sqeq1  28901  nndiffz1  28936  fzsplit3  28940  pmtrto1cl  29180  fzto1st1  29183  fzto1st  29184  psgnfzto1st  29186  1smat1  29198  submateqlem1  29201  madjusmdetlem2  29222  unitdivcld  29275  sqsscirc1  29282  nexple  29399  indf1o  29413  esumdivc  29472  dya2ub  29659  dya2iocress  29663  dya2iocbrsiga  29664  dya2icobrsiga  29665  dya2icoseg  29666  dya2iocucvr  29673  sxbrsigalem2  29675  fibp1  29790  probmeasb  29819  dstrvprob  29860  dstfrvunirn  29863  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemsgt1  29899  ballotlemsel1i  29901  ballotlemfrcn0  29918  signsply0  29954  subfaclim  30424  cvmliftlem2  30522  cvmliftlem13  30532  snmlff  30565  bccolsum  30878  faclim  30885  nn0prpwlem  31487  dnibndlem10  31647  dnibndlem12  31649  knoppcnlem4  31656  unblimceq0  31668  knoppndvlem1  31673  knoppndvlem2  31674  knoppndvlem3  31675  knoppndvlem7  31679  knoppndvlem11  31683  knoppndvlem12  31684  knoppndvlem14  31686  knoppndvlem15  31687  knoppndvlem17  31689  knoppndvlem18  31690  knoppndvlem20  31692  poimirlem6  32585  poimirlem7  32586  poimirlem15  32594  poimirlem19  32598  poimirlem29  32608  poimirlem30  32609  poimirlem31  32610  poimirlem32  32611  broucube  32613  itg2addnclem2  32632  itg2addnclem3  32633  areacirclem1  32670  areacirclem4  32673  incsequz  32714  totbndbnd  32758  bfplem2  32792  lzenom  36351  irrapxlem1  36404  irrapxlem2  36405  irrapxlem4  36407  irrapxlem5  36408  pellexlem2  36412  pell1qrge1  36452  pell1qr1  36453  elpell1qr2  36454  pell14qrgapw  36458  pellfundgt1  36465  pellfundglb  36467  pellfundex  36468  pellfundrp  36470  pellfundne1  36471  rmspecsqrtnq  36488  rmspecnonsq  36490  rmspecfund  36492  rmspecpos  36499  monotoddzzfi  36525  rmygeid  36549  areaquad  36821  imo72b2lem0  37487  imo72b2lem1  37493  imo72b2  37497  cvgdvgrat  37534  radcnvrat  37535  hashnzfzclim  37543  lhe4.4ex1a  37550  binomcxplemnn0  37570  binomcxplemdvbinom  37574  binomcxplemnotnn0  37577  oddfl  38430  abscosbd  38431  zltlesub  38438  abssinbd  38450  monoords  38452  fzisoeu  38455  fzdifsuc2  38466  suplesup  38496  xralrple2  38511  infxr  38524  infleinflem2  38528  reclt0d  38548  xrralrecnnge  38554  sqrlearg  38627  iooiinioc  38630  fmul01  38647  fmul01lt1lem1  38651  fmul01lt1lem2  38652  climsuselem1  38674  sumnnodd  38697  0ellimcdiv  38716  dvmptidg  38805  dvcosax  38816  ioodvbdlimc1lem1  38821  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvxpaek  38830  dvnmul  38833  iblspltprt  38865  itgspltprt  38871  stoweidlem5  38898  stoweidlem7  38900  stoweidlem10  38903  stoweidlem11  38904  stoweidlem12  38905  stoweidlem13  38906  stoweidlem14  38907  stoweidlem16  38909  stoweidlem18  38911  stoweidlem20  38913  stoweidlem24  38917  stoweidlem25  38918  stoweidlem34  38927  stoweidlem36  38929  stoweidlem38  38931  stoweidlem40  38933  stoweidlem41  38934  stoweidlem42  38935  stoweidlem45  38938  stoweidlem51  38944  stoweidlem60  38953  wallispilem3  38960  wallispilem4  38961  wallispilem5  38962  wallispi  38963  wallispi2lem1  38964  wallispi2lem2  38965  wallispi2  38966  stirlinglem1  38967  stirlinglem3  38969  stirlinglem5  38971  stirlinglem6  38972  stirlinglem7  38973  stirlinglem8  38974  stirlinglem10  38976  stirlinglem11  38977  stirlinglem12  38978  stirlinglem13  38979  stirlinglem15  38981  dirker2re  38985  dirkerval2  38987  dirkerre  38988  dirkertrigeqlem1  38991  dirkertrigeqlem3  38993  dirkeritg  38995  dirkercncflem1  38996  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem5  39005  fourierdlem6  39006  fourierdlem11  39011  fourierdlem15  39015  fourierdlem19  39019  fourierdlem20  39020  fourierdlem24  39024  fourierdlem26  39026  fourierdlem28  39028  fourierdlem30  39030  fourierdlem39  39039  fourierdlem41  39041  fourierdlem43  39043  fourierdlem47  39046  fourierdlem48  39047  fourierdlem56  39055  fourierdlem60  39059  fourierdlem61  39060  fourierdlem62  39061  fourierdlem64  39063  fourierdlem65  39064  fourierdlem66  39065  fourierdlem68  39067  fourierdlem73  39072  fourierdlem78  39077  fourierdlem79  39078  fourierdlem87  39086  fourierdlem103  39102  fourierdlem104  39103  sqwvfoura  39121  fouriersw  39124  etransclem4  39131  etransclem23  39150  etransclem24  39151  etransclem31  39158  etransclem32  39159  etransclem35  39162  etransclem41  39168  etransclem46  39173  etransclem48  39175  etransc  39176  ioorrnopnxrlem  39202  nnfoctbdjlem  39348  iundjiun  39353  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoidmvlelem4  39488  ovnhoilem1  39491  vonioolem2  39572  vonicclem2  39575  pimrecltneg  39610  smfrec  39674  smfmullem1  39676  smfmullem2  39677  smfdiv  39682  sigaradd  39704  m1mod0mod1  39949  iccpartiltu  39960  iccpartlt  39962  iccpartgt  39965  fmtnoge3  39980  fmtnodvds  39994  fmtnoprmfac2lem1  40016  2pwp1prm  40041  flsqrt  40046  sfprmdvdsmersenne  40058  lighneallem2  40061  lighneallem4a  40063  proththdlem  40068  proththd  40069  nnoALTV  40144  bgoldbtbndlem4  40224  pfx2  40275  p1lep2  40346  zm1nn  40348  nbusgrvtxm1  40607  upgrewlkle2  40808  pthdlem1  40972  crctcsh1wlkn0lem3  41015  crctcsh1wlkn0lem5  41017  wwlksm1edg  41078  wwlksnextproplem2  41116  clwlkclwwlklem2fv1  41204  clwlkclwwlklem2fv2  41205  clwlkclwwlklem2  41209  clwlkclwwlk2  41212  clwwlksf1  41224  clwwlksext2edg  41230  clwwisshclwwslem  41234  av-extwwlkfablem2  41510  av-numclwwlkovf2ex  41517  av-numclwlk1lem2f1  41524  av-numclwwlk7  41545  av-frgrareggt1  41547  av-frgraogt3nreg  41551  cznnring  41748  nn0le2is012  41938  divge1b  42096  divgt1b  42097  m1modmmod  42110  difmodm1lt  42111  nn0eo  42116  regt1loggt0  42128  rege1logbrege0  42150  logblt1b  42156  fllog2  42160  nnolog2flm1  42182  dignn0flhalflem1  42207  reseccl  42293  recsccl  42294  amgmwlem  42357  amgmlemALT  42358