Theorem 1red 10680

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 10574  1c1 10576

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-mulcl 10637  ax-mulrcl 10638  ax-i2m1 10643  ax-1ne0 10644  ax-rrecex 10647  ax-cnre 10648

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-ne 2952  df-ral 3075  df-rex 3076  df-v 3411  df-un 3863  df-in 3865  df-ss 3875  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-iota 6294  df-fv 6343  df-ov 7153

This theorem is referenced by:  recgt0  11524  ltrec  11560  nnne0  11708  nn0p1gt0  11963  nn0ge2m1nn  12003  nn0le2is012  12085  suprzcl  12101  ledivge1le  12501  qbtwnre  12633  lincmb01cmp  12927  iccf1o  12928  xov1plusxeqvd  12930  zltaddlt1le  12937  fznatpl1  13010  elfz1b  13025  fzonn0p1p1  13165  elfznelfzo  13191  elfznelfzob  13192  fladdz  13244  2tnp1ge0ge0  13248  flhalf  13249  ltdifltdiv  13253  fldiv4lem1div2uz2  13255  mulp1mod1  13329  m1modge3gt1  13335  modltm1p1mod  13340  addmodlteq  13363  ltexp2a  13580  expcan  13583  ltexp2  13584  leexp2  13585  leexp2a  13586  leexp2r  13588  nnlesq  13618  bernneq3  13642  expnbnd  13643  expnlbnd2  13645  expnngt1  13652  fzsdom2  13839  wrdlenge2n0  13951  swrd2lsw  14361  2swrd2eqwrdeq  14362  sqrlem7  14656  rddif  14748  reccn2  15001  rlimo1  15021  o1fsum  15216  abscvgcvg  15222  climcndslem1  15252  flo1  15257  harmonic  15262  geomulcvg  15280  fprodrecl  15355  fprodreclf  15361  fprodle  15398  bpoly4  15461  efcllem  15479  efgt1  15517  tanhlt1  15561  sinltx  15590  eirrlem  15605  p1modz1  15662  mod2eq1n2dvds  15748  oddge22np1  15750  ltoddhalfle  15762  nn0o1gt2  15782  nno  15783  nn0oddm1d2  15786  nnoddm1d2  15787  bitsfzolem  15833  bitsfzo  15834  bitsmod  15835  bitscmp  15837  bitsinv1lem  15840  smuval2  15881  coprmgcdb  16045  prmind2  16081  dvdsnprmd  16086  2mulprm  16089  isprm5  16103  isprm7  16104  divdenle  16144  zsqrtelqelz  16153  fermltl  16176  odzdvds  16187  modprm0  16197  iserodd  16227  difsqpwdvds  16278  pcfaclem  16289  prmreclem1  16307  4sqlem11  16346  4sqlem12  16347  ramub1lem1  16417  prmgaplem8  16449  2expltfac  16484  pgpfaclem2  19272  znidomb  20329  chfacfisf  21554  chfacfisfcpmat  21555  chfacfscmulgsum  21560  chfacfpmmulgsum  21564  nrginvrcnlem  23393  nmoid  23444  xrsmopn  23513  metnrmlem1a  23559  iccpnfhmeo  23646  lebnumii  23667  htpycc  23681  pcohtpylem  23720  pcoass  23725  pcorevlem  23727  nmhmcn  23821  cncmet  24022  ovoliunlem1  24202  dyadmaxlem  24297  vitalilem2  24309  mbfi1fseqlem6  24420  itg2mulc  24447  itg2monolem1  24450  itg2monolem3  24452  dveflem  24678  mvth  24691  dvlipcn  24693  lhop1lem  24712  dvfsumlem1  24725  dvfsumlem2  24726  dvfsumlem3  24727  dvfsumlem4  24728  dvfsum2  24733  fta1glem2  24866  plyeq0lem  24906  fta1lem  25002  vieta1lem2  25006  aalioulem3  25029  aalioulem4  25030  radcnvlem1  25107  radcnvlem2  25108  dvradcnv  25115  abelthlem2  25126  abelthlem5  25129  abelthlem7  25132  abelth2  25136  cos02pilt1  25217  cosne0  25220  rplogcl  25294  logdivlti  25310  logno1  25326  dvlog2lem  25342  advlog  25344  logtayllem  25349  cxplt  25384  cxple  25385  cxpaddlelem  25439  cxpaddle  25440  relogbf  25476  logbgt0b  25478  isosctrlem1  25503  isosctrlem2  25504  chordthmlem4  25520  heron  25523  atanlogaddlem  25598  bndatandm  25614  leibpi  25627  log2tlbnd  25630  birthdaylem3  25638  rlimcnp  25650  rlimcnp2  25651  efrlim  25654  cxp2limlem  25660  cxp2lim  25661  divsqrtsumo1  25668  jensenlem2  25672  logdiflbnd  25679  fsumharmonic  25696  lgamgulmlem2  25714  lgamgulmlem3  25715  lgamgulmlem4  25716  lgamgulmlem5  25717  lgamgulmlem6  25718  lgamcvg2  25739  regamcl  25745  wilthlem2  25753  ftalem2  25758  basellem9  25773  vma1  25850  ppieq0  25860  mumullem2  25864  fsumfldivdiaglem  25873  chpeq0  25891  chtub  25895  chpval2  25901  chpchtsum  25902  chpub  25903  logfacrlim  25907  logexprlim  25908  mersenne  25910  perfectlem2  25913  dchrelbas4  25926  bcmono  25960  bposlem1  25967  bposlem2  25968  zabsle1  25979  lgslem3  25982  lgsmod  26006  lgsdir2lem4  26011  lgsdirprm  26014  gausslemma2dlem1a  26048  gausslemma2d  26057  lgsquadlem2  26064  2sqlem8  26109  chebbnd1lem1  26152  chebbnd1lem2  26153  chtppilimlem1  26156  chebbnd2  26160  chto1lb  26161  chpchtlim  26162  chpo1ubb  26164  vmadivsum  26165  rplogsumlem1  26167  rpvmasumlem  26170  dchrisumlem3  26174  dchrmusumlema  26176  dchrmusum2  26177  dchrvmasumlem2  26181  dchrvmasumlem3  26182  dchrvmasumiflem1  26184  dchrvmasumiflem2  26185  dchrisum0flblem1  26191  dchrisum0flblem2  26192  dchrisum0fno1  26194  dchrisum0re  26196  dchrisum0lema  26197  dchrisum0lem1b  26198  dchrisum0lem2a  26200  dchrisum0lem2  26201  dchrisum0lem3  26202  rplogsum  26210  dirith2  26211  mudivsum  26213  mulogsumlem  26214  mulogsum  26215  mulog2sumlem1  26217  mulog2sumlem2  26218  vmalogdivsum2  26221  vmalogdivsum  26222  2vmadivsumlem  26223  log2sumbnd  26227  selberglem2  26229  selberg2lem  26233  chpdifbnd  26238  selberg3lem1  26240  selberg3  26242  selberg4lem1  26243  selberg4  26244  pntrmax  26247  pntrsumo1  26248  pntrsumbnd  26249  selberg3r  26252  selberg4r  26253  selberg34r  26254  pntrlog2bndlem1  26260  pntrlog2bndlem2  26261  pntrlog2bndlem3  26262  pntrlog2bndlem4  26263  pntrlog2bndlem5  26264  pntrlog2bndlem6  26266  pntrlog2bnd  26267  pntpbnd1a  26268  pntpbnd1  26269  pntibndlem2a  26273  pntibndlem2  26274  pntibnd  26276  pntlemc  26278  pntlemg  26281  pntlemr  26285  pntlemk  26289  pnt  26297  qabvle  26308  ostth2lem3  26318  ostth2  26320  trgcgrg  26408  tgcgr4  26424  ttgcontlem1  26778  axpaschlem  26833  axlowdimlem16  26850  axcontlem2  26858  axcontlem7  26863  nbusgrvtxm1  27268  upgrewlkle2  27495  pthdlem1  27654  crctcshwlkn0lem3  27697  crctcshwlkn0lem5  27699  wwlksm1edg  27766  wwlksnextproplem2  27795  clwlkclwwlklem2fv1  27879  clwlkclwwlklem2fv2  27880  clwlkclwwlklem2  27884  clwlkclwwlk2  27887  clwwisshclwwslem  27898  clwwlkf1  27933  clwwlkext2edg  27940  clwlknf1oclwwlknlem1  27965  clwwlknonex2lem2  27992  numclwwlk7  28275  frgrreggt1  28277  frgrogt3nreg  28281  smcnlem  28579  nmoub3i  28655  blocnilem  28686  ubthlem2  28753  minvecolem4  28762  htthlem  28799  nmcexi  29908  nmopcoi  29977  stadd3i  30130  cdj1i  30315  nnmulge  30597  nndiffz1  30631  fzsplit3  30639  wrdt2ind  30749  pmtrto1cl  30892  fzto1st1  30895  fzto1st  30896  psgnfzto1st  30898  cycpmco2lem6  30924  cycpmco2lem7  30925  cycpmrn  30936  qsidomlem1  31149  krull  31164  1smat1  31275  submateqlem1  31278  madjusmdetlem2  31299  unitdivcld  31372  sqsscirc1  31379  nexple  31496  indf1o  31511  esumdivc  31570  dya2ub  31756  dya2iocress  31760  dya2iocbrsiga  31761  dya2icobrsiga  31762  dya2icoseg  31763  dya2iocucvr  31770  sxbrsigalem2  31772  fibp1  31887  probmeasb  31916  dstrvprob  31957  dstfrvunirn  31960  ballotlemfc0  31978  ballotlemfcc  31979  ballotlemsgt1  31996  ballotlemsel1i  31998  ballotlemfrcn0  32015  signsply0  32049  itgexpif  32105  reprlt  32118  chtvalz  32128  breprexplemc  32131  breprexp  32132  circlemeth  32139  tgoldbachgnn  32158  acycgr1v  32627  subfaclim  32666  cvmliftlem2  32764  cvmliftlem13  32774  snmlff  32807  bccolsum  33220  faclim  33227  nn0prpwlem  34060  dnibndlem10  34216  dnibndlem12  34218  knoppcnlem4  34225  unblimceq0  34236  knoppndvlem1  34241  knoppndvlem2  34242  knoppndvlem3  34243  knoppndvlem7  34247  knoppndvlem11  34251  knoppndvlem12  34252  knoppndvlem14  34254  knoppndvlem15  34255  knoppndvlem17  34257  knoppndvlem18  34258  knoppndvlem20  34260  irrdiff  35020  poimirlem6  35343  poimirlem7  35344  poimirlem15  35352  poimirlem19  35356  poimirlem29  35366  poimirlem30  35367  poimirlem31  35368  poimirlem32  35369  broucube  35371  itg2addnclem2  35389  itg2addnclem3  35390  areacirclem1  35425  areacirclem4  35428  incsequz  35466  totbndbnd  35507  bfplem2  35541  resdvopclptsd  39595  lcmineqlem2  39597  lcmineqlem3  39598  lcmineqlem10  39605  lcmineqlem12  39607  lcmineqlem15  39610  lcmineqlem18  39613  lcmineqlem19  39614  lcmineqlem20  39615  lcmineqlem22  39617  lcmineqlem23  39618  3lexlogpow5ineq2  39622  3lexlogpow5ineq4  39623  3lexlogpow5ineq3  39624  3lexlogpow2ineq1  39625  3lexlogpow2ineq2  39626  3lexlogpow5ineq5  39627  dvrelog2  39630  dvrelog3  39631  dvrelog2b  39632  dvrelogpow2b  39634  aks4d1p1p3  39635  aks4d1p1p2  39636  aks4d1p1p4  39637  aks4d1p1p6  39639  aks4d1p1p7  39640  aks4d1p1p5  39641  aks4d1p1  39642  2np3bcnp1  39645  2ap1caineq  39646  metakunt1  39647  metakunt2  39648  metakunt7  39653  metakunt15  39661  metakunt16  39662  metakunt24  39670  metakunt28  39674  metakunt29  39675  2xp3dxp2ge1d  39684  factwoffsmonot  39685  sn-1ne2  39797  rtprmirr  39844  sn-00idlem2  39879  sn-0ne2  39886  sn-0tie0  39918  mulgt0b2d  39927  flt4lem7  39988  fltnlta  39992  3cubeslem1  39998  3cubeslem3r  40001  3cubeslem4  40003  lzenom  40084  irrapxlem1  40136  irrapxlem2  40137  irrapxlem4  40139  irrapxlem5  40140  pellexlem2  40144  pell1qrge1  40184  pell1qr1  40185  elpell1qr2  40186  pell14qrgapw  40190  pellfundgt1  40197  pellfundglb  40199  pellfundex  40200  pellfundrp  40202  pellfundne1  40203  rmspecsqrtnq  40220  rmspecnonsq  40221  rmspecfund  40223  rmspecpos  40230  monotoddzzfi  40256  rmygeid  40278  areaquad  40539  imo72b2lem0  41242  imo72b2lem1  41247  imo72b2  41251  cvgdvgrat  41390  radcnvrat  41391  hashnzfzclim  41399  lhe4.4ex1a  41406  binomcxplemnn0  41426  binomcxplemdvbinom  41430  binomcxplemnotnn0  41433  oddfl  42276  abscosbd  42277  zltlesub  42284  abssinbd  42295  monoords  42297  fzisoeu  42300  fzdifsuc2  42310  suplesup  42339  xralrple2  42354  infxr  42367  infleinflem2  42371  reclt0d  42389  xrralrecnnge  42393  sqrlearg  42556  iooiinioc  42559  fmul01  42588  fmul01lt1lem1  42592  fmul01lt1lem2  42593  climsuselem1  42615  sumnnodd  42638  0ellimcdiv  42657  dvmptidg  42925  dvcosax  42934  ioodvbdlimc1lem1  42939  ioodvbdlimc1lem2  42940  ioodvbdlimc2lem  42942  dvxpaek  42948  dvnmul  42951  iblspltprt  42981  itgspltprt  42987  stoweidlem5  43013  stoweidlem7  43015  stoweidlem10  43018  stoweidlem11  43019  stoweidlem12  43020  stoweidlem13  43021  stoweidlem14  43022  stoweidlem16  43024  stoweidlem18  43026  stoweidlem20  43028  stoweidlem24  43032  stoweidlem25  43033  stoweidlem34  43042  stoweidlem36  43044  stoweidlem38  43046  stoweidlem40  43048  stoweidlem41  43049  stoweidlem42  43050  stoweidlem45  43053  stoweidlem51  43059  stoweidlem60  43068  wallispilem3  43075  wallispilem4  43076  wallispilem5  43077  wallispi  43078  wallispi2lem1  43079  wallispi2lem2  43080  wallispi2  43081  stirlinglem1  43082  stirlinglem3  43084  stirlinglem5  43086  stirlinglem6  43087  stirlinglem7  43088  stirlinglem8  43089  stirlinglem10  43091  stirlinglem11  43092  stirlinglem12  43093  stirlinglem13  43094  stirlinglem15  43096  dirker2re  43100  dirkerval2  43102  dirkerre  43103  dirkertrigeqlem1  43106  dirkertrigeqlem3  43108  dirkeritg  43110  dirkercncflem1  43111  dirkercncflem2  43112  dirkercncflem4  43114  fourierdlem5  43120  fourierdlem6  43121  fourierdlem11  43126  fourierdlem15  43130  fourierdlem19  43134  fourierdlem20  43135  fourierdlem24  43139  fourierdlem26  43141  fourierdlem28  43143  fourierdlem30  43145  fourierdlem39  43154  fourierdlem41  43156  fourierdlem43  43158  fourierdlem47  43161  fourierdlem48  43162  fourierdlem56  43170  fourierdlem60  43174  fourierdlem61  43175  fourierdlem62  43176  fourierdlem64  43178  fourierdlem65  43179  fourierdlem66  43180  fourierdlem68  43182  fourierdlem73  43187  fourierdlem78  43192  fourierdlem79  43193  fourierdlem87  43201  fourierdlem103  43217  fourierdlem104  43218  sqwvfoura  43236  fouriersw  43239  etransclem4  43246  etransclem23  43265  etransclem24  43266  etransclem31  43273  etransclem32  43274  etransclem35  43277  etransclem41  43283  etransclem46  43288  etransclem48  43290  etransc  43291  ioorrnopnxrlem  43314  nnfoctbdjlem  43460  iundjiun  43465  hoidmvlelem1  43600  hoidmvlelem2  43601  hoidmvlelem3  43602  hoidmvlelem4  43603  ovnhoilem1  43606  vonioolem2  43686  vonicclem2  43689  pimrecltneg  43724  smfrec  43787  smfmullem1  43789  smfmullem2  43790  smfdiv  43795  sigaradd  43846  p1lep2  44225  zm1nn  44227  m1mod0mod1  44254  iccpartiltu  44307  iccpartlt  44309  iccpartgt  44312  fmtnoge3  44415  fmtnodvds  44429  fmtnoprmfac2lem1  44451  2pwp1prm  44474  flsqrt  44478  sfprmdvdsmersenne  44488  lighneallem2  44491  lighneallem4a  44493  proththdlem  44498  proththd  44499  nnoALTV  44580  bgoldbtbndlem4  44693  cznnring  44947  divge1b  45286  divgt1b  45287  m1modmmod  45300  difmodm1lt  45301  nn0eo  45307  regt1loggt0  45315  rege1logbrege0  45337  logblt1b  45343  fllog2  45347  nnolog2flm1  45369  dignn0flhalflem1  45394  rrxlinesc  45514  rrxlinec  45515  eenglngeehlnmlem1  45516  eenglngeehlnmlem2  45517  line2ylem  45530  line2  45531  line2xlem  45532  reseccl  45670  recsccl  45671  amgmwlem  45721  amgmlemALT  45722