Theorem 1red 11291

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11183  1c1 11185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451

This theorem is referenced by:  recgt0  12140  mulgt1  12156  ltrec  12177  nnne0  12327  nn0p1gt0  12582  nn0ge2m1nn  12622  nn0le2is012  12707  suprzcl  12723  ledivge1le  13128  qbtwnre  13261  lincmb01cmp  13555  iccf1o  13556  xov1plusxeqvd  13558  zltaddlt1le  13565  fznatpl1  13638  elfz1b  13653  fzonn0p1p1  13795  elfznelfzo  13822  elfznelfzob  13823  fladdz  13876  2tnp1ge0ge0  13880  flhalf  13881  ltdifltdiv  13885  fldiv4lem1div2uz2  13887  mulp1mod1  13963  m1modge3gt1  13969  modltm1p1mod  13974  addmodlteq  13997  ltexp2a  14216  expcan  14219  ltexp2  14220  leexp2  14221  leexp2a  14222  leexp2r  14224  nnlesq  14254  bernneq3  14280  expnbnd  14281  expnlbnd2  14283  expnngt1  14290  fzsdom2  14477  wrdlenge2n0  14600  swrd2lsw  15001  2swrd2eqwrdeq  15002  01sqrexlem7  15297  rddif  15389  reccn2  15643  rlimo1  15663  o1fsum  15861  abscvgcvg  15867  climcndslem1  15897  flo1  15902  harmonic  15907  geomulcvg  15924  fprodrecl  16001  fprodreclf  16007  fprodle  16044  bpoly4  16107  efcllem  16125  efgt1  16164  tanhlt1  16208  sinltx  16237  eirrlem  16252  p1modz1  16309  mod2eq1n2dvds  16395  oddge22np1  16397  ltoddhalfle  16409  nn0o1gt2  16429  nno  16430  nn0oddm1d2  16433  nnoddm1d2  16434  bitsfzolem  16480  bitsfzo  16481  bitsmod  16482  bitscmp  16484  bitsinv1lem  16487  smuval2  16528  coprmgcdb  16696  prmind2  16732  dvdsnprmd  16737  2mulprm  16740  isprm5  16754  isprm7  16755  divdenle  16796  zsqrtelqelz  16805  fermltl  16831  odzdvds  16842  modprm0  16852  iserodd  16882  difsqpwdvds  16934  pcfaclem  16945  prmreclem1  16963  4sqlem11  17002  4sqlem12  17003  ramub1lem1  17073  prmgaplem8  17105  2expltfac  17140  pgpfaclem2  20126  znidomb  21603  chfacfisf  22881  chfacfisfcpmat  22882  chfacfscmulgsum  22887  chfacfpmmulgsum  22891  nrginvrcnlem  24733  nmoid  24784  xrsmopn  24853  metnrmlem1a  24899  iihalf2cn  24981  iccpnfhmeo  24995  lebnumii  25017  htpycc  25031  pcohtpylem  25071  pcoass  25076  pcorevlem  25078  nmhmcn  25172  cncmet  25375  ovoliunlem1  25556  dyadmaxlem  25651  vitalilem2  25663  mbfi1fseqlem6  25775  itg2mulc  25802  itg2monolem1  25805  itg2monolem3  25807  dveflem  26037  mvth  26051  dvlipcn  26053  lhop1lem  26072  dvfsumlem1  26086  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem3  26089  dvfsumlem4  26090  dvfsum2  26095  fta1glem2  26228  plyeq0lem  26269  fta1lem  26367  vieta1lem2  26371  aalioulem3  26394  aalioulem4  26395  radcnvlem1  26474  radcnvlem2  26475  dvradcnv  26482  abelthlem2  26494  abelthlem5  26497  abelthlem7  26500  abelth2  26504  cos02pilt1  26586  cosne0  26589  rplogcl  26664  logdivlti  26680  logno1  26696  dvlog2lem  26712  advlog  26714  logtayllem  26719  cxplt  26754  cxple  26755  cxpaddlelem  26812  cxpaddle  26813  rtprmirr  26821  relogbf  26852  logbgt0b  26854  isosctrlem1  26879  isosctrlem2  26880  chordthmlem4  26896  heron  26899  atanlogaddlem  26974  bndatandm  26990  leibpi  27003  log2tlbnd  27006  birthdaylem3  27014  rlimcnp  27026  rlimcnp2  27027  efrlim  27030  efrlimOLD  27031  cxp2limlem  27037  cxp2lim  27038  divsqrtsumo1  27045  jensenlem2  27049  logdiflbnd  27056  fsumharmonic  27073  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamgulmlem4  27093  lgamgulmlem5  27094  lgamgulmlem6  27095  lgamcvg2  27116  regamcl  27122  wilthlem2  27130  ftalem2  27135  basellem9  27150  vma1  27227  ppieq0  27237  mumullem2  27241  fsumfldivdiaglem  27250  chpeq0  27270  chtub  27274  chpval2  27280  chpchtsum  27281  chpub  27282  logfacrlim  27286  logexprlim  27287  mersenne  27289  perfectlem2  27292  dchrelbas4  27305  bcmono  27339  bposlem1  27346  bposlem2  27347  zabsle1  27358  lgslem3  27361  lgsmod  27385  lgsdir2lem4  27390  lgsdirprm  27393  gausslemma2dlem1a  27427  gausslemma2d  27436  lgsquadlem2  27443  2sqlem8  27488  chebbnd1lem1  27531  chebbnd1lem2  27532  chtppilimlem1  27535  chebbnd2  27539  chto1lb  27540  chpchtlim  27541  chpo1ubb  27543  vmadivsum  27544  rplogsumlem1  27546  rpvmasumlem  27549  dchrisumlem3  27553  dchrmusumlema  27555  dchrmusum2  27556  dchrvmasumlem2  27560  dchrvmasumlem3  27561  dchrvmasumiflem1  27563  dchrvmasumiflem2  27564  dchrisum0flblem1  27570  dchrisum0flblem2  27571  dchrisum0fno1  27573  dchrisum0re  27575  dchrisum0lema  27576  dchrisum0lem1b  27577  dchrisum0lem2a  27579  dchrisum0lem2  27580  dchrisum0lem3  27581  rplogsum  27589  dirith2  27590  mudivsum  27592  mulogsumlem  27593  mulogsum  27594  mulog2sumlem1  27596  mulog2sumlem2  27597  vmalogdivsum2  27600  vmalogdivsum  27601  2vmadivsumlem  27602  log2sumbnd  27606  selberglem2  27608  selberg2lem  27612  chpdifbnd  27617  selberg3lem1  27619  selberg3  27621  selberg4lem1  27622  selberg4  27623  pntrmax  27626  pntrsumo1  27627  pntrsumbnd  27628  selberg3r  27631  selberg4r  27632  selberg34r  27633  pntrlog2bndlem1  27639  pntrlog2bndlem2  27640  pntrlog2bndlem3  27641  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  pntrlog2bndlem6  27645  pntrlog2bnd  27646  pntpbnd1a  27647  pntpbnd1  27648  pntibndlem2a  27652  pntibndlem2  27653  pntibnd  27655  pntlemc  27657  pntlemg  27660  pntlemr  27664  pntlemk  27668  pnt  27676  qabvle  27687  ostth2lem3  27697  ostth2  27699  trgcgrg  28541  tgcgr4  28557  ttgcontlem1  28917  axpaschlem  28973  axlowdimlem16  28990  axcontlem2  28998  axcontlem7  29003  nbusgrvtxm1  29414  upgrewlkle2  29642  pthdlem1  29802  crctcshwlkn0lem3  29845  crctcshwlkn0lem5  29847  wwlksm1edg  29914  wwlksnextproplem2  29943  clwlkclwwlklem2fv1  30027  clwlkclwwlklem2fv2  30028  clwlkclwwlklem2  30032  clwlkclwwlk2  30035  clwwisshclwwslem  30046  clwwlkf1  30081  clwwlkext2edg  30088  clwlknf1oclwwlknlem1  30113  clwwlknonex2lem2  30140  numclwwlk7  30423  frgrreggt1  30425  frgrogt3nreg  30429  smcnlem  30729  nmoub3i  30805  blocnilem  30836  ubthlem2  30903  minvecolem4  30912  htthlem  30949  nmcexi  32058  nmopcoi  32127  stadd3i  32280  cdj1i  32465  nnmulge  32752  nndiffz1  32791  fzsplit3  32799  wrdt2ind  32920  pmtrto1cl  33092  fzto1st1  33095  fzto1st  33096  psgnfzto1st  33098  cycpmco2lem6  33124  cycpmco2lem7  33125  cycpmrn  33136  qsidomlem1  33445  krull  33472  ply1degltel  33580  ply1degltlss  33582  1smat1  33750  submateqlem1  33753  madjusmdetlem2  33774  unitdivcld  33847  sqsscirc1  33854  nexple  33973  indf1o  33988  esumdivc  34047  dya2ub  34235  dya2iocress  34239  dya2iocbrsiga  34240  dya2icobrsiga  34241  dya2icoseg  34242  dya2iocucvr  34249  sxbrsigalem2  34251  fibp1  34366  probmeasb  34395  dstrvprob  34436  dstfrvunirn  34439  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemsgt1  34475  ballotlemsel1i  34477  ballotlemfrcn0  34494  signsply0  34528  itgexpif  34583  reprlt  34596  chtvalz  34606  breprexplemc  34609  breprexp  34610  circlemeth  34617  tgoldbachgnn  34636  acycgr1v  35117  subfaclim  35156  cvmliftlem2  35254  cvmliftlem13  35264  snmlff  35297  bccolsum  35701  faclim  35708  nn0prpwlem  36288  dnibndlem10  36453  dnibndlem12  36455  knoppcnlem4  36462  unblimceq0  36473  knoppndvlem1  36478  knoppndvlem2  36479  knoppndvlem3  36480  knoppndvlem7  36484  knoppndvlem11  36488  knoppndvlem12  36489  knoppndvlem14  36491  knoppndvlem15  36492  knoppndvlem17  36494  knoppndvlem18  36495  knoppndvlem20  36497  irrdiff  37292  poimirlem6  37586  poimirlem7  37587  poimirlem15  37595  poimirlem19  37599  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimirlem32  37612  broucube  37614  itg2addnclem2  37632  itg2addnclem3  37633  areacirclem1  37668  areacirclem4  37671  incsequz  37708  totbndbnd  37749  bfplem2  37783  resdvopclptsd  41985  lcmineqlem2  41987  lcmineqlem3  41988  lcmineqlem10  41995  lcmineqlem12  41997  lcmineqlem15  42000  lcmineqlem18  42003  lcmineqlem19  42004  lcmineqlem20  42005  lcmineqlem22  42007  lcmineqlem23  42008  3lexlogpow5ineq2  42012  3lexlogpow5ineq4  42013  3lexlogpow5ineq3  42014  3lexlogpow2ineq1  42015  3lexlogpow2ineq2  42016  3lexlogpow5ineq5  42017  aks4d1lem1  42019  dvrelog2  42021  dvrelog3  42022  dvrelog2b  42023  dvrelogpow2b  42025  aks4d1p1p3  42026  aks4d1p1p2  42027  aks4d1p1p4  42028  aks4d1p1p6  42030  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p1  42033  aks4d1p2  42034  aks4d1p3  42035  aks4d1p5  42037  aks4d1p6  42038  aks4d1p7d1  42039  aks4d1p7  42040  aks4d1p8d2  42042  aks4d1p8d3  42043  aks4d1p8  42044  aks4d1p9  42045  posbezout  42057  primrootlekpowne0  42062  primrootspoweq0  42063  aks6d1c1  42073  aks6d1c2p2  42076  hashscontpow1  42078  aks6d1c3  42080  aks6d1c2lem4  42084  aks6d1c2  42087  2np3bcnp1  42101  2ap1caineq  42102  sticksstones6  42108  sticksstones7  42109  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  sticksstones22  42125  aks6d1c6lem3  42129  aks6d1c6lem4  42130  bcled  42135  bcle2d  42136  aks6d1c7lem1  42137  aks6d1c7lem2  42138  unitscyglem2  42153  unitscyglem4  42155  unitscyglem5  42156  aks5lem8  42158  metakunt1  42162  metakunt2  42163  metakunt7  42168  metakunt15  42176  metakunt16  42177  metakunt24  42185  metakunt28  42189  metakunt29  42190  2xp3dxp2ge1d  42198  factwoffsmonot  42199  sn-1ne2  42254  sn-00idlem2  42375  sn-0ne2  42382  rei4  42399  sn-0tie0  42415  sn-nnne0  42424  mulgt0b2d  42436  sn-ltmulgt11d  42438  sn-0lt1  42439  sn-mulgt1d  42441  fimgmcyc  42489  flt4lem7  42614  fltnlta  42618  3cubeslem1  42640  3cubeslem3r  42643  3cubeslem4  42645  lzenom  42726  irrapxlem1  42778  irrapxlem2  42779  irrapxlem4  42781  irrapxlem5  42782  pellexlem2  42786  pell1qrge1  42826  pell1qr1  42827  elpell1qr2  42828  pell14qrgapw  42832  pellfundgt1  42839  pellfundglb  42841  pellfundex  42842  pellfundrp  42844  pellfundne1  42845  rmspecsqrtnq  42862  rmspecnonsq  42863  rmspecfund  42865  rmspecpos  42873  monotoddzzfi  42899  rmygeid  42921  areaquad  43177  imo72b2lem0  44127  imo72b2lem1  44131  imo72b2  44134  cvgdvgrat  44282  radcnvrat  44283  hashnzfzclim  44291  lhe4.4ex1a  44298  binomcxplemnn0  44318  binomcxplemdvbinom  44322  binomcxplemnotnn0  44325  oddfl  45192  abscosbd  45193  zltlesub  45200  abssinbd  45210  monoords  45212  fzisoeu  45215  fzdifsuc2  45225  suplesup  45254  xralrple2  45269  infxr  45282  infleinflem2  45286  reclt0d  45302  xrralrecnnge  45305  sqrlearg  45471  iooiinioc  45474  fmul01  45501  fmul01lt1lem1  45505  fmul01lt1lem2  45506  climsuselem1  45528  sumnnodd  45551  0ellimcdiv  45570  dvmptidg  45838  dvcosax  45847  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvxpaek  45861  dvnmul  45864  iblspltprt  45894  itgspltprt  45900  stoweidlem5  45926  stoweidlem7  45928  stoweidlem10  45931  stoweidlem11  45932  stoweidlem12  45933  stoweidlem13  45934  stoweidlem14  45935  stoweidlem16  45937  stoweidlem18  45939  stoweidlem20  45941  stoweidlem24  45945  stoweidlem25  45946  stoweidlem34  45955  stoweidlem36  45957  stoweidlem38  45959  stoweidlem40  45961  stoweidlem41  45962  stoweidlem42  45963  stoweidlem45  45966  stoweidlem51  45972  stoweidlem60  45981  wallispilem3  45988  wallispilem4  45989  wallispilem5  45990  wallispi  45991  wallispi2lem1  45992  wallispi2lem2  45993  wallispi2  45994  stirlinglem1  45995  stirlinglem3  45997  stirlinglem5  45999  stirlinglem6  46000  stirlinglem7  46001  stirlinglem8  46002  stirlinglem10  46004  stirlinglem11  46005  stirlinglem12  46006  stirlinglem13  46007  stirlinglem15  46009  dirker2re  46013  dirkerval2  46015  dirkerre  46016  dirkertrigeqlem1  46019  dirkertrigeqlem3  46021  dirkeritg  46023  dirkercncflem1  46024  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem5  46033  fourierdlem6  46034  fourierdlem11  46039  fourierdlem15  46043  fourierdlem19  46047  fourierdlem20  46048  fourierdlem24  46052  fourierdlem26  46054  fourierdlem28  46056  fourierdlem30  46058  fourierdlem39  46067  fourierdlem41  46069  fourierdlem43  46071  fourierdlem47  46074  fourierdlem48  46075  fourierdlem56  46083  fourierdlem60  46087  fourierdlem61  46088  fourierdlem62  46089  fourierdlem64  46091  fourierdlem65  46092  fourierdlem66  46093  fourierdlem68  46095  fourierdlem73  46100  fourierdlem78  46105  fourierdlem79  46106  fourierdlem87  46114  fourierdlem103  46130  fourierdlem104  46131  sqwvfoura  46149  fouriersw  46152  etransclem4  46159  etransclem23  46178  etransclem24  46179  etransclem31  46186  etransclem32  46187  etransclem35  46190  etransclem41  46196  etransclem46  46201  etransclem48  46203  etransc  46204  ioorrnopnxrlem  46227  nnfoctbdjlem  46376  iundjiun  46381  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  ovnhoilem1  46522  vonioolem2  46602  vonicclem2  46605  pimrecltneg  46645  smfrec  46710  smfmullem1  46712  smfmullem2  46713  smfdiv  46718  sigaradd  46787  p1lep2  47215  zm1nn  47217  m1mod0mod1  47243  iccpartiltu  47296  iccpartlt  47298  iccpartgt  47301  fmtnoge3  47404  fmtnodvds  47418  fmtnoprmfac2lem1  47440  2pwp1prm  47463  flsqrt  47467  sfprmdvdsmersenne  47477  lighneallem2  47480  lighneallem4a  47482  proththdlem  47487  proththd  47488  nnoALTV  47569  bgoldbtbndlem4  47682  cznnring  47985  divge1b  48241  divgt1b  48242  m1modmmod  48255  difmodm1lt  48256  nn0eo  48262  regt1loggt0  48270  rege1logbrege0  48292  logblt1b  48298  fllog2  48302  nnolog2flm1  48324  dignn0flhalflem1  48349  rrxlinesc  48469  rrxlinec  48470  eenglngeehlnmlem1  48471  eenglngeehlnmlem2  48472  line2ylem  48485  line2  48486  line2xlem  48487  reseccl  48845  recsccl  48846  amgmwlem  48896  amgmlemALT  48897