Theorem 1red 11137

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11029  1c1 11031

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 2709  ax-1cn 11088  ax-icn 11089  ax-addcl 11090  ax-mulcl 11092  ax-mulrcl 11093  ax-i2m1 11098  ax-1ne0 11099  ax-rrecex 11102  ax-cnre 11103

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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7363

This theorem is referenced by:  recgt0  11991  mulgt1  12007  ltrec  12028  nnne0  12183  nn0p1gt0  12434  nn0ge2m1nn  12475  nn0le2is012  12560  suprzcl  12576  ledivge1le  12982  ge2halflem1  13026  qbtwnre  13118  lincmb01cmp  13415  iccf1o  13416  xov1plusxeqvd  13418  zltaddlt1le  13425  fznatpl1  13498  elfz1b  13513  elfzo0subge1  13625  fzonn0p1p1  13664  elfznelfzo  13693  elfznelfzob  13694  fladdz  13749  2tnp1ge0ge0  13753  flhalf  13754  ltdifltdiv  13758  fldiv4lem1div2uz2  13760  mulp1mod1  13838  m1modge3gt1  13845  modltm1p1mod  13850  addmodlteq  13873  ltexp2a  14093  expcan  14096  ltexp2  14097  leexp2  14098  leexp2a  14099  leexp2r  14101  nnlesq  14132  bernneq3  14158  expnbnd  14159  expnlbnd2  14161  expnngt1  14168  fzsdom2  14355  wrdlenge2n0  14479  swrd2lsw  14879  2swrd2eqwrdeq  14880  01sqrexlem7  15175  rddif  15268  reccn2  15524  rlimo1  15544  o1fsum  15740  abscvgcvg  15746  climcndslem1  15776  flo1  15781  harmonic  15786  geomulcvg  15803  fprodrecl  15880  fprodreclf  15886  fprodle  15923  bpoly4  15986  efcllem  16004  efgt1  16045  tanhlt1  16089  sinltx  16118  eirrlem  16133  p1modz1  16190  mod2eq1n2dvds  16278  oddge22np1  16280  ltoddhalfle  16292  nn0o1gt2  16312  nno  16313  nn0oddm1d2  16316  nnoddm1d2  16317  bitsfzolem  16365  bitsfzo  16366  bitsmod  16367  bitscmp  16369  bitsinv1lem  16372  smuval2  16413  coprmgcdb  16580  prmind2  16616  dvdsnprmd  16621  2mulprm  16624  isprm5  16638  isprm7  16639  divdenle  16680  zsqrtelqelz  16689  fermltl  16715  odzdvds  16727  modprm0  16737  iserodd  16767  difsqpwdvds  16819  pcfaclem  16830  prmreclem1  16848  4sqlem11  16887  4sqlem12  16888  ramub1lem1  16958  prmgaplem8  16990  2expltfac  17024  chnccat  18553  pgpfaclem2  20017  znidomb  21520  psdmvr  22116  chfacfisf  22802  chfacfisfcpmat  22803  chfacfscmulgsum  22808  chfacfpmmulgsum  22812  nrginvrcnlem  24639  nmoid  24690  xrsmopn  24761  metnrmlem1a  24807  iihalf2cn  24889  iccpnfhmeo  24903  lebnumii  24925  htpycc  24939  pcohtpylem  24979  pcoass  24984  pcorevlem  24986  nmhmcn  25080  cncmet  25282  ovoliunlem1  25463  dyadmaxlem  25558  vitalilem2  25570  mbfi1fseqlem6  25681  itg2mulc  25708  itg2monolem1  25711  itg2monolem3  25713  dveflem  25943  mvth  25957  dvlipcn  25959  lhop1lem  25978  dvfsumlem1  25992  dvfsumlem2  25993  dvfsumlem2OLD  25994  dvfsumlem3  25995  dvfsumlem4  25996  dvfsum2  26001  fta1glem2  26134  plyeq0lem  26175  fta1lem  26275  vieta1lem2  26279  aalioulem3  26302  aalioulem4  26303  radcnvlem1  26382  radcnvlem2  26383  dvradcnv  26390  abelthlem2  26402  abelthlem5  26405  abelthlem7  26408  abelth2  26412  cos02pilt1  26495  cosne0  26498  rplogcl  26573  logdivlti  26589  logno1  26605  dvlog2lem  26621  advlog  26623  logtayllem  26628  cxplt  26663  cxple  26664  cxpaddlelem  26721  cxpaddle  26722  rtprmirr  26730  relogbf  26761  logbgt0b  26763  isosctrlem1  26788  isosctrlem2  26789  chordthmlem4  26805  heron  26808  atanlogaddlem  26883  bndatandm  26899  leibpi  26912  log2tlbnd  26915  birthdaylem3  26923  rlimcnp  26935  rlimcnp2  26936  efrlim  26939  efrlimOLD  26940  cxp2limlem  26946  cxp2lim  26947  divsqrtsumo1  26954  jensenlem2  26958  logdiflbnd  26965  fsumharmonic  26982  lgamgulmlem2  27000  lgamgulmlem3  27001  lgamgulmlem4  27002  lgamgulmlem5  27003  lgamgulmlem6  27004  lgamcvg2  27025  regamcl  27031  wilthlem2  27039  ftalem2  27044  basellem9  27059  vma1  27136  ppieq0  27146  mumullem2  27150  fsumfldivdiaglem  27159  chpeq0  27179  chtub  27183  chpval2  27189  chpchtsum  27190  chpub  27191  logfacrlim  27195  logexprlim  27196  mersenne  27198  perfectlem2  27201  dchrelbas4  27214  bcmono  27248  bposlem1  27255  bposlem2  27256  zabsle1  27267  lgslem3  27270  lgsmod  27294  lgsdir2lem4  27299  lgsdirprm  27302  gausslemma2dlem1a  27336  gausslemma2d  27345  lgsquadlem2  27352  2sqlem8  27397  chebbnd1lem1  27440  chebbnd1lem2  27441  chtppilimlem1  27444  chebbnd2  27448  chto1lb  27449  chpchtlim  27450  chpo1ubb  27452  vmadivsum  27453  rplogsumlem1  27455  rpvmasumlem  27458  dchrisumlem3  27462  dchrmusumlema  27464  dchrmusum2  27465  dchrvmasumlem2  27469  dchrvmasumlem3  27470  dchrvmasumiflem1  27472  dchrvmasumiflem2  27473  dchrisum0flblem1  27479  dchrisum0flblem2  27480  dchrisum0fno1  27482  dchrisum0re  27484  dchrisum0lema  27485  dchrisum0lem1b  27486  dchrisum0lem2a  27488  dchrisum0lem2  27489  dchrisum0lem3  27490  rplogsum  27498  dirith2  27499  mudivsum  27501  mulogsumlem  27502  mulogsum  27503  mulog2sumlem1  27505  mulog2sumlem2  27506  vmalogdivsum2  27509  vmalogdivsum  27510  2vmadivsumlem  27511  log2sumbnd  27515  selberglem2  27517  selberg2lem  27521  chpdifbnd  27526  selberg3lem1  27528  selberg3  27530  selberg4lem1  27531  selberg4  27532  pntrmax  27535  pntrsumo1  27536  pntrsumbnd  27537  selberg3r  27540  selberg4r  27541  selberg34r  27542  pntrlog2bndlem1  27548  pntrlog2bndlem2  27549  pntrlog2bndlem3  27550  pntrlog2bndlem4  27551  pntrlog2bndlem5  27552  pntrlog2bndlem6  27554  pntrlog2bnd  27555  pntpbnd1a  27556  pntpbnd1  27557  pntibndlem2a  27561  pntibndlem2  27562  pntibnd  27564  pntlemc  27566  pntlemg  27569  pntlemr  27573  pntlemk  27577  pnt  27585  qabvle  27596  ostth2lem3  27606  ostth2  27608  trgcgrg  28570  tgcgr4  28586  ttgcontlem1  28940  axpaschlem  28996  axlowdimlem16  29013  axcontlem2  29021  axcontlem7  29026  nbusgrvtxm1  29435  upgrewlkle2  29663  pthdlem1  29822  crctcshwlkn0lem3  29868  crctcshwlkn0lem5  29870  wwlksm1edg  29937  wwlksnextproplem2  29966  clwlkclwwlklem2fv1  30053  clwlkclwwlklem2fv2  30054  clwlkclwwlklem2  30058  clwlkclwwlk2  30061  clwwisshclwwslem  30072  clwwlkf1  30107  clwwlkext2edg  30114  clwlknf1oclwwlknlem1  30139  clwwlknonex2lem2  30166  numclwwlk7  30449  frgrreggt1  30451  frgrogt3nreg  30455  smcnlem  30755  nmoub3i  30831  blocnilem  30862  ubthlem2  30929  minvecolem4  30938  htthlem  30975  nmcexi  32084  nmopcoi  32153  stadd3i  32306  cdj1i  32491  nnmulge  32799  receqid  32805  nndiffz1  32847  fzsplit3  32854  nexple  32906  indf1o  32927  wrdt2ind  33016  pmtrto1cl  33162  fzto1st1  33165  fzto1st  33166  psgnfzto1st  33168  cycpmco2lem6  33194  cycpmco2lem7  33195  cycpmrn  33206  qsidomlem1  33514  krull  33541  ply1degltel  33656  ply1degltlss  33658  constrnegcl  33901  constrdircl  33903  iconstr  33904  constrrecl  33907  constrmulcl  33909  constrreinvcl  33910  constrresqrtcl  33915  cos9thpiminplylem1  33920  cos9thpiminply  33926  cos9thpinconstrlem1  33927  1smat1  33942  submateqlem1  33945  madjusmdetlem2  33966  unitdivcld  34039  sqsscirc1  34046  esumdivc  34221  dya2ub  34408  dya2iocress  34412  dya2iocbrsiga  34413  dya2icobrsiga  34414  dya2icoseg  34415  dya2iocucvr  34422  sxbrsigalem2  34424  fibp1  34539  probmeasb  34568  dstrvprob  34610  dstfrvunirn  34613  ballotlemfc0  34631  ballotlemfcc  34632  ballotlemsgt1  34649  ballotlemsel1i  34651  ballotlemfrcn0  34668  signsply0  34689  itgexpif  34744  reprlt  34757  chtvalz  34767  breprexplemc  34770  breprexp  34771  circlemeth  34778  tgoldbachgnn  34797  acycgr1v  35324  subfaclim  35363  cvmliftlem2  35461  cvmliftlem13  35471  snmlff  35504  bccolsum  35914  faclim  35921  nn0prpwlem  36497  dnibndlem10  36668  dnibndlem12  36670  knoppcnlem4  36677  unblimceq0  36688  knoppndvlem1  36693  knoppndvlem2  36694  knoppndvlem3  36695  knoppndvlem7  36699  knoppndvlem11  36703  knoppndvlem12  36704  knoppndvlem14  36706  knoppndvlem15  36707  knoppndvlem17  36709  knoppndvlem18  36710  knoppndvlem20  36712  irrdiff  37508  poimirlem6  37804  poimirlem7  37805  poimirlem15  37813  poimirlem19  37817  poimirlem29  37827  poimirlem30  37828  poimirlem31  37829  poimirlem32  37830  broucube  37832  itg2addnclem2  37850  itg2addnclem3  37851  areacirclem1  37886  areacirclem4  37889  incsequz  37926  totbndbnd  37967  bfplem2  38001  resdvopclptsd  42325  lcmineqlem2  42327  lcmineqlem3  42328  lcmineqlem10  42335  lcmineqlem12  42337  lcmineqlem15  42340  lcmineqlem18  42343  lcmineqlem19  42344  lcmineqlem20  42345  lcmineqlem22  42347  lcmineqlem23  42348  3lexlogpow5ineq2  42352  3lexlogpow5ineq4  42353  3lexlogpow5ineq3  42354  3lexlogpow2ineq1  42355  3lexlogpow2ineq2  42356  3lexlogpow5ineq5  42357  aks4d1lem1  42359  dvrelog2  42361  dvrelog3  42362  dvrelog2b  42363  dvrelogpow2b  42365  aks4d1p1p3  42366  aks4d1p1p2  42367  aks4d1p1p4  42368  aks4d1p1p6  42370  aks4d1p1p7  42371  aks4d1p1p5  42372  aks4d1p1  42373  aks4d1p2  42374  aks4d1p3  42375  aks4d1p5  42377  aks4d1p6  42378  aks4d1p7d1  42379  aks4d1p7  42380  aks4d1p8d2  42382  aks4d1p8d3  42383  aks4d1p8  42384  aks4d1p9  42385  posbezout  42397  primrootlekpowne0  42402  primrootspoweq0  42403  aks6d1c1  42413  aks6d1c2p2  42416  hashscontpow1  42418  aks6d1c3  42420  aks6d1c2lem4  42424  aks6d1c2  42427  2np3bcnp1  42441  2ap1caineq  42442  sticksstones6  42448  sticksstones7  42449  sticksstones10  42452  sticksstones12a  42454  sticksstones12  42455  sticksstones22  42465  aks6d1c6lem3  42469  aks6d1c6lem4  42470  bcled  42475  bcle2d  42476  aks6d1c7lem1  42477  aks6d1c7lem2  42478  unitscyglem2  42493  unitscyglem4  42495  unitscyglem5  42496  aks5lem8  42498  sn-1ne2  42562  redvmptabs  42657  sn-00idlem2  42696  sn-0ne2  42703  rei4  42721  sn-rereccld  42745  rerecid  42746  sn-0tie0  42748  sn-nnne0  42757  mulgt0b1d  42769  sn-ltmulgt11d  42771  sn-0lt1  42772  sn-mulgt1d  42776  fimgmcyc  42831  flt4lem7  42944  fltnlta  42948  3cubeslem1  42968  3cubeslem3r  42971  3cubeslem4  42973  lzenom  43054  irrapxlem1  43106  irrapxlem2  43107  irrapxlem4  43109  irrapxlem5  43110  pellexlem2  43114  pell1qrge1  43154  pell1qr1  43155  elpell1qr2  43156  pell14qrgapw  43160  pellfundgt1  43167  pellfundglb  43169  pellfundex  43170  pellfundrp  43172  pellfundne1  43173  rmspecsqrtnq  43190  rmspecnonsq  43191  rmspecfund  43193  rmspecpos  43200  monotoddzzfi  43226  rmygeid  43248  areaquad  43500  imo72b2lem0  44448  imo72b2lem1  44452  imo72b2  44455  cvgdvgrat  44596  radcnvrat  44597  hashnzfzclim  44605  lhe4.4ex1a  44612  binomcxplemnn0  44632  binomcxplemdvbinom  44636  binomcxplemnotnn0  44639  oddfl  45568  abscosbd  45569  zltlesub  45575  abssinbd  45585  monoords  45587  fzisoeu  45590  fzdifsuc2  45600  suplesup  45626  xralrple2  45641  infxr  45653  infleinflem2  45657  reclt0d  45673  xrralrecnnge  45676  sqrlearg  45841  iooiinioc  45844  fmul01  45868  fmul01lt1lem1  45872  fmul01lt1lem2  45873  climsuselem1  45895  sumnnodd  45918  0ellimcdiv  45935  dvmptidg  46203  dvcosax  46212  ioodvbdlimc1lem1  46217  ioodvbdlimc1lem2  46218  ioodvbdlimc2lem  46220  dvxpaek  46226  dvnmul  46229  iblspltprt  46259  itgspltprt  46265  stoweidlem5  46291  stoweidlem7  46293  stoweidlem10  46296  stoweidlem11  46297  stoweidlem12  46298  stoweidlem13  46299  stoweidlem14  46300  stoweidlem16  46302  stoweidlem18  46304  stoweidlem20  46306  stoweidlem24  46310  stoweidlem25  46311  stoweidlem34  46320  stoweidlem36  46322  stoweidlem38  46324  stoweidlem40  46326  stoweidlem41  46327  stoweidlem42  46328  stoweidlem45  46331  stoweidlem51  46337  stoweidlem60  46346  wallispilem3  46353  wallispilem4  46354  wallispilem5  46355  wallispi  46356  wallispi2lem1  46357  wallispi2lem2  46358  wallispi2  46359  stirlinglem1  46360  stirlinglem3  46362  stirlinglem5  46364  stirlinglem6  46365  stirlinglem7  46366  stirlinglem8  46367  stirlinglem10  46369  stirlinglem11  46370  stirlinglem12  46371  stirlinglem13  46372  stirlinglem15  46374  dirker2re  46378  dirkerval2  46380  dirkerre  46381  dirkertrigeqlem1  46384  dirkertrigeqlem3  46386  dirkeritg  46388  dirkercncflem1  46389  dirkercncflem2  46390  dirkercncflem4  46392  fourierdlem5  46398  fourierdlem6  46399  fourierdlem11  46404  fourierdlem15  46408  fourierdlem19  46412  fourierdlem20  46413  fourierdlem24  46417  fourierdlem26  46419  fourierdlem28  46421  fourierdlem30  46423  fourierdlem39  46432  fourierdlem41  46434  fourierdlem43  46436  fourierdlem47  46439  fourierdlem48  46440  fourierdlem56  46448  fourierdlem60  46452  fourierdlem61  46453  fourierdlem62  46454  fourierdlem64  46456  fourierdlem65  46457  fourierdlem66  46458  fourierdlem68  46460  fourierdlem73  46465  fourierdlem78  46470  fourierdlem79  46471  fourierdlem87  46479  fourierdlem103  46495  fourierdlem104  46496  sqwvfoura  46514  fouriersw  46517  etransclem4  46524  etransclem23  46543  etransclem24  46544  etransclem31  46551  etransclem32  46552  etransclem35  46555  etransclem41  46561  etransclem46  46566  etransclem48  46568  etransc  46569  ioorrnopnxrlem  46592  nnfoctbdjlem  46741  iundjiun  46746  hoidmvlelem1  46881  hoidmvlelem2  46882  hoidmvlelem3  46883  hoidmvlelem4  46884  ovnhoilem1  46887  vonioolem2  46967  vonicclem2  46970  pimrecltneg  47010  smfrec  47075  smfmullem1  47077  smfmullem2  47078  smfdiv  47083  sigaradd  47152  ormkglobd  47161  cjnpoly  47177  p1lep2  47588  zm1nn  47590  ceilhalfgt1  47617  2tceilhalfelfzo1  47620  ceilbi  47621  rehalfge1  47623  ceilhalfnn  47624  addmodne  47632  m1mod0mod1  47642  m1modmmod  47646  difmodm1lt  47647  modmknepk  47650  modp2nep1  47655  modm1nem2  47657  iccpartiltu  47710  iccpartlt  47712  iccpartgt  47715  fmtnoge3  47818  fmtnodvds  47832  fmtnoprmfac2lem1  47854  2pwp1prm  47877  flsqrt  47881  sfprmdvdsmersenne  47891  lighneallem2  47894  lighneallem4a  47896  proththdlem  47901  proththd  47902  nnoALTV  47983  bgoldbtbndlem4  48096  gpgprismgrusgra  48346  gpgedgvtx0  48349  gpgvtxedg0  48351  gpg5nbgrvtx03starlem2  48357  gpg3kgrtriexlem4  48374  gpg3kgrtriexlem6  48376  cznnring  48550  divge1b  48800  divgt1b  48801  nn0eo  48816  regt1loggt0  48824  rege1logbrege0  48846  logblt1b  48852  fllog2  48856  nnolog2flm1  48878  dignn0flhalflem1  48903  rrxlinesc  49023  rrxlinec  49024  eenglngeehlnmlem1  49025  eenglngeehlnmlem2  49026  line2ylem  49039  line2  49040  line2xlem  49041  reseccl  50040  recsccl  50041  amgmwlem  50089  amgmlemALT  50090