Theorem 1red 11135

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11027  1c1 11029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-mulcl 11090  ax-mulrcl 11091  ax-i2m1 11096  ax-1ne0 11097  ax-rrecex 11100  ax-cnre 11101

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-iota 6442  df-fv 6494  df-ov 7356

This theorem is referenced by:  recgt0  11988  mulgt1  12004  ltrec  12025  nnne0  12180  nn0p1gt0  12431  nn0ge2m1nn  12472  nn0le2is012  12558  suprzcl  12574  ledivge1le  12984  ge2halflem1  13028  qbtwnre  13119  lincmb01cmp  13416  iccf1o  13417  xov1plusxeqvd  13419  zltaddlt1le  13426  fznatpl1  13499  elfz1b  13514  elfzo0subge1  13626  fzonn0p1p1  13665  elfznelfzo  13693  elfznelfzob  13694  fladdz  13747  2tnp1ge0ge0  13751  flhalf  13752  ltdifltdiv  13756  fldiv4lem1div2uz2  13758  mulp1mod1  13836  m1modge3gt1  13843  modltm1p1mod  13848  addmodlteq  13871  ltexp2a  14091  expcan  14094  ltexp2  14095  leexp2  14096  leexp2a  14097  leexp2r  14099  nnlesq  14130  bernneq3  14156  expnbnd  14157  expnlbnd2  14159  expnngt1  14166  fzsdom2  14353  wrdlenge2n0  14477  swrd2lsw  14877  2swrd2eqwrdeq  14878  01sqrexlem7  15173  rddif  15266  reccn2  15522  rlimo1  15542  o1fsum  15738  abscvgcvg  15744  climcndslem1  15774  flo1  15779  harmonic  15784  geomulcvg  15801  fprodrecl  15878  fprodreclf  15884  fprodle  15921  bpoly4  15984  efcllem  16002  efgt1  16043  tanhlt1  16087  sinltx  16116  eirrlem  16131  p1modz1  16188  mod2eq1n2dvds  16276  oddge22np1  16278  ltoddhalfle  16290  nn0o1gt2  16310  nno  16311  nn0oddm1d2  16314  nnoddm1d2  16315  bitsfzolem  16363  bitsfzo  16364  bitsmod  16365  bitscmp  16367  bitsinv1lem  16370  smuval2  16411  coprmgcdb  16578  prmind2  16614  dvdsnprmd  16619  2mulprm  16622  isprm5  16636  isprm7  16637  divdenle  16678  zsqrtelqelz  16687  fermltl  16713  odzdvds  16725  modprm0  16735  iserodd  16765  difsqpwdvds  16817  pcfaclem  16828  prmreclem1  16846  4sqlem11  16885  4sqlem12  16886  ramub1lem1  16956  prmgaplem8  16988  2expltfac  17022  pgpfaclem2  19981  znidomb  21486  psdmvr  22072  chfacfisf  22757  chfacfisfcpmat  22758  chfacfscmulgsum  22763  chfacfpmmulgsum  22767  nrginvrcnlem  24595  nmoid  24646  xrsmopn  24717  metnrmlem1a  24763  iihalf2cn  24845  iccpnfhmeo  24859  lebnumii  24881  htpycc  24895  pcohtpylem  24935  pcoass  24940  pcorevlem  24942  nmhmcn  25036  cncmet  25238  ovoliunlem1  25419  dyadmaxlem  25514  vitalilem2  25526  mbfi1fseqlem6  25637  itg2mulc  25664  itg2monolem1  25667  itg2monolem3  25669  dveflem  25899  mvth  25913  dvlipcn  25915  lhop1lem  25934  dvfsumlem1  25948  dvfsumlem2  25949  dvfsumlem2OLD  25950  dvfsumlem3  25951  dvfsumlem4  25952  dvfsum2  25957  fta1glem2  26090  plyeq0lem  26131  fta1lem  26231  vieta1lem2  26235  aalioulem3  26258  aalioulem4  26259  radcnvlem1  26338  radcnvlem2  26339  dvradcnv  26346  abelthlem2  26358  abelthlem5  26361  abelthlem7  26364  abelth2  26368  cos02pilt1  26451  cosne0  26454  rplogcl  26529  logdivlti  26545  logno1  26561  dvlog2lem  26577  advlog  26579  logtayllem  26584  cxplt  26619  cxple  26620  cxpaddlelem  26677  cxpaddle  26678  rtprmirr  26686  relogbf  26717  logbgt0b  26719  isosctrlem1  26744  isosctrlem2  26745  chordthmlem4  26761  heron  26764  atanlogaddlem  26839  bndatandm  26855  leibpi  26868  log2tlbnd  26871  birthdaylem3  26879  rlimcnp  26891  rlimcnp2  26892  efrlim  26895  efrlimOLD  26896  cxp2limlem  26902  cxp2lim  26903  divsqrtsumo1  26910  jensenlem2  26914  logdiflbnd  26921  fsumharmonic  26938  lgamgulmlem2  26956  lgamgulmlem3  26957  lgamgulmlem4  26958  lgamgulmlem5  26959  lgamgulmlem6  26960  lgamcvg2  26981  regamcl  26987  wilthlem2  26995  ftalem2  27000  basellem9  27015  vma1  27092  ppieq0  27102  mumullem2  27106  fsumfldivdiaglem  27115  chpeq0  27135  chtub  27139  chpval2  27145  chpchtsum  27146  chpub  27147  logfacrlim  27151  logexprlim  27152  mersenne  27154  perfectlem2  27157  dchrelbas4  27170  bcmono  27204  bposlem1  27211  bposlem2  27212  zabsle1  27223  lgslem3  27226  lgsmod  27250  lgsdir2lem4  27255  lgsdirprm  27258  gausslemma2dlem1a  27292  gausslemma2d  27301  lgsquadlem2  27308  2sqlem8  27353  chebbnd1lem1  27396  chebbnd1lem2  27397  chtppilimlem1  27400  chebbnd2  27404  chto1lb  27405  chpchtlim  27406  chpo1ubb  27408  vmadivsum  27409  rplogsumlem1  27411  rpvmasumlem  27414  dchrisumlem3  27418  dchrmusumlema  27420  dchrmusum2  27421  dchrvmasumlem2  27425  dchrvmasumlem3  27426  dchrvmasumiflem1  27428  dchrvmasumiflem2  27429  dchrisum0flblem1  27435  dchrisum0flblem2  27436  dchrisum0fno1  27438  dchrisum0re  27440  dchrisum0lema  27441  dchrisum0lem1b  27442  dchrisum0lem2a  27444  dchrisum0lem2  27445  dchrisum0lem3  27446  rplogsum  27454  dirith2  27455  mudivsum  27457  mulogsumlem  27458  mulogsum  27459  mulog2sumlem1  27461  mulog2sumlem2  27462  vmalogdivsum2  27465  vmalogdivsum  27466  2vmadivsumlem  27467  log2sumbnd  27471  selberglem2  27473  selberg2lem  27477  chpdifbnd  27482  selberg3lem1  27484  selberg3  27486  selberg4lem1  27487  selberg4  27488  pntrmax  27491  pntrsumo1  27492  pntrsumbnd  27493  selberg3r  27496  selberg4r  27497  selberg34r  27498  pntrlog2bndlem1  27504  pntrlog2bndlem2  27505  pntrlog2bndlem3  27506  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  pntrlog2bndlem6  27510  pntrlog2bnd  27511  pntpbnd1a  27512  pntpbnd1  27513  pntibndlem2a  27517  pntibndlem2  27518  pntibnd  27520  pntlemc  27522  pntlemg  27525  pntlemr  27529  pntlemk  27533  pnt  27541  qabvle  27552  ostth2lem3  27562  ostth2  27564  trgcgrg  28478  tgcgr4  28494  ttgcontlem1  28848  axpaschlem  28903  axlowdimlem16  28920  axcontlem2  28928  axcontlem7  28933  nbusgrvtxm1  29342  upgrewlkle2  29570  pthdlem1  29729  crctcshwlkn0lem3  29775  crctcshwlkn0lem5  29777  wwlksm1edg  29844  wwlksnextproplem2  29873  clwlkclwwlklem2fv1  29957  clwlkclwwlklem2fv2  29958  clwlkclwwlklem2  29962  clwlkclwwlk2  29965  clwwisshclwwslem  29976  clwwlkf1  30011  clwwlkext2edg  30018  clwlknf1oclwwlknlem1  30043  clwwlknonex2lem2  30070  numclwwlk7  30353  frgrreggt1  30355  frgrogt3nreg  30359  smcnlem  30659  nmoub3i  30735  blocnilem  30766  ubthlem2  30833  minvecolem4  30842  htthlem  30879  nmcexi  31988  nmopcoi  32057  stadd3i  32210  cdj1i  32395  nnmulge  32695  receqid  32701  nndiffz1  32742  fzsplit3  32749  nexple  32802  indf1o  32820  wrdt2ind  32908  pmtrto1cl  33054  fzto1st1  33057  fzto1st  33058  psgnfzto1st  33060  cycpmco2lem6  33086  cycpmco2lem7  33087  cycpmrn  33098  qsidomlem1  33399  krull  33426  ply1degltel  33536  ply1degltlss  33538  constrnegcl  33729  constrdircl  33731  iconstr  33732  constrrecl  33735  constrmulcl  33737  constrreinvcl  33738  constrresqrtcl  33743  cos9thpiminplylem1  33748  cos9thpiminply  33754  cos9thpinconstrlem1  33755  1smat1  33770  submateqlem1  33773  madjusmdetlem2  33794  unitdivcld  33867  sqsscirc1  33874  esumdivc  34049  dya2ub  34237  dya2iocress  34241  dya2iocbrsiga  34242  dya2icobrsiga  34243  dya2icoseg  34244  dya2iocucvr  34251  sxbrsigalem2  34253  fibp1  34368  probmeasb  34397  dstrvprob  34439  dstfrvunirn  34442  ballotlemfc0  34460  ballotlemfcc  34461  ballotlemsgt1  34478  ballotlemsel1i  34480  ballotlemfrcn0  34497  signsply0  34518  itgexpif  34573  reprlt  34586  chtvalz  34596  breprexplemc  34599  breprexp  34600  circlemeth  34607  tgoldbachgnn  34626  acycgr1v  35121  subfaclim  35160  cvmliftlem2  35258  cvmliftlem13  35268  snmlff  35301  bccolsum  35711  faclim  35718  nn0prpwlem  36295  dnibndlem10  36460  dnibndlem12  36462  knoppcnlem4  36469  unblimceq0  36480  knoppndvlem1  36485  knoppndvlem2  36486  knoppndvlem3  36487  knoppndvlem7  36491  knoppndvlem11  36495  knoppndvlem12  36496  knoppndvlem14  36498  knoppndvlem15  36499  knoppndvlem17  36501  knoppndvlem18  36502  knoppndvlem20  36504  irrdiff  37299  poimirlem6  37605  poimirlem7  37606  poimirlem15  37614  poimirlem19  37618  poimirlem29  37628  poimirlem30  37629  poimirlem31  37630  poimirlem32  37631  broucube  37633  itg2addnclem2  37651  itg2addnclem3  37652  areacirclem1  37687  areacirclem4  37690  incsequz  37727  totbndbnd  37768  bfplem2  37802  resdvopclptsd  42001  lcmineqlem2  42003  lcmineqlem3  42004  lcmineqlem10  42011  lcmineqlem12  42013  lcmineqlem15  42016  lcmineqlem18  42019  lcmineqlem19  42020  lcmineqlem20  42021  lcmineqlem22  42023  lcmineqlem23  42024  3lexlogpow5ineq2  42028  3lexlogpow5ineq4  42029  3lexlogpow5ineq3  42030  3lexlogpow2ineq1  42031  3lexlogpow2ineq2  42032  3lexlogpow5ineq5  42033  aks4d1lem1  42035  dvrelog2  42037  dvrelog3  42038  dvrelog2b  42039  dvrelogpow2b  42041  aks4d1p1p3  42042  aks4d1p1p2  42043  aks4d1p1p4  42044  aks4d1p1p6  42046  aks4d1p1p7  42047  aks4d1p1p5  42048  aks4d1p1  42049  aks4d1p2  42050  aks4d1p3  42051  aks4d1p5  42053  aks4d1p6  42054  aks4d1p7d1  42055  aks4d1p7  42056  aks4d1p8d2  42058  aks4d1p8d3  42059  aks4d1p8  42060  aks4d1p9  42061  posbezout  42073  primrootlekpowne0  42078  primrootspoweq0  42079  aks6d1c1  42089  aks6d1c2p2  42092  hashscontpow1  42094  aks6d1c3  42096  aks6d1c2lem4  42100  aks6d1c2  42103  2np3bcnp1  42117  2ap1caineq  42118  sticksstones6  42124  sticksstones7  42125  sticksstones10  42128  sticksstones12a  42130  sticksstones12  42131  sticksstones22  42141  aks6d1c6lem3  42145  aks6d1c6lem4  42146  bcled  42151  bcle2d  42152  aks6d1c7lem1  42153  aks6d1c7lem2  42154  unitscyglem2  42169  unitscyglem4  42171  unitscyglem5  42172  aks5lem8  42174  sn-1ne2  42238  redvmptabs  42333  sn-00idlem2  42372  sn-0ne2  42379  rei4  42397  sn-rereccld  42421  rerecid  42422  sn-0tie0  42424  sn-nnne0  42433  mulgt0b1d  42445  sn-ltmulgt11d  42447  sn-0lt1  42448  sn-mulgt1d  42452  fimgmcyc  42507  flt4lem7  42632  fltnlta  42636  3cubeslem1  42657  3cubeslem3r  42660  3cubeslem4  42662  lzenom  42743  irrapxlem1  42795  irrapxlem2  42796  irrapxlem4  42798  irrapxlem5  42799  pellexlem2  42803  pell1qrge1  42843  pell1qr1  42844  elpell1qr2  42845  pell14qrgapw  42849  pellfundgt1  42856  pellfundglb  42858  pellfundex  42859  pellfundrp  42861  pellfundne1  42862  rmspecsqrtnq  42879  rmspecnonsq  42880  rmspecfund  42882  rmspecpos  42889  monotoddzzfi  42915  rmygeid  42937  areaquad  43189  imo72b2lem0  44138  imo72b2lem1  44142  imo72b2  44145  cvgdvgrat  44286  radcnvrat  44287  hashnzfzclim  44295  lhe4.4ex1a  44302  binomcxplemnn0  44322  binomcxplemdvbinom  44326  binomcxplemnotnn0  44329  oddfl  45260  abscosbd  45261  zltlesub  45267  abssinbd  45277  monoords  45279  fzisoeu  45282  fzdifsuc2  45292  suplesup  45319  xralrple2  45334  infxr  45347  infleinflem2  45351  reclt0d  45367  xrralrecnnge  45370  sqrlearg  45535  iooiinioc  45538  fmul01  45562  fmul01lt1lem1  45566  fmul01lt1lem2  45567  climsuselem1  45589  sumnnodd  45612  0ellimcdiv  45631  dvmptidg  45899  dvcosax  45908  ioodvbdlimc1lem1  45913  ioodvbdlimc1lem2  45914  ioodvbdlimc2lem  45916  dvxpaek  45922  dvnmul  45925  iblspltprt  45955  itgspltprt  45961  stoweidlem5  45987  stoweidlem7  45989  stoweidlem10  45992  stoweidlem11  45993  stoweidlem12  45994  stoweidlem13  45995  stoweidlem14  45996  stoweidlem16  45998  stoweidlem18  46000  stoweidlem20  46002  stoweidlem24  46006  stoweidlem25  46007  stoweidlem34  46016  stoweidlem36  46018  stoweidlem38  46020  stoweidlem40  46022  stoweidlem41  46023  stoweidlem42  46024  stoweidlem45  46027  stoweidlem51  46033  stoweidlem60  46042  wallispilem3  46049  wallispilem4  46050  wallispilem5  46051  wallispi  46052  wallispi2lem1  46053  wallispi2lem2  46054  wallispi2  46055  stirlinglem1  46056  stirlinglem3  46058  stirlinglem5  46060  stirlinglem6  46061  stirlinglem7  46062  stirlinglem8  46063  stirlinglem10  46065  stirlinglem11  46066  stirlinglem12  46067  stirlinglem13  46068  stirlinglem15  46070  dirker2re  46074  dirkerval2  46076  dirkerre  46077  dirkertrigeqlem1  46080  dirkertrigeqlem3  46082  dirkeritg  46084  dirkercncflem1  46085  dirkercncflem2  46086  dirkercncflem4  46088  fourierdlem5  46094  fourierdlem6  46095  fourierdlem11  46100  fourierdlem15  46104  fourierdlem19  46108  fourierdlem20  46109  fourierdlem24  46113  fourierdlem26  46115  fourierdlem28  46117  fourierdlem30  46119  fourierdlem39  46128  fourierdlem41  46130  fourierdlem43  46132  fourierdlem47  46135  fourierdlem48  46136  fourierdlem56  46144  fourierdlem60  46148  fourierdlem61  46149  fourierdlem62  46150  fourierdlem64  46152  fourierdlem65  46153  fourierdlem66  46154  fourierdlem68  46156  fourierdlem73  46161  fourierdlem78  46166  fourierdlem79  46167  fourierdlem87  46175  fourierdlem103  46191  fourierdlem104  46192  sqwvfoura  46210  fouriersw  46213  etransclem4  46220  etransclem23  46239  etransclem24  46240  etransclem31  46247  etransclem32  46248  etransclem35  46251  etransclem41  46257  etransclem46  46262  etransclem48  46264  etransc  46265  ioorrnopnxrlem  46288  nnfoctbdjlem  46437  iundjiun  46442  hoidmvlelem1  46577  hoidmvlelem2  46578  hoidmvlelem3  46579  hoidmvlelem4  46580  ovnhoilem1  46583  vonioolem2  46663  vonicclem2  46666  pimrecltneg  46706  smfrec  46771  smfmullem1  46773  smfmullem2  46774  smfdiv  46779  sigaradd  46848  ormkglobd  46857  cjnpoly  46874  p1lep2  47285  zm1nn  47287  ceilhalfgt1  47314  2tceilhalfelfzo1  47317  ceilbi  47318  rehalfge1  47320  ceilhalfnn  47321  addmodne  47329  m1mod0mod1  47339  m1modmmod  47343  difmodm1lt  47344  modmknepk  47347  modp2nep1  47352  modm1nem2  47354  iccpartiltu  47407  iccpartlt  47409  iccpartgt  47412  fmtnoge3  47515  fmtnodvds  47529  fmtnoprmfac2lem1  47551  2pwp1prm  47574  flsqrt  47578  sfprmdvdsmersenne  47588  lighneallem2  47591  lighneallem4a  47593  proththdlem  47598  proththd  47599  nnoALTV  47680  bgoldbtbndlem4  47793  gpgprismgrusgra  48043  gpgedgvtx0  48046  gpgvtxedg0  48048  gpg5nbgrvtx03starlem2  48054  gpg3kgrtriexlem4  48071  gpg3kgrtriexlem6  48073  cznnring  48247  divge1b  48498  divgt1b  48499  nn0eo  48514  regt1loggt0  48522  rege1logbrege0  48544  logblt1b  48550  fllog2  48554  nnolog2flm1  48576  dignn0flhalflem1  48601  rrxlinesc  48721  rrxlinec  48722  eenglngeehlnmlem1  48723  eenglngeehlnmlem2  48724  line2ylem  48737  line2  48738  line2xlem  48739  reseccl  49739  recsccl  49740  amgmwlem  49788  amgmlemALT  49789