Theorem 1red 11110

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 11002  1c1 11004

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 2113  ax-9 2121  ax-ext 2703  ax-1cn 11061  ax-icn 11062  ax-addcl 11063  ax-mulcl 11065  ax-mulrcl 11066  ax-i2m1 11071  ax-1ne0 11072  ax-rrecex 11075  ax-cnre 11076

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 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  recgt0  11964  mulgt1  11980  ltrec  12001  nnne0  12156  nn0p1gt0  12407  nn0ge2m1nn  12448  nn0le2is012  12534  suprzcl  12550  ledivge1le  12960  ge2halflem1  13004  qbtwnre  13095  lincmb01cmp  13392  iccf1o  13393  xov1plusxeqvd  13395  zltaddlt1le  13402  fznatpl1  13475  elfz1b  13490  elfzo0subge1  13602  fzonn0p1p1  13641  elfznelfzo  13670  elfznelfzob  13671  fladdz  13726  2tnp1ge0ge0  13730  flhalf  13731  ltdifltdiv  13735  fldiv4lem1div2uz2  13737  mulp1mod1  13815  m1modge3gt1  13822  modltm1p1mod  13827  addmodlteq  13850  ltexp2a  14070  expcan  14073  ltexp2  14074  leexp2  14075  leexp2a  14076  leexp2r  14078  nnlesq  14109  bernneq3  14135  expnbnd  14136  expnlbnd2  14138  expnngt1  14145  fzsdom2  14332  wrdlenge2n0  14456  swrd2lsw  14856  2swrd2eqwrdeq  14857  01sqrexlem7  15152  rddif  15245  reccn2  15501  rlimo1  15521  o1fsum  15717  abscvgcvg  15723  climcndslem1  15753  flo1  15758  harmonic  15763  geomulcvg  15780  fprodrecl  15857  fprodreclf  15863  fprodle  15900  bpoly4  15963  efcllem  15981  efgt1  16022  tanhlt1  16066  sinltx  16095  eirrlem  16110  p1modz1  16167  mod2eq1n2dvds  16255  oddge22np1  16257  ltoddhalfle  16269  nn0o1gt2  16289  nno  16290  nn0oddm1d2  16293  nnoddm1d2  16294  bitsfzolem  16342  bitsfzo  16343  bitsmod  16344  bitscmp  16346  bitsinv1lem  16349  smuval2  16390  coprmgcdb  16557  prmind2  16593  dvdsnprmd  16598  2mulprm  16601  isprm5  16615  isprm7  16616  divdenle  16657  zsqrtelqelz  16666  fermltl  16692  odzdvds  16704  modprm0  16714  iserodd  16744  difsqpwdvds  16796  pcfaclem  16807  prmreclem1  16825  4sqlem11  16864  4sqlem12  16865  ramub1lem1  16935  prmgaplem8  16967  2expltfac  17001  chnccat  18529  pgpfaclem2  19994  znidomb  21496  psdmvr  22082  chfacfisf  22767  chfacfisfcpmat  22768  chfacfscmulgsum  22773  chfacfpmmulgsum  22777  nrginvrcnlem  24604  nmoid  24655  xrsmopn  24726  metnrmlem1a  24772  iihalf2cn  24854  iccpnfhmeo  24868  lebnumii  24890  htpycc  24904  pcohtpylem  24944  pcoass  24949  pcorevlem  24951  nmhmcn  25045  cncmet  25247  ovoliunlem1  25428  dyadmaxlem  25523  vitalilem2  25535  mbfi1fseqlem6  25646  itg2mulc  25673  itg2monolem1  25676  itg2monolem3  25678  dveflem  25908  mvth  25922  dvlipcn  25924  lhop1lem  25943  dvfsumlem1  25957  dvfsumlem2  25958  dvfsumlem2OLD  25959  dvfsumlem3  25960  dvfsumlem4  25961  dvfsum2  25966  fta1glem2  26099  plyeq0lem  26140  fta1lem  26240  vieta1lem2  26244  aalioulem3  26267  aalioulem4  26268  radcnvlem1  26347  radcnvlem2  26348  dvradcnv  26355  abelthlem2  26367  abelthlem5  26370  abelthlem7  26373  abelth2  26377  cos02pilt1  26460  cosne0  26463  rplogcl  26538  logdivlti  26554  logno1  26570  dvlog2lem  26586  advlog  26588  logtayllem  26593  cxplt  26628  cxple  26629  cxpaddlelem  26686  cxpaddle  26687  rtprmirr  26695  relogbf  26726  logbgt0b  26728  isosctrlem1  26753  isosctrlem2  26754  chordthmlem4  26770  heron  26773  atanlogaddlem  26848  bndatandm  26864  leibpi  26877  log2tlbnd  26880  birthdaylem3  26888  rlimcnp  26900  rlimcnp2  26901  efrlim  26904  efrlimOLD  26905  cxp2limlem  26911  cxp2lim  26912  divsqrtsumo1  26919  jensenlem2  26923  logdiflbnd  26930  fsumharmonic  26947  lgamgulmlem2  26965  lgamgulmlem3  26966  lgamgulmlem4  26967  lgamgulmlem5  26968  lgamgulmlem6  26969  lgamcvg2  26990  regamcl  26996  wilthlem2  27004  ftalem2  27009  basellem9  27024  vma1  27101  ppieq0  27111  mumullem2  27115  fsumfldivdiaglem  27124  chpeq0  27144  chtub  27148  chpval2  27154  chpchtsum  27155  chpub  27156  logfacrlim  27160  logexprlim  27161  mersenne  27163  perfectlem2  27166  dchrelbas4  27179  bcmono  27213  bposlem1  27220  bposlem2  27221  zabsle1  27232  lgslem3  27235  lgsmod  27259  lgsdir2lem4  27264  lgsdirprm  27267  gausslemma2dlem1a  27301  gausslemma2d  27310  lgsquadlem2  27317  2sqlem8  27362  chebbnd1lem1  27405  chebbnd1lem2  27406  chtppilimlem1  27409  chebbnd2  27413  chto1lb  27414  chpchtlim  27415  chpo1ubb  27417  vmadivsum  27418  rplogsumlem1  27420  rpvmasumlem  27423  dchrisumlem3  27427  dchrmusumlema  27429  dchrmusum2  27430  dchrvmasumlem2  27434  dchrvmasumlem3  27435  dchrvmasumiflem1  27437  dchrvmasumiflem2  27438  dchrisum0flblem1  27444  dchrisum0flblem2  27445  dchrisum0fno1  27447  dchrisum0re  27449  dchrisum0lema  27450  dchrisum0lem1b  27451  dchrisum0lem2a  27453  dchrisum0lem2  27454  dchrisum0lem3  27455  rplogsum  27463  dirith2  27464  mudivsum  27466  mulogsumlem  27467  mulogsum  27468  mulog2sumlem1  27470  mulog2sumlem2  27471  vmalogdivsum2  27474  vmalogdivsum  27475  2vmadivsumlem  27476  log2sumbnd  27480  selberglem2  27482  selberg2lem  27486  chpdifbnd  27491  selberg3lem1  27493  selberg3  27495  selberg4lem1  27496  selberg4  27497  pntrmax  27500  pntrsumo1  27501  pntrsumbnd  27502  selberg3r  27505  selberg4r  27506  selberg34r  27507  pntrlog2bndlem1  27513  pntrlog2bndlem2  27514  pntrlog2bndlem3  27515  pntrlog2bndlem4  27516  pntrlog2bndlem5  27517  pntrlog2bndlem6  27519  pntrlog2bnd  27520  pntpbnd1a  27521  pntpbnd1  27522  pntibndlem2a  27526  pntibndlem2  27527  pntibnd  27529  pntlemc  27531  pntlemg  27534  pntlemr  27538  pntlemk  27542  pnt  27550  qabvle  27561  ostth2lem3  27571  ostth2  27573  trgcgrg  28491  tgcgr4  28507  ttgcontlem1  28861  axpaschlem  28916  axlowdimlem16  28933  axcontlem2  28941  axcontlem7  28946  nbusgrvtxm1  29355  upgrewlkle2  29583  pthdlem1  29742  crctcshwlkn0lem3  29788  crctcshwlkn0lem5  29790  wwlksm1edg  29857  wwlksnextproplem2  29886  clwlkclwwlklem2fv1  29970  clwlkclwwlklem2fv2  29971  clwlkclwwlklem2  29975  clwlkclwwlk2  29978  clwwisshclwwslem  29989  clwwlkf1  30024  clwwlkext2edg  30031  clwlknf1oclwwlknlem1  30056  clwwlknonex2lem2  30083  numclwwlk7  30366  frgrreggt1  30368  frgrogt3nreg  30372  smcnlem  30672  nmoub3i  30748  blocnilem  30779  ubthlem2  30846  minvecolem4  30855  htthlem  30892  nmcexi  32001  nmopcoi  32070  stadd3i  32223  cdj1i  32408  nnmulge  32717  receqid  32723  nndiffz1  32764  fzsplit3  32771  nexple  32822  indf1o  32840  wrdt2ind  32929  pmtrto1cl  33063  fzto1st1  33066  fzto1st  33067  psgnfzto1st  33069  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmrn  33107  qsidomlem1  33412  krull  33439  ply1degltel  33550  ply1degltlss  33552  constrnegcl  33771  constrdircl  33773  iconstr  33774  constrrecl  33777  constrmulcl  33779  constrreinvcl  33780  constrresqrtcl  33785  cos9thpiminplylem1  33790  cos9thpiminply  33796  cos9thpinconstrlem1  33797  1smat1  33812  submateqlem1  33815  madjusmdetlem2  33836  unitdivcld  33909  sqsscirc1  33916  esumdivc  34091  dya2ub  34278  dya2iocress  34282  dya2iocbrsiga  34283  dya2icobrsiga  34284  dya2icoseg  34285  dya2iocucvr  34292  sxbrsigalem2  34294  fibp1  34409  probmeasb  34438  dstrvprob  34480  dstfrvunirn  34483  ballotlemfc0  34501  ballotlemfcc  34502  ballotlemsgt1  34519  ballotlemsel1i  34521  ballotlemfrcn0  34538  signsply0  34559  itgexpif  34614  reprlt  34627  chtvalz  34637  breprexplemc  34640  breprexp  34641  circlemeth  34648  tgoldbachgnn  34667  acycgr1v  35181  subfaclim  35220  cvmliftlem2  35318  cvmliftlem13  35328  snmlff  35361  bccolsum  35771  faclim  35778  nn0prpwlem  36355  dnibndlem10  36520  dnibndlem12  36522  knoppcnlem4  36529  unblimceq0  36540  knoppndvlem1  36545  knoppndvlem2  36546  knoppndvlem3  36547  knoppndvlem7  36551  knoppndvlem11  36555  knoppndvlem12  36556  knoppndvlem14  36558  knoppndvlem15  36559  knoppndvlem17  36561  knoppndvlem18  36562  knoppndvlem20  36564  irrdiff  37359  poimirlem6  37665  poimirlem7  37666  poimirlem15  37674  poimirlem19  37678  poimirlem29  37688  poimirlem30  37689  poimirlem31  37690  poimirlem32  37691  broucube  37693  itg2addnclem2  37711  itg2addnclem3  37712  areacirclem1  37747  areacirclem4  37750  incsequz  37787  totbndbnd  37828  bfplem2  37862  resdvopclptsd  42060  lcmineqlem2  42062  lcmineqlem3  42063  lcmineqlem10  42070  lcmineqlem12  42072  lcmineqlem15  42075  lcmineqlem18  42078  lcmineqlem19  42079  lcmineqlem20  42080  lcmineqlem22  42082  lcmineqlem23  42083  3lexlogpow5ineq2  42087  3lexlogpow5ineq4  42088  3lexlogpow5ineq3  42089  3lexlogpow2ineq1  42090  3lexlogpow2ineq2  42091  3lexlogpow5ineq5  42092  aks4d1lem1  42094  dvrelog2  42096  dvrelog3  42097  dvrelog2b  42098  dvrelogpow2b  42100  aks4d1p1p3  42101  aks4d1p1p2  42102  aks4d1p1p4  42103  aks4d1p1p6  42105  aks4d1p1p7  42106  aks4d1p1p5  42107  aks4d1p1  42108  aks4d1p2  42109  aks4d1p3  42110  aks4d1p5  42112  aks4d1p6  42113  aks4d1p7d1  42114  aks4d1p7  42115  aks4d1p8d2  42117  aks4d1p8d3  42118  aks4d1p8  42119  aks4d1p9  42120  posbezout  42132  primrootlekpowne0  42137  primrootspoweq0  42138  aks6d1c1  42148  aks6d1c2p2  42151  hashscontpow1  42153  aks6d1c3  42155  aks6d1c2lem4  42159  aks6d1c2  42162  2np3bcnp1  42176  2ap1caineq  42177  sticksstones6  42183  sticksstones7  42184  sticksstones10  42187  sticksstones12a  42189  sticksstones12  42190  sticksstones22  42200  aks6d1c6lem3  42204  aks6d1c6lem4  42205  bcled  42210  bcle2d  42211  aks6d1c7lem1  42212  aks6d1c7lem2  42213  unitscyglem2  42228  unitscyglem4  42230  unitscyglem5  42231  aks5lem8  42233  sn-1ne2  42297  redvmptabs  42392  sn-00idlem2  42431  sn-0ne2  42438  rei4  42456  sn-rereccld  42480  rerecid  42481  sn-0tie0  42483  sn-nnne0  42492  mulgt0b1d  42504  sn-ltmulgt11d  42506  sn-0lt1  42507  sn-mulgt1d  42511  fimgmcyc  42566  flt4lem7  42691  fltnlta  42695  3cubeslem1  42716  3cubeslem3r  42719  3cubeslem4  42721  lzenom  42802  irrapxlem1  42854  irrapxlem2  42855  irrapxlem4  42857  irrapxlem5  42858  pellexlem2  42862  pell1qrge1  42902  pell1qr1  42903  elpell1qr2  42904  pell14qrgapw  42908  pellfundgt1  42915  pellfundglb  42917  pellfundex  42918  pellfundrp  42920  pellfundne1  42921  rmspecsqrtnq  42938  rmspecnonsq  42939  rmspecfund  42941  rmspecpos  42948  monotoddzzfi  42974  rmygeid  42996  areaquad  43248  imo72b2lem0  44197  imo72b2lem1  44201  imo72b2  44204  cvgdvgrat  44345  radcnvrat  44346  hashnzfzclim  44354  lhe4.4ex1a  44361  binomcxplemnn0  44381  binomcxplemdvbinom  44385  binomcxplemnotnn0  44388  oddfl  45318  abscosbd  45319  zltlesub  45325  abssinbd  45335  monoords  45337  fzisoeu  45340  fzdifsuc2  45350  suplesup  45377  xralrple2  45392  infxr  45404  infleinflem2  45408  reclt0d  45424  xrralrecnnge  45427  sqrlearg  45592  iooiinioc  45595  fmul01  45619  fmul01lt1lem1  45623  fmul01lt1lem2  45624  climsuselem1  45646  sumnnodd  45669  0ellimcdiv  45686  dvmptidg  45954  dvcosax  45963  ioodvbdlimc1lem1  45968  ioodvbdlimc1lem2  45969  ioodvbdlimc2lem  45971  dvxpaek  45977  dvnmul  45980  iblspltprt  46010  itgspltprt  46016  stoweidlem5  46042  stoweidlem7  46044  stoweidlem10  46047  stoweidlem11  46048  stoweidlem12  46049  stoweidlem13  46050  stoweidlem14  46051  stoweidlem16  46053  stoweidlem18  46055  stoweidlem20  46057  stoweidlem24  46061  stoweidlem25  46062  stoweidlem34  46071  stoweidlem36  46073  stoweidlem38  46075  stoweidlem40  46077  stoweidlem41  46078  stoweidlem42  46079  stoweidlem45  46082  stoweidlem51  46088  stoweidlem60  46097  wallispilem3  46104  wallispilem4  46105  wallispilem5  46106  wallispi  46107  wallispi2lem1  46108  wallispi2lem2  46109  wallispi2  46110  stirlinglem1  46111  stirlinglem3  46113  stirlinglem5  46115  stirlinglem6  46116  stirlinglem7  46117  stirlinglem8  46118  stirlinglem10  46120  stirlinglem11  46121  stirlinglem12  46122  stirlinglem13  46123  stirlinglem15  46125  dirker2re  46129  dirkerval2  46131  dirkerre  46132  dirkertrigeqlem1  46135  dirkertrigeqlem3  46137  dirkeritg  46139  dirkercncflem1  46140  dirkercncflem2  46141  dirkercncflem4  46143  fourierdlem5  46149  fourierdlem6  46150  fourierdlem11  46155  fourierdlem15  46159  fourierdlem19  46163  fourierdlem20  46164  fourierdlem24  46168  fourierdlem26  46170  fourierdlem28  46172  fourierdlem30  46174  fourierdlem39  46183  fourierdlem41  46185  fourierdlem43  46187  fourierdlem47  46190  fourierdlem48  46191  fourierdlem56  46199  fourierdlem60  46203  fourierdlem61  46204  fourierdlem62  46205  fourierdlem64  46207  fourierdlem65  46208  fourierdlem66  46209  fourierdlem68  46211  fourierdlem73  46216  fourierdlem78  46221  fourierdlem79  46222  fourierdlem87  46230  fourierdlem103  46246  fourierdlem104  46247  sqwvfoura  46265  fouriersw  46268  etransclem4  46275  etransclem23  46294  etransclem24  46295  etransclem31  46302  etransclem32  46303  etransclem35  46306  etransclem41  46312  etransclem46  46317  etransclem48  46319  etransc  46320  ioorrnopnxrlem  46343  nnfoctbdjlem  46492  iundjiun  46497  hoidmvlelem1  46632  hoidmvlelem2  46633  hoidmvlelem3  46634  hoidmvlelem4  46635  ovnhoilem1  46638  vonioolem2  46718  vonicclem2  46721  pimrecltneg  46761  smfrec  46826  smfmullem1  46828  smfmullem2  46829  smfdiv  46834  sigaradd  46903  ormkglobd  46912  cjnpoly  46919  p1lep2  47330  zm1nn  47332  ceilhalfgt1  47359  2tceilhalfelfzo1  47362  ceilbi  47363  rehalfge1  47365  ceilhalfnn  47366  addmodne  47374  m1mod0mod1  47384  m1modmmod  47388  difmodm1lt  47389  modmknepk  47392  modp2nep1  47397  modm1nem2  47399  iccpartiltu  47452  iccpartlt  47454  iccpartgt  47457  fmtnoge3  47560  fmtnodvds  47574  fmtnoprmfac2lem1  47596  2pwp1prm  47619  flsqrt  47623  sfprmdvdsmersenne  47633  lighneallem2  47636  lighneallem4a  47638  proththdlem  47643  proththd  47644  nnoALTV  47725  bgoldbtbndlem4  47838  gpgprismgrusgra  48088  gpgedgvtx0  48091  gpgvtxedg0  48093  gpg5nbgrvtx03starlem2  48099  gpg3kgrtriexlem4  48116  gpg3kgrtriexlem6  48118  cznnring  48292  divge1b  48543  divgt1b  48544  nn0eo  48559  regt1loggt0  48567  rege1logbrege0  48589  logblt1b  48595  fllog2  48599  nnolog2flm1  48621  dignn0flhalflem1  48646  rrxlinesc  48766  rrxlinec  48767  eenglngeehlnmlem1  48768  eenglngeehlnmlem2  48769  line2ylem  48782  line2  48783  line2xlem  48784  reseccl  49784  recsccl  49785  amgmwlem  49833  amgmlemALT  49834