Theorem 1red 11133

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

Syntax hints:   → wi 4   ∈ wcel 2113  ℝcr 11025  1c1 11027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rrecex 11098  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361

This theorem is referenced by:  recgt0  11987  mulgt1  12003  ltrec  12024  nnne0  12179  nn0p1gt0  12430  nn0ge2m1nn  12471  nn0le2is012  12556  suprzcl  12572  ledivge1le  12978  ge2halflem1  13022  qbtwnre  13114  lincmb01cmp  13411  iccf1o  13412  xov1plusxeqvd  13414  zltaddlt1le  13421  fznatpl1  13494  elfz1b  13509  elfzo0subge1  13621  fzonn0p1p1  13660  elfznelfzo  13689  elfznelfzob  13690  fladdz  13745  2tnp1ge0ge0  13749  flhalf  13750  ltdifltdiv  13754  fldiv4lem1div2uz2  13756  mulp1mod1  13834  m1modge3gt1  13841  modltm1p1mod  13846  addmodlteq  13869  ltexp2a  14089  expcan  14092  ltexp2  14093  leexp2  14094  leexp2a  14095  leexp2r  14097  nnlesq  14128  bernneq3  14154  expnbnd  14155  expnlbnd2  14157  expnngt1  14164  fzsdom2  14351  wrdlenge2n0  14475  swrd2lsw  14875  2swrd2eqwrdeq  14876  01sqrexlem7  15171  rddif  15264  reccn2  15520  rlimo1  15540  o1fsum  15736  abscvgcvg  15742  climcndslem1  15772  flo1  15777  harmonic  15782  geomulcvg  15799  fprodrecl  15876  fprodreclf  15882  fprodle  15919  bpoly4  15982  efcllem  16000  efgt1  16041  tanhlt1  16085  sinltx  16114  eirrlem  16129  p1modz1  16186  mod2eq1n2dvds  16274  oddge22np1  16276  ltoddhalfle  16288  nn0o1gt2  16308  nno  16309  nn0oddm1d2  16312  nnoddm1d2  16313  bitsfzolem  16361  bitsfzo  16362  bitsmod  16363  bitscmp  16365  bitsinv1lem  16368  smuval2  16409  coprmgcdb  16576  prmind2  16612  dvdsnprmd  16617  2mulprm  16620  isprm5  16634  isprm7  16635  divdenle  16676  zsqrtelqelz  16685  fermltl  16711  odzdvds  16723  modprm0  16733  iserodd  16763  difsqpwdvds  16815  pcfaclem  16826  prmreclem1  16844  4sqlem11  16883  4sqlem12  16884  ramub1lem1  16954  prmgaplem8  16986  2expltfac  17020  chnccat  18549  pgpfaclem2  20013  znidomb  21516  psdmvr  22112  chfacfisf  22798  chfacfisfcpmat  22799  chfacfscmulgsum  22804  chfacfpmmulgsum  22808  nrginvrcnlem  24635  nmoid  24686  xrsmopn  24757  metnrmlem1a  24803  iihalf2cn  24885  iccpnfhmeo  24899  lebnumii  24921  htpycc  24935  pcohtpylem  24975  pcoass  24980  pcorevlem  24982  nmhmcn  25076  cncmet  25278  ovoliunlem1  25459  dyadmaxlem  25554  vitalilem2  25566  mbfi1fseqlem6  25677  itg2mulc  25704  itg2monolem1  25707  itg2monolem3  25709  dveflem  25939  mvth  25953  dvlipcn  25955  lhop1lem  25974  dvfsumlem1  25988  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumlem3  25991  dvfsumlem4  25992  dvfsum2  25997  fta1glem2  26130  plyeq0lem  26171  fta1lem  26271  vieta1lem2  26275  aalioulem3  26298  aalioulem4  26299  radcnvlem1  26378  radcnvlem2  26379  dvradcnv  26386  abelthlem2  26398  abelthlem5  26401  abelthlem7  26404  abelth2  26408  cos02pilt1  26491  cosne0  26494  rplogcl  26569  logdivlti  26585  logno1  26601  dvlog2lem  26617  advlog  26619  logtayllem  26624  cxplt  26659  cxple  26660  cxpaddlelem  26717  cxpaddle  26718  rtprmirr  26726  relogbf  26757  logbgt0b  26759  isosctrlem1  26784  isosctrlem2  26785  chordthmlem4  26801  heron  26804  atanlogaddlem  26879  bndatandm  26895  leibpi  26908  log2tlbnd  26911  birthdaylem3  26919  rlimcnp  26931  rlimcnp2  26932  efrlim  26935  efrlimOLD  26936  cxp2limlem  26942  cxp2lim  26943  divsqrtsumo1  26950  jensenlem2  26954  logdiflbnd  26961  fsumharmonic  26978  lgamgulmlem2  26996  lgamgulmlem3  26997  lgamgulmlem4  26998  lgamgulmlem5  26999  lgamgulmlem6  27000  lgamcvg2  27021  regamcl  27027  wilthlem2  27035  ftalem2  27040  basellem9  27055  vma1  27132  ppieq0  27142  mumullem2  27146  fsumfldivdiaglem  27155  chpeq0  27175  chtub  27179  chpval2  27185  chpchtsum  27186  chpub  27187  logfacrlim  27191  logexprlim  27192  mersenne  27194  perfectlem2  27197  dchrelbas4  27210  bcmono  27244  bposlem1  27251  bposlem2  27252  zabsle1  27263  lgslem3  27266  lgsmod  27290  lgsdir2lem4  27295  lgsdirprm  27298  gausslemma2dlem1a  27332  gausslemma2d  27341  lgsquadlem2  27348  2sqlem8  27393  chebbnd1lem1  27436  chebbnd1lem2  27437  chtppilimlem1  27440  chebbnd2  27444  chto1lb  27445  chpchtlim  27446  chpo1ubb  27448  vmadivsum  27449  rplogsumlem1  27451  rpvmasumlem  27454  dchrisumlem3  27458  dchrmusumlema  27460  dchrmusum2  27461  dchrvmasumlem2  27465  dchrvmasumlem3  27466  dchrvmasumiflem1  27468  dchrvmasumiflem2  27469  dchrisum0flblem1  27475  dchrisum0flblem2  27476  dchrisum0fno1  27478  dchrisum0re  27480  dchrisum0lema  27481  dchrisum0lem1b  27482  dchrisum0lem2a  27484  dchrisum0lem2  27485  dchrisum0lem3  27486  rplogsum  27494  dirith2  27495  mudivsum  27497  mulogsumlem  27498  mulogsum  27499  mulog2sumlem1  27501  mulog2sumlem2  27502  vmalogdivsum2  27505  vmalogdivsum  27506  2vmadivsumlem  27507  log2sumbnd  27511  selberglem2  27513  selberg2lem  27517  chpdifbnd  27522  selberg3lem1  27524  selberg3  27526  selberg4lem1  27527  selberg4  27528  pntrmax  27531  pntrsumo1  27532  pntrsumbnd  27533  selberg3r  27536  selberg4r  27537  selberg34r  27538  pntrlog2bndlem1  27544  pntrlog2bndlem2  27545  pntrlog2bndlem3  27546  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntrlog2bnd  27551  pntpbnd1a  27552  pntpbnd1  27553  pntibndlem2a  27557  pntibndlem2  27558  pntibnd  27560  pntlemc  27562  pntlemg  27565  pntlemr  27569  pntlemk  27573  pnt  27581  qabvle  27592  ostth2lem3  27602  ostth2  27604  trgcgrg  28587  tgcgr4  28603  ttgcontlem1  28957  axpaschlem  29013  axlowdimlem16  29030  axcontlem2  29038  axcontlem7  29043  nbusgrvtxm1  29452  upgrewlkle2  29680  pthdlem1  29839  crctcshwlkn0lem3  29885  crctcshwlkn0lem5  29887  wwlksm1edg  29954  wwlksnextproplem2  29983  clwlkclwwlklem2fv1  30070  clwlkclwwlklem2fv2  30071  clwlkclwwlklem2  30075  clwlkclwwlk2  30078  clwwisshclwwslem  30089  clwwlkf1  30124  clwwlkext2edg  30131  clwlknf1oclwwlknlem1  30156  clwwlknonex2lem2  30183  numclwwlk7  30466  frgrreggt1  30468  frgrogt3nreg  30472  smcnlem  30772  nmoub3i  30848  blocnilem  30879  ubthlem2  30946  minvecolem4  30955  htthlem  30992  nmcexi  32101  nmopcoi  32170  stadd3i  32323  cdj1i  32508  nnmulge  32818  receqid  32824  nndiffz1  32866  fzsplit3  32873  nexple  32925  indf1o  32946  wrdt2ind  33035  pmtrto1cl  33181  fzto1st1  33184  fzto1st  33185  psgnfzto1st  33187  cycpmco2lem6  33213  cycpmco2lem7  33214  cycpmrn  33225  qsidomlem1  33533  krull  33560  ply1degltel  33675  ply1degltlss  33677  constrnegcl  33920  constrdircl  33922  iconstr  33923  constrrecl  33926  constrmulcl  33928  constrreinvcl  33929  constrresqrtcl  33934  cos9thpiminplylem1  33939  cos9thpiminply  33945  cos9thpinconstrlem1  33946  1smat1  33961  submateqlem1  33964  madjusmdetlem2  33985  unitdivcld  34058  sqsscirc1  34065  esumdivc  34240  dya2ub  34427  dya2iocress  34431  dya2iocbrsiga  34432  dya2icobrsiga  34433  dya2icoseg  34434  dya2iocucvr  34441  sxbrsigalem2  34443  fibp1  34558  probmeasb  34587  dstrvprob  34629  dstfrvunirn  34632  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemsgt1  34668  ballotlemsel1i  34670  ballotlemfrcn0  34687  signsply0  34708  itgexpif  34763  reprlt  34776  chtvalz  34786  breprexplemc  34789  breprexp  34790  circlemeth  34797  tgoldbachgnn  34816  acycgr1v  35343  subfaclim  35382  cvmliftlem2  35480  cvmliftlem13  35490  snmlff  35523  bccolsum  35933  faclim  35940  nn0prpwlem  36516  dnibndlem10  36687  dnibndlem12  36689  knoppcnlem4  36696  unblimceq0  36707  knoppndvlem1  36712  knoppndvlem2  36713  knoppndvlem3  36714  knoppndvlem7  36718  knoppndvlem11  36722  knoppndvlem12  36723  knoppndvlem14  36725  knoppndvlem15  36726  knoppndvlem17  36728  knoppndvlem18  36729  knoppndvlem20  36731  irrdiff  37527  poimirlem6  37823  poimirlem7  37824  poimirlem15  37832  poimirlem19  37836  poimirlem29  37846  poimirlem30  37847  poimirlem31  37848  poimirlem32  37849  broucube  37851  itg2addnclem2  37869  itg2addnclem3  37870  areacirclem1  37905  areacirclem4  37908  incsequz  37945  totbndbnd  37986  bfplem2  38020  resdvopclptsd  42278  lcmineqlem2  42280  lcmineqlem3  42281  lcmineqlem10  42288  lcmineqlem12  42290  lcmineqlem15  42293  lcmineqlem18  42296  lcmineqlem19  42297  lcmineqlem20  42298  lcmineqlem22  42300  lcmineqlem23  42301  3lexlogpow5ineq2  42305  3lexlogpow5ineq4  42306  3lexlogpow5ineq3  42307  3lexlogpow2ineq1  42308  3lexlogpow2ineq2  42309  3lexlogpow5ineq5  42310  aks4d1lem1  42312  dvrelog2  42314  dvrelog3  42315  dvrelog2b  42316  dvrelogpow2b  42318  aks4d1p1p3  42319  aks4d1p1p2  42320  aks4d1p1p4  42321  aks4d1p1p6  42323  aks4d1p1p7  42324  aks4d1p1p5  42325  aks4d1p1  42326  aks4d1p2  42327  aks4d1p3  42328  aks4d1p5  42330  aks4d1p6  42331  aks4d1p7d1  42332  aks4d1p7  42333  aks4d1p8d2  42335  aks4d1p8d3  42336  aks4d1p8  42337  aks4d1p9  42338  posbezout  42350  primrootlekpowne0  42355  primrootspoweq0  42356  aks6d1c1  42366  aks6d1c2p2  42369  hashscontpow1  42371  aks6d1c3  42373  aks6d1c2lem4  42377  aks6d1c2  42380  2np3bcnp1  42394  2ap1caineq  42395  sticksstones6  42401  sticksstones7  42402  sticksstones10  42405  sticksstones12a  42407  sticksstones12  42408  sticksstones22  42418  aks6d1c6lem3  42422  aks6d1c6lem4  42423  bcled  42428  bcle2d  42429  aks6d1c7lem1  42430  aks6d1c7lem2  42431  unitscyglem2  42446  unitscyglem4  42448  unitscyglem5  42449  aks5lem8  42451  sn-1ne2  42516  redvmptabs  42611  sn-00idlem2  42650  sn-0ne2  42657  rei4  42675  sn-rereccld  42699  rerecid  42700  sn-0tie0  42702  sn-nnne0  42711  mulgt0b1d  42723  sn-ltmulgt11d  42725  sn-0lt1  42726  sn-mulgt1d  42730  fimgmcyc  42785  flt4lem7  42898  fltnlta  42902  3cubeslem1  42922  3cubeslem3r  42925  3cubeslem4  42927  lzenom  43008  irrapxlem1  43060  irrapxlem2  43061  irrapxlem4  43063  irrapxlem5  43064  pellexlem2  43068  pell1qrge1  43108  pell1qr1  43109  elpell1qr2  43110  pell14qrgapw  43114  pellfundgt1  43121  pellfundglb  43123  pellfundex  43124  pellfundrp  43126  pellfundne1  43127  rmspecsqrtnq  43144  rmspecnonsq  43145  rmspecfund  43147  rmspecpos  43154  monotoddzzfi  43180  rmygeid  43202  areaquad  43454  imo72b2lem0  44402  imo72b2lem1  44406  imo72b2  44409  cvgdvgrat  44550  radcnvrat  44551  hashnzfzclim  44559  lhe4.4ex1a  44566  binomcxplemnn0  44586  binomcxplemdvbinom  44590  binomcxplemnotnn0  44593  oddfl  45522  abscosbd  45523  zltlesub  45529  abssinbd  45539  monoords  45541  fzisoeu  45544  fzdifsuc2  45554  suplesup  45580  xralrple2  45595  infxr  45607  infleinflem2  45611  reclt0d  45627  xrralrecnnge  45630  sqrlearg  45795  iooiinioc  45798  fmul01  45822  fmul01lt1lem1  45826  fmul01lt1lem2  45827  climsuselem1  45849  sumnnodd  45872  0ellimcdiv  45889  dvmptidg  46157  dvcosax  46166  ioodvbdlimc1lem1  46171  ioodvbdlimc1lem2  46172  ioodvbdlimc2lem  46174  dvxpaek  46180  dvnmul  46183  iblspltprt  46213  itgspltprt  46219  stoweidlem5  46245  stoweidlem7  46247  stoweidlem10  46250  stoweidlem11  46251  stoweidlem12  46252  stoweidlem13  46253  stoweidlem14  46254  stoweidlem16  46256  stoweidlem18  46258  stoweidlem20  46260  stoweidlem24  46264  stoweidlem25  46265  stoweidlem34  46274  stoweidlem36  46276  stoweidlem38  46278  stoweidlem40  46280  stoweidlem41  46281  stoweidlem42  46282  stoweidlem45  46285  stoweidlem51  46291  stoweidlem60  46300  wallispilem3  46307  wallispilem4  46308  wallispilem5  46309  wallispi  46310  wallispi2lem1  46311  wallispi2lem2  46312  wallispi2  46313  stirlinglem1  46314  stirlinglem3  46316  stirlinglem5  46318  stirlinglem6  46319  stirlinglem7  46320  stirlinglem8  46321  stirlinglem10  46323  stirlinglem11  46324  stirlinglem12  46325  stirlinglem13  46326  stirlinglem15  46328  dirker2re  46332  dirkerval2  46334  dirkerre  46335  dirkertrigeqlem1  46338  dirkertrigeqlem3  46340  dirkeritg  46342  dirkercncflem1  46343  dirkercncflem2  46344  dirkercncflem4  46346  fourierdlem5  46352  fourierdlem6  46353  fourierdlem11  46358  fourierdlem15  46362  fourierdlem19  46366  fourierdlem20  46367  fourierdlem24  46371  fourierdlem26  46373  fourierdlem28  46375  fourierdlem30  46377  fourierdlem39  46386  fourierdlem41  46388  fourierdlem43  46390  fourierdlem47  46393  fourierdlem48  46394  fourierdlem56  46402  fourierdlem60  46406  fourierdlem61  46407  fourierdlem62  46408  fourierdlem64  46410  fourierdlem65  46411  fourierdlem66  46412  fourierdlem68  46414  fourierdlem73  46419  fourierdlem78  46424  fourierdlem79  46425  fourierdlem87  46433  fourierdlem103  46449  fourierdlem104  46450  sqwvfoura  46468  fouriersw  46471  etransclem4  46478  etransclem23  46497  etransclem24  46498  etransclem31  46505  etransclem32  46506  etransclem35  46509  etransclem41  46515  etransclem46  46520  etransclem48  46522  etransc  46523  ioorrnopnxrlem  46546  nnfoctbdjlem  46695  iundjiun  46700  hoidmvlelem1  46835  hoidmvlelem2  46836  hoidmvlelem3  46837  hoidmvlelem4  46838  ovnhoilem1  46841  vonioolem2  46921  vonicclem2  46924  pimrecltneg  46964  smfrec  47029  smfmullem1  47031  smfmullem2  47032  smfdiv  47037  sigaradd  47106  ormkglobd  47115  cjnpoly  47131  p1lep2  47542  zm1nn  47544  ceilhalfgt1  47571  2tceilhalfelfzo1  47574  ceilbi  47575  rehalfge1  47577  ceilhalfnn  47578  addmodne  47586  m1mod0mod1  47596  m1modmmod  47600  difmodm1lt  47601  modmknepk  47604  modp2nep1  47609  modm1nem2  47611  iccpartiltu  47664  iccpartlt  47666  iccpartgt  47669  fmtnoge3  47772  fmtnodvds  47786  fmtnoprmfac2lem1  47808  2pwp1prm  47831  flsqrt  47835  sfprmdvdsmersenne  47845  lighneallem2  47848  lighneallem4a  47850  proththdlem  47855  proththd  47856  nnoALTV  47937  bgoldbtbndlem4  48050  gpgprismgrusgra  48300  gpgedgvtx0  48303  gpgvtxedg0  48305  gpg5nbgrvtx03starlem2  48311  gpg3kgrtriexlem4  48328  gpg3kgrtriexlem6  48330  cznnring  48504  divge1b  48754  divgt1b  48755  nn0eo  48770  regt1loggt0  48778  rege1logbrege0  48800  logblt1b  48806  fllog2  48810  nnolog2flm1  48832  dignn0flhalflem1  48857  rrxlinesc  48977  rrxlinec  48978  eenglngeehlnmlem1  48979  eenglngeehlnmlem2  48980  line2ylem  48993  line2  48994  line2xlem  48995  reseccl  49994  recsccl  49995  amgmwlem  50043  amgmlemALT  50044