Theorem 1red 11145

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  1c1 11039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370

This theorem is referenced by:  recgt0  12001  mulgt1  12017  ltrec  12038  nnne0  12211  nn0p1gt0  12466  nn0ge2m1nn  12507  nn0le2is012  12593  suprzcl  12609  ledivge1le  13015  ge2halflem1  13059  qbtwnre  13151  lincmb01cmp  13448  iccf1o  13449  xov1plusxeqvd  13451  zltaddlt1le  13458  nnge2recico01  13460  fznatpl1  13532  elfz1b  13547  elfzo0subge1  13660  fzonn0p1p1  13699  elfznelfzo  13728  elfznelfzob  13729  fladdz  13784  2tnp1ge0ge0  13788  flhalf  13789  ltdifltdiv  13793  fldiv4lem1div2uz2  13795  mulp1mod1  13873  m1modge3gt1  13880  modltm1p1mod  13885  addmodlteq  13908  ltexp2a  14128  expcan  14131  ltexp2  14132  leexp2  14133  leexp2a  14134  leexp2r  14136  nnlesq  14167  bernneq3  14193  expnbnd  14194  expnlbnd2  14196  expnngt1  14203  fzsdom2  14390  wrdlenge2n0  14514  swrd2lsw  14914  2swrd2eqwrdeq  14915  01sqrexlem7  15210  rddif  15303  reccn2  15559  rlimo1  15579  o1fsum  15776  abscvgcvg  15782  climcndslem1  15814  flo1  15819  harmonic  15824  geomulcvg  15841  fprodrecl  15918  fprodreclf  15924  fprodle  15961  bpoly4  16024  efcllem  16042  efgt1  16083  tanhlt1  16127  sinltx  16156  eirrlem  16171  p1modz1  16228  mod2eq1n2dvds  16316  oddge22np1  16318  ltoddhalfle  16330  nn0o1gt2  16350  nno  16351  nn0oddm1d2  16354  nnoddm1d2  16355  bitsfzolem  16403  bitsfzo  16404  bitsmod  16405  bitscmp  16407  bitsinv1lem  16410  smuval2  16451  coprmgcdb  16618  prmind2  16654  dvdsnprmd  16659  2mulprm  16662  isprm5  16677  isprm7  16678  divdenle  16719  zsqrtelqelz  16728  fermltl  16754  odzdvds  16766  modprm0  16776  iserodd  16806  difsqpwdvds  16858  pcfaclem  16869  prmreclem1  16887  4sqlem11  16926  4sqlem12  16927  ramub1lem1  16997  prmgaplem8  17029  2expltfac  17063  chnccat  18592  pgpfaclem2  20059  znidomb  21541  psdmvr  22135  chfacfisf  22819  chfacfisfcpmat  22820  chfacfscmulgsum  22825  chfacfpmmulgsum  22829  nrginvrcnlem  24656  nmoid  24707  xrsmopn  24778  metnrmlem1a  24824  iihalf2cn  24901  iccpnfhmeo  24912  lebnumii  24933  htpycc  24947  pcohtpylem  24986  pcoass  24991  pcorevlem  24993  nmhmcn  25087  cncmet  25289  ovoliunlem1  25469  dyadmaxlem  25564  vitalilem2  25576  mbfi1fseqlem6  25687  itg2mulc  25714  itg2monolem1  25717  itg2monolem3  25719  dveflem  25946  mvth  25959  dvlipcn  25961  lhop1lem  25980  dvfsumlem1  25993  dvfsumlem2  25994  dvfsumlem3  25995  dvfsumlem4  25996  dvfsum2  26001  fta1glem2  26134  plyeq0lem  26175  fta1lem  26273  vieta1lem2  26277  aalioulem3  26300  aalioulem4  26301  radcnvlem1  26378  radcnvlem2  26379  dvradcnv  26386  abelthlem2  26397  abelthlem5  26400  abelthlem7  26403  abelth2  26407  cos02pilt1  26490  cosne0  26493  rplogcl  26568  logdivlti  26584  logno1  26600  dvlog2lem  26616  advlog  26618  logtayllem  26623  cxplt  26658  cxple  26659  cxpaddlelem  26715  cxpaddle  26716  rtprmirr  26724  relogbf  26755  logbgt0b  26757  isosctrlem1  26782  isosctrlem2  26783  chordthmlem4  26799  heron  26802  atanlogaddlem  26877  bndatandm  26893  leibpi  26906  log2tlbnd  26909  birthdaylem3  26917  rlimcnp  26929  rlimcnp2  26930  efrlim  26933  cxp2limlem  26939  cxp2lim  26940  divsqrtsumo1  26947  jensenlem2  26951  logdiflbnd  26958  fsumharmonic  26975  lgamgulmlem2  26993  lgamgulmlem3  26994  lgamgulmlem4  26995  lgamgulmlem5  26996  lgamgulmlem6  26997  lgamcvg2  27018  regamcl  27024  wilthlem2  27032  ftalem2  27037  basellem9  27052  vma1  27129  ppieq0  27139  mumullem2  27143  fsumfldivdiaglem  27152  chpeq0  27171  chtub  27175  chpval2  27181  chpchtsum  27182  chpub  27183  logfacrlim  27187  logexprlim  27188  mersenne  27190  perfectlem2  27193  dchrelbas4  27206  bcmono  27240  bposlem1  27247  bposlem2  27248  zabsle1  27259  lgslem3  27262  lgsmod  27286  lgsdir2lem4  27291  lgsdirprm  27294  gausslemma2dlem1a  27328  gausslemma2d  27337  lgsquadlem2  27344  2sqlem8  27389  chebbnd1lem1  27432  chebbnd1lem2  27433  chtppilimlem1  27436  chebbnd2  27440  chto1lb  27441  chpchtlim  27442  chpo1ubb  27444  vmadivsum  27445  rplogsumlem1  27447  rpvmasumlem  27450  dchrisumlem3  27454  dchrmusumlema  27456  dchrmusum2  27457  dchrvmasumlem2  27461  dchrvmasumlem3  27462  dchrvmasumiflem1  27464  dchrvmasumiflem2  27465  dchrisum0flblem1  27471  dchrisum0flblem2  27472  dchrisum0fno1  27474  dchrisum0re  27476  dchrisum0lema  27477  dchrisum0lem1b  27478  dchrisum0lem2a  27480  dchrisum0lem2  27481  dchrisum0lem3  27482  rplogsum  27490  dirith2  27491  mudivsum  27493  mulogsumlem  27494  mulogsum  27495  mulog2sumlem1  27497  mulog2sumlem2  27498  vmalogdivsum2  27501  vmalogdivsum  27502  2vmadivsumlem  27503  log2sumbnd  27507  selberglem2  27509  selberg2lem  27513  chpdifbnd  27518  selberg3lem1  27520  selberg3  27522  selberg4lem1  27523  selberg4  27524  pntrmax  27527  pntrsumo1  27528  pntrsumbnd  27529  selberg3r  27532  selberg4r  27533  selberg34r  27534  pntrlog2bndlem1  27540  pntrlog2bndlem2  27541  pntrlog2bndlem3  27542  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntrlog2bndlem6  27546  pntrlog2bnd  27547  pntpbnd1a  27548  pntpbnd1  27549  pntibndlem2a  27553  pntibndlem2  27554  pntibnd  27556  pntlemc  27558  pntlemg  27561  pntlemr  27565  pntlemk  27569  pnt  27577  qabvle  27588  ostth2lem3  27598  ostth2  27600  trgcgrg  28583  tgcgr4  28599  ttgcontlem1  28953  axpaschlem  29009  axlowdimlem16  29026  axcontlem2  29034  axcontlem7  29039  nbusgrvtxm1  29448  upgrewlkle2  29675  pthdlem1  29834  crctcshwlkn0lem3  29880  crctcshwlkn0lem5  29882  wwlksm1edg  29949  wwlksnextproplem2  29978  clwlkclwwlklem2fv1  30065  clwlkclwwlklem2fv2  30066  clwlkclwwlklem2  30070  clwlkclwwlk2  30073  clwwisshclwwslem  30084  clwwlkf1  30119  clwwlkext2edg  30126  clwlknf1oclwwlknlem1  30151  clwwlknonex2lem2  30178  numclwwlk7  30461  frgrreggt1  30463  frgrogt3nreg  30467  smcnlem  30768  nmoub3i  30844  blocnilem  30875  ubthlem2  30942  minvecolem4  30951  htthlem  30988  nmcexi  32097  nmopcoi  32166  stadd3i  32319  cdj1i  32504  nnmulge  32812  receqid  32817  nndiffz1  32859  fzsplit3  32866  nexple  32917  indf1o  32924  wrdt2ind  33013  pmtrto1cl  33160  fzto1st1  33163  fzto1st  33164  psgnfzto1st  33166  cycpmco2lem6  33192  cycpmco2lem7  33193  cycpmrn  33204  qsidomlem1  33512  krull  33539  ply1degltel  33654  ply1degltlss  33656  constrnegcl  33907  constrdircl  33909  iconstr  33910  constrrecl  33913  constrmulcl  33915  constrreinvcl  33916  constrresqrtcl  33921  cos9thpiminplylem1  33926  cos9thpiminply  33932  cos9thpinconstrlem1  33933  1smat1  33948  submateqlem1  33951  madjusmdetlem2  33972  unitdivcld  34045  sqsscirc1  34052  esumdivc  34227  dya2ub  34414  dya2iocress  34418  dya2iocbrsiga  34419  dya2icobrsiga  34420  dya2icoseg  34421  dya2iocucvr  34428  sxbrsigalem2  34430  fibp1  34545  probmeasb  34574  dstrvprob  34616  dstfrvunirn  34619  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemsgt1  34655  ballotlemsel1i  34657  ballotlemfrcn0  34674  signsply0  34695  itgexpif  34750  reprlt  34763  chtvalz  34773  breprexplemc  34776  breprexp  34777  circlemeth  34784  tgoldbachgnn  34803  acycgr1v  35331  subfaclim  35370  cvmliftlem2  35468  cvmliftlem13  35478  snmlff  35511  bccolsum  35921  faclim  35928  nn0prpwlem  36504  dnibndlem10  36747  dnibndlem12  36749  knoppcnlem4  36756  unblimceq0  36767  knoppndvlem1  36772  knoppndvlem2  36773  knoppndvlem3  36774  knoppndvlem7  36778  knoppndvlem11  36782  knoppndvlem12  36783  knoppndvlem14  36785  knoppndvlem15  36786  knoppndvlem17  36788  knoppndvlem18  36789  knoppndvlem20  36791  irrdiff  37640  poimirlem6  37947  poimirlem7  37948  poimirlem15  37956  poimirlem19  37960  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimirlem32  37973  broucube  37975  itg2addnclem2  37993  itg2addnclem3  37994  areacirclem1  38029  areacirclem4  38032  incsequz  38069  totbndbnd  38110  bfplem2  38144  resdvopclptsd  42467  lcmineqlem2  42469  lcmineqlem3  42470  lcmineqlem10  42477  lcmineqlem12  42479  lcmineqlem15  42482  lcmineqlem18  42485  lcmineqlem19  42486  lcmineqlem20  42487  lcmineqlem22  42489  lcmineqlem23  42490  3lexlogpow5ineq2  42494  3lexlogpow5ineq4  42495  3lexlogpow5ineq3  42496  3lexlogpow2ineq1  42497  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  aks4d1lem1  42501  dvrelog2  42503  dvrelog3  42504  dvrelog2b  42505  dvrelogpow2b  42507  aks4d1p1p3  42508  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p1  42515  aks4d1p2  42516  aks4d1p3  42517  aks4d1p5  42519  aks4d1p6  42520  aks4d1p7d1  42521  aks4d1p7  42522  aks4d1p8d2  42524  aks4d1p8d3  42525  aks4d1p8  42526  aks4d1p9  42527  posbezout  42539  primrootlekpowne0  42544  primrootspoweq0  42545  aks6d1c1  42555  aks6d1c2p2  42558  hashscontpow1  42560  aks6d1c3  42562  aks6d1c2lem4  42566  aks6d1c2  42569  2np3bcnp1  42583  2ap1caineq  42584  sticksstones6  42590  sticksstones7  42591  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  sticksstones22  42607  aks6d1c6lem3  42611  aks6d1c6lem4  42612  bcled  42617  bcle2d  42618  aks6d1c7lem1  42619  aks6d1c7lem2  42620  unitscyglem2  42635  unitscyglem4  42637  unitscyglem5  42638  aks5lem8  42640  sn-1ne2  42703  redvmptabs  42792  sn-00idlem2  42831  sn-0ne2  42838  rei4  42856  rediveq1d  42883  sn-rediv1d  42884  sn-rereccld  42887  rerecne0d  42888  rerecidd  42889  rerecrecd  42891  sn-0tie0  42896  sn-nnne0  42905  mulgt0b1d  42917  sn-ltmulgt11d  42919  sn-0lt1  42920  sn-mulgt1d  42924  fimgmcyc  42979  flt4lem7  43092  fltnlta  43096  3cubeslem1  43116  3cubeslem3r  43119  3cubeslem4  43121  lzenom  43202  irrapxlem1  43250  irrapxlem2  43251  irrapxlem4  43253  irrapxlem5  43254  pellexlem2  43258  pell1qrge1  43298  pell1qr1  43299  elpell1qr2  43300  pell14qrgapw  43304  pellfundgt1  43311  pellfundglb  43313  pellfundex  43314  pellfundrp  43316  pellfundne1  43317  rmspecsqrtnq  43334  rmspecnonsq  43335  rmspecfund  43337  rmspecpos  43344  monotoddzzfi  43370  rmygeid  43392  areaquad  43644  imo72b2lem0  44592  imo72b2lem1  44596  imo72b2  44599  cvgdvgrat  44740  radcnvrat  44741  hashnzfzclim  44749  lhe4.4ex1a  44756  binomcxplemnn0  44776  binomcxplemdvbinom  44780  binomcxplemnotnn0  44783  oddfl  45711  abscosbd  45712  zltlesub  45718  abssinbd  45728  monoords  45730  fzisoeu  45733  fzdifsuc2  45743  suplesup  45769  xralrple2  45784  infxr  45796  infleinflem2  45800  reclt0d  45816  xrralrecnnge  45819  sqrlearg  45983  iooiinioc  45986  fmul01  46010  fmul01lt1lem1  46014  fmul01lt1lem2  46015  climsuselem1  46037  sumnnodd  46060  0ellimcdiv  46077  dvmptidg  46345  dvcosax  46354  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvxpaek  46368  dvnmul  46371  iblspltprt  46401  itgspltprt  46407  stoweidlem5  46433  stoweidlem7  46435  stoweidlem10  46438  stoweidlem11  46439  stoweidlem12  46440  stoweidlem13  46441  stoweidlem14  46442  stoweidlem16  46444  stoweidlem18  46446  stoweidlem20  46448  stoweidlem24  46452  stoweidlem25  46453  stoweidlem34  46462  stoweidlem36  46464  stoweidlem38  46466  stoweidlem40  46468  stoweidlem41  46469  stoweidlem42  46470  stoweidlem45  46473  stoweidlem51  46479  stoweidlem60  46488  wallispilem3  46495  wallispilem4  46496  wallispilem5  46497  wallispi  46498  wallispi2lem1  46499  wallispi2lem2  46500  wallispi2  46501  stirlinglem1  46502  stirlinglem3  46504  stirlinglem5  46506  stirlinglem6  46507  stirlinglem7  46508  stirlinglem8  46509  stirlinglem10  46511  stirlinglem11  46512  stirlinglem12  46513  stirlinglem13  46514  stirlinglem15  46516  dirker2re  46520  dirkerval2  46522  dirkerre  46523  dirkertrigeqlem1  46526  dirkertrigeqlem3  46528  dirkeritg  46530  dirkercncflem1  46531  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem5  46540  fourierdlem6  46541  fourierdlem11  46546  fourierdlem15  46550  fourierdlem19  46554  fourierdlem20  46555  fourierdlem24  46559  fourierdlem26  46561  fourierdlem28  46563  fourierdlem30  46565  fourierdlem39  46574  fourierdlem41  46576  fourierdlem43  46578  fourierdlem47  46581  fourierdlem48  46582  fourierdlem56  46590  fourierdlem60  46594  fourierdlem61  46595  fourierdlem62  46596  fourierdlem64  46598  fourierdlem65  46599  fourierdlem66  46600  fourierdlem68  46602  fourierdlem73  46607  fourierdlem78  46612  fourierdlem79  46613  fourierdlem87  46621  fourierdlem103  46637  fourierdlem104  46638  sqwvfoura  46656  fouriersw  46659  etransclem4  46666  etransclem23  46685  etransclem24  46686  etransclem31  46693  etransclem32  46694  etransclem35  46697  etransclem41  46703  etransclem46  46708  etransclem48  46710  etransc  46711  ioorrnopnxrlem  46734  nnfoctbdjlem  46883  iundjiun  46888  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  ovnhoilem1  47029  vonioolem2  47109  vonicclem2  47112  pimrecltneg  47152  smfrec  47217  smfmullem1  47219  smfmullem2  47220  smfdiv  47225  sigaradd  47294  ormkglobd  47305  cjnpoly  47337  p1lep2  47748  zm1nn  47750  ceilhalfgt1  47781  2tceilhalfelfzo1  47784  ceilbi  47785  rehalfge1  47787  ceilhalfnn  47788  flmrecm1  47791  addmodne  47798  m1mod0mod1  47808  m1modmmod  47812  difmodm1lt  47813  modmknepk  47816  modp2nep1  47821  modm1nem2  47823  2timesltsqm1  47827  muldvdsfacm1  47835  iccpartiltu  47882  iccpartlt  47884  iccpartgt  47887  fmtnoge3  47993  fmtnodvds  48007  fmtnoprmfac2lem1  48029  2pwp1prm  48052  flsqrt  48056  sfprmdvdsmersenne  48066  lighneallem2  48069  lighneallem4a  48071  proththdlem  48076  proththd  48077  nprmdvdsfacm1lem4  48086  nnoALTV  48171  bgoldbtbndlem4  48284  gpgprismgrusgra  48534  gpgedgvtx0  48537  gpgvtxedg0  48539  gpg5nbgrvtx03starlem2  48545  gpg3kgrtriexlem4  48562  gpg3kgrtriexlem6  48564  cznnring  48738  divge1b  48988  divgt1b  48989  nn0eo  49004  regt1loggt0  49012  rege1logbrege0  49034  logblt1b  49040  fllog2  49044  nnolog2flm1  49066  dignn0flhalflem1  49091  rrxlinesc  49211  rrxlinec  49212  eenglngeehlnmlem1  49213  eenglngeehlnmlem2  49214  line2ylem  49227  line2  49228  line2xlem  49229  reseccl  50228  recsccl  50229  amgmwlem  50277  amgmlemALT  50278