Theorem 1red 10985

Description: The number 1 is real, deduction form. (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

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

Proof of Theorem 1red

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 10879  1c1 10881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-mulcl 10942  ax-mulrcl 10943  ax-i2m1 10948  ax-1ne0 10949  ax-rrecex 10952  ax-cnre 10953

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-iota 6395  df-fv 6445  df-ov 7287

This theorem is referenced by:  recgt0  11830  ltrec  11866  nnne0  12016  nn0p1gt0  12271  nn0ge2m1nn  12311  nn0le2is012  12393  suprzcl  12409  ledivge1le  12810  qbtwnre  12942  lincmb01cmp  13236  iccf1o  13237  xov1plusxeqvd  13239  zltaddlt1le  13246  fznatpl1  13319  elfz1b  13334  fzonn0p1p1  13475  elfznelfzo  13501  elfznelfzob  13502  fladdz  13554  2tnp1ge0ge0  13558  flhalf  13559  ltdifltdiv  13563  fldiv4lem1div2uz2  13565  mulp1mod1  13641  m1modge3gt1  13647  modltm1p1mod  13652  addmodlteq  13675  ltexp2a  13893  expcan  13896  ltexp2  13897  leexp2  13898  leexp2a  13899  leexp2r  13901  nnlesq  13931  bernneq3  13955  expnbnd  13956  expnlbnd2  13958  expnngt1  13965  fzsdom2  14152  wrdlenge2n0  14264  swrd2lsw  14674  2swrd2eqwrdeq  14675  sqrlem7  14969  rddif  15061  reccn2  15315  rlimo1  15335  o1fsum  15534  abscvgcvg  15540  climcndslem1  15570  flo1  15575  harmonic  15580  geomulcvg  15597  fprodrecl  15672  fprodreclf  15678  fprodle  15715  bpoly4  15778  efcllem  15796  efgt1  15834  tanhlt1  15878  sinltx  15907  eirrlem  15922  p1modz1  15979  mod2eq1n2dvds  16065  oddge22np1  16067  ltoddhalfle  16079  nn0o1gt2  16099  nno  16100  nn0oddm1d2  16103  nnoddm1d2  16104  bitsfzolem  16150  bitsfzo  16151  bitsmod  16152  bitscmp  16154  bitsinv1lem  16157  smuval2  16198  coprmgcdb  16363  prmind2  16399  dvdsnprmd  16404  2mulprm  16407  isprm5  16421  isprm7  16422  divdenle  16462  zsqrtelqelz  16471  fermltl  16494  odzdvds  16505  modprm0  16515  iserodd  16545  difsqpwdvds  16597  pcfaclem  16608  prmreclem1  16626  4sqlem11  16665  4sqlem12  16666  ramub1lem1  16736  prmgaplem8  16768  2expltfac  16803  pgpfaclem2  19694  znidomb  20778  chfacfisf  22012  chfacfisfcpmat  22013  chfacfscmulgsum  22018  chfacfpmmulgsum  22022  nrginvrcnlem  23864  nmoid  23915  xrsmopn  23984  metnrmlem1a  24030  iccpnfhmeo  24117  lebnumii  24138  htpycc  24152  pcohtpylem  24191  pcoass  24196  pcorevlem  24198  nmhmcn  24292  cncmet  24495  ovoliunlem1  24675  dyadmaxlem  24770  vitalilem2  24782  mbfi1fseqlem6  24894  itg2mulc  24921  itg2monolem1  24924  itg2monolem3  24926  dveflem  25152  mvth  25165  dvlipcn  25167  lhop1lem  25186  dvfsumlem1  25199  dvfsumlem2  25200  dvfsumlem3  25201  dvfsumlem4  25202  dvfsum2  25207  fta1glem2  25340  plyeq0lem  25380  fta1lem  25476  vieta1lem2  25480  aalioulem3  25503  aalioulem4  25504  radcnvlem1  25581  radcnvlem2  25582  dvradcnv  25589  abelthlem2  25600  abelthlem5  25603  abelthlem7  25606  abelth2  25610  cos02pilt1  25691  cosne0  25694  rplogcl  25768  logdivlti  25784  logno1  25800  dvlog2lem  25816  advlog  25818  logtayllem  25823  cxplt  25858  cxple  25859  cxpaddlelem  25913  cxpaddle  25914  relogbf  25950  logbgt0b  25952  isosctrlem1  25977  isosctrlem2  25978  chordthmlem4  25994  heron  25997  atanlogaddlem  26072  bndatandm  26088  leibpi  26101  log2tlbnd  26104  birthdaylem3  26112  rlimcnp  26124  rlimcnp2  26125  efrlim  26128  cxp2limlem  26134  cxp2lim  26135  divsqrtsumo1  26142  jensenlem2  26146  logdiflbnd  26153  fsumharmonic  26170  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamgulmlem4  26190  lgamgulmlem5  26191  lgamgulmlem6  26192  lgamcvg2  26213  regamcl  26219  wilthlem2  26227  ftalem2  26232  basellem9  26247  vma1  26324  ppieq0  26334  mumullem2  26338  fsumfldivdiaglem  26347  chpeq0  26365  chtub  26369  chpval2  26375  chpchtsum  26376  chpub  26377  logfacrlim  26381  logexprlim  26382  mersenne  26384  perfectlem2  26387  dchrelbas4  26400  bcmono  26434  bposlem1  26441  bposlem2  26442  zabsle1  26453  lgslem3  26456  lgsmod  26480  lgsdir2lem4  26485  lgsdirprm  26488  gausslemma2dlem1a  26522  gausslemma2d  26531  lgsquadlem2  26538  2sqlem8  26583  chebbnd1lem1  26626  chebbnd1lem2  26627  chtppilimlem1  26630  chebbnd2  26634  chto1lb  26635  chpchtlim  26636  chpo1ubb  26638  vmadivsum  26639  rplogsumlem1  26641  rpvmasumlem  26644  dchrisumlem3  26648  dchrmusumlema  26650  dchrmusum2  26651  dchrvmasumlem2  26655  dchrvmasumlem3  26656  dchrvmasumiflem1  26658  dchrvmasumiflem2  26659  dchrisum0flblem1  26665  dchrisum0flblem2  26666  dchrisum0fno1  26668  dchrisum0re  26670  dchrisum0lema  26671  dchrisum0lem1b  26672  dchrisum0lem2a  26674  dchrisum0lem2  26675  dchrisum0lem3  26676  rplogsum  26684  dirith2  26685  mudivsum  26687  mulogsumlem  26688  mulogsum  26689  mulog2sumlem1  26691  mulog2sumlem2  26692  vmalogdivsum2  26695  vmalogdivsum  26696  2vmadivsumlem  26697  log2sumbnd  26701  selberglem2  26703  selberg2lem  26707  chpdifbnd  26712  selberg3lem1  26714  selberg3  26716  selberg4lem1  26717  selberg4  26718  pntrmax  26721  pntrsumo1  26722  pntrsumbnd  26723  selberg3r  26726  selberg4r  26727  selberg34r  26728  pntrlog2bndlem1  26734  pntrlog2bndlem2  26735  pntrlog2bndlem3  26736  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntrlog2bndlem6  26740  pntrlog2bnd  26741  pntpbnd1a  26742  pntpbnd1  26743  pntibndlem2a  26747  pntibndlem2  26748  pntibnd  26750  pntlemc  26752  pntlemg  26755  pntlemr  26759  pntlemk  26763  pnt  26771  qabvle  26782  ostth2lem3  26792  ostth2  26794  trgcgrg  26885  tgcgr4  26901  ttgcontlem1  27261  axpaschlem  27317  axlowdimlem16  27334  axcontlem2  27342  axcontlem7  27347  nbusgrvtxm1  27755  upgrewlkle2  27982  pthdlem1  28143  crctcshwlkn0lem3  28186  crctcshwlkn0lem5  28188  wwlksm1edg  28255  wwlksnextproplem2  28284  clwlkclwwlklem2fv1  28368  clwlkclwwlklem2fv2  28369  clwlkclwwlklem2  28373  clwlkclwwlk2  28376  clwwisshclwwslem  28387  clwwlkf1  28422  clwwlkext2edg  28429  clwlknf1oclwwlknlem1  28454  clwwlknonex2lem2  28481  numclwwlk7  28764  frgrreggt1  28766  frgrogt3nreg  28770  smcnlem  29068  nmoub3i  29144  blocnilem  29175  ubthlem2  29242  minvecolem4  29251  htthlem  29288  nmcexi  30397  nmopcoi  30466  stadd3i  30619  cdj1i  30804  nnmulge  31082  nndiffz1  31116  fzsplit3  31124  wrdt2ind  31234  pmtrto1cl  31375  fzto1st1  31378  fzto1st  31379  psgnfzto1st  31381  cycpmco2lem6  31407  cycpmco2lem7  31408  cycpmrn  31419  qsidomlem1  31637  krull  31652  1smat1  31763  submateqlem1  31766  madjusmdetlem2  31787  unitdivcld  31860  sqsscirc1  31867  nexple  31986  indf1o  32001  esumdivc  32060  dya2ub  32246  dya2iocress  32250  dya2iocbrsiga  32251  dya2icobrsiga  32252  dya2icoseg  32253  dya2iocucvr  32260  sxbrsigalem2  32262  fibp1  32377  probmeasb  32406  dstrvprob  32447  dstfrvunirn  32450  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemsgt1  32486  ballotlemsel1i  32488  ballotlemfrcn0  32505  signsply0  32539  itgexpif  32595  reprlt  32608  chtvalz  32618  breprexplemc  32621  breprexp  32622  circlemeth  32629  tgoldbachgnn  32648  acycgr1v  33120  subfaclim  33159  cvmliftlem2  33257  cvmliftlem13  33267  snmlff  33300  bccolsum  33714  faclim  33721  nn0prpwlem  34520  dnibndlem10  34676  dnibndlem12  34678  knoppcnlem4  34685  unblimceq0  34696  knoppndvlem1  34701  knoppndvlem2  34702  knoppndvlem3  34703  knoppndvlem7  34707  knoppndvlem11  34711  knoppndvlem12  34712  knoppndvlem14  34714  knoppndvlem15  34715  knoppndvlem17  34717  knoppndvlem18  34718  knoppndvlem20  34720  irrdiff  35506  poimirlem6  35792  poimirlem7  35793  poimirlem15  35801  poimirlem19  35805  poimirlem29  35815  poimirlem30  35816  poimirlem31  35817  poimirlem32  35818  broucube  35820  itg2addnclem2  35838  itg2addnclem3  35839  areacirclem1  35874  areacirclem4  35877  incsequz  35915  totbndbnd  35956  bfplem2  35990  resdvopclptsd  40043  lcmineqlem2  40045  lcmineqlem3  40046  lcmineqlem10  40053  lcmineqlem12  40055  lcmineqlem15  40058  lcmineqlem18  40061  lcmineqlem19  40062  lcmineqlem20  40063  lcmineqlem22  40065  lcmineqlem23  40066  3lexlogpow5ineq2  40070  3lexlogpow5ineq4  40071  3lexlogpow5ineq3  40072  3lexlogpow2ineq1  40073  3lexlogpow2ineq2  40074  3lexlogpow5ineq5  40075  aks4d1lem1  40077  dvrelog2  40079  dvrelog3  40080  dvrelog2b  40081  dvrelogpow2b  40083  aks4d1p1p3  40084  aks4d1p1p2  40085  aks4d1p1p4  40086  aks4d1p1p6  40088  aks4d1p1p7  40089  aks4d1p1p5  40090  aks4d1p1  40091  aks4d1p2  40092  aks4d1p3  40093  aks4d1p5  40095  aks4d1p6  40096  aks4d1p7d1  40097  aks4d1p7  40098  aks4d1p8d2  40100  aks4d1p8d3  40101  aks4d1p8  40102  aks4d1p9  40103  2np3bcnp1  40107  2ap1caineq  40108  sticksstones6  40114  sticksstones7  40115  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  sticksstones22  40131  metakunt1  40132  metakunt2  40133  metakunt7  40138  metakunt15  40146  metakunt16  40147  metakunt24  40155  metakunt28  40159  metakunt29  40160  2xp3dxp2ge1d  40169  factwoffsmonot  40170  sn-1ne2  40302  rtprmirr  40354  sn-00idlem2  40389  sn-0ne2  40396  sn-0tie0  40428  mulgt0b2d  40437  flt4lem7  40503  fltnlta  40507  3cubeslem1  40513  3cubeslem3r  40516  3cubeslem4  40518  lzenom  40599  irrapxlem1  40651  irrapxlem2  40652  irrapxlem4  40654  irrapxlem5  40655  pellexlem2  40659  pell1qrge1  40699  pell1qr1  40700  elpell1qr2  40701  pell14qrgapw  40705  pellfundgt1  40712  pellfundglb  40714  pellfundex  40715  pellfundrp  40717  pellfundne1  40718  rmspecsqrtnq  40735  rmspecnonsq  40736  rmspecfund  40738  rmspecpos  40745  monotoddzzfi  40771  rmygeid  40793  areaquad  41054  imo72b2lem0  41783  imo72b2lem1  41787  imo72b2  41790  cvgdvgrat  41938  radcnvrat  41939  hashnzfzclim  41947  lhe4.4ex1a  41954  binomcxplemnn0  41974  binomcxplemdvbinom  41978  binomcxplemnotnn0  41981  oddfl  42823  abscosbd  42824  zltlesub  42831  abssinbd  42841  monoords  42843  fzisoeu  42846  fzdifsuc2  42856  suplesup  42885  xralrple2  42900  infxr  42913  infleinflem2  42917  reclt0d  42933  xrralrecnnge  42937  sqrlearg  43098  iooiinioc  43101  fmul01  43128  fmul01lt1lem1  43132  fmul01lt1lem2  43133  climsuselem1  43155  sumnnodd  43178  0ellimcdiv  43197  dvmptidg  43465  dvcosax  43474  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvxpaek  43488  dvnmul  43491  iblspltprt  43521  itgspltprt  43527  stoweidlem5  43553  stoweidlem7  43555  stoweidlem10  43558  stoweidlem11  43559  stoweidlem12  43560  stoweidlem13  43561  stoweidlem14  43562  stoweidlem16  43564  stoweidlem18  43566  stoweidlem20  43568  stoweidlem24  43572  stoweidlem25  43573  stoweidlem34  43582  stoweidlem36  43584  stoweidlem38  43586  stoweidlem40  43588  stoweidlem41  43589  stoweidlem42  43590  stoweidlem45  43593  stoweidlem51  43599  stoweidlem60  43608  wallispilem3  43615  wallispilem4  43616  wallispilem5  43617  wallispi  43618  wallispi2lem1  43619  wallispi2lem2  43620  wallispi2  43621  stirlinglem1  43622  stirlinglem3  43624  stirlinglem5  43626  stirlinglem6  43627  stirlinglem7  43628  stirlinglem8  43629  stirlinglem10  43631  stirlinglem11  43632  stirlinglem12  43633  stirlinglem13  43634  stirlinglem15  43636  dirker2re  43640  dirkerval2  43642  dirkerre  43643  dirkertrigeqlem1  43646  dirkertrigeqlem3  43648  dirkeritg  43650  dirkercncflem1  43651  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem5  43660  fourierdlem6  43661  fourierdlem11  43666  fourierdlem15  43670  fourierdlem19  43674  fourierdlem20  43675  fourierdlem24  43679  fourierdlem26  43681  fourierdlem28  43683  fourierdlem30  43685  fourierdlem39  43694  fourierdlem41  43696  fourierdlem43  43698  fourierdlem47  43701  fourierdlem48  43702  fourierdlem56  43710  fourierdlem60  43714  fourierdlem61  43715  fourierdlem62  43716  fourierdlem64  43718  fourierdlem65  43719  fourierdlem66  43720  fourierdlem68  43722  fourierdlem73  43727  fourierdlem78  43732  fourierdlem79  43733  fourierdlem87  43741  fourierdlem103  43757  fourierdlem104  43758  sqwvfoura  43776  fouriersw  43779  etransclem4  43786  etransclem23  43805  etransclem24  43806  etransclem31  43813  etransclem32  43814  etransclem35  43817  etransclem41  43823  etransclem46  43828  etransclem48  43830  etransc  43831  ioorrnopnxrlem  43854  nnfoctbdjlem  44000  iundjiun  44005  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem3  44142  hoidmvlelem4  44143  ovnhoilem1  44146  vonioolem2  44226  vonicclem2  44229  pimrecltneg  44269  smfrec  44334  smfmullem1  44336  smfmullem2  44337  smfdiv  44342  sigaradd  44393  p1lep2  44803  zm1nn  44805  m1mod0mod1  44832  iccpartiltu  44885  iccpartlt  44887  iccpartgt  44890  fmtnoge3  44993  fmtnodvds  45007  fmtnoprmfac2lem1  45029  2pwp1prm  45052  flsqrt  45056  sfprmdvdsmersenne  45066  lighneallem2  45069  lighneallem4a  45071  proththdlem  45076  proththd  45077  nnoALTV  45158  bgoldbtbndlem4  45271  cznnring  45525  divge1b  45864  divgt1b  45865  m1modmmod  45878  difmodm1lt  45879  nn0eo  45885  regt1loggt0  45893  rege1logbrege0  45915  logblt1b  45921  fllog2  45925  nnolog2flm1  45947  dignn0flhalflem1  45972  rrxlinesc  46092  rrxlinec  46093  eenglngeehlnmlem1  46094  eenglngeehlnmlem2  46095  line2ylem  46108  line2  46109  line2xlem  46110  reseccl  46466  recsccl  46467  amgmwlem  46517  amgmlemALT  46518