Theorem 1red 10631

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℝcr 10525  1c1 10527

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 2770  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rrecex 10598  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ne 2988  df-ral 3111  df-rex 3112  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138

This theorem is referenced by:  recgt0  11475  ltrec  11511  nnne0  11659  nn0p1gt0  11914  nn0ge2m1nn  11952  nn0le2is012  12034  suprzcl  12050  ledivge1le  12448  qbtwnre  12580  lincmb01cmp  12873  iccf1o  12874  xov1plusxeqvd  12876  zltaddlt1le  12883  fznatpl1  12956  elfz1b  12971  fzonn0p1p1  13111  elfznelfzo  13137  elfznelfzob  13138  fladdz  13190  2tnp1ge0ge0  13194  flhalf  13195  ltdifltdiv  13199  fldiv4lem1div2uz2  13201  mulp1mod1  13275  m1modge3gt1  13281  modltm1p1mod  13286  addmodlteq  13309  ltexp2a  13526  expcan  13529  ltexp2  13530  leexp2  13531  leexp2a  13532  leexp2r  13534  nnlesq  13564  bernneq3  13588  expnbnd  13589  expnlbnd2  13591  expnngt1  13598  fzsdom2  13785  wrdlenge2n0  13895  swrd2lsw  14305  2swrd2eqwrdeq  14306  sqrlem7  14600  rddif  14692  reccn2  14945  rlimo1  14965  o1fsum  15160  abscvgcvg  15166  climcndslem1  15196  flo1  15201  harmonic  15206  geomulcvg  15224  fprodrecl  15299  fprodreclf  15305  fprodle  15342  bpoly4  15405  efcllem  15423  efgt1  15461  tanhlt1  15505  sinltx  15534  eirrlem  15549  p1modz1  15606  mod2eq1n2dvds  15688  oddge22np1  15690  ltoddhalfle  15702  nn0o1gt2  15722  nno  15723  nn0oddm1d2  15726  nnoddm1d2  15727  bitsfzolem  15773  bitsfzo  15774  bitsmod  15775  bitscmp  15777  bitsinv1lem  15780  smuval2  15821  coprmgcdb  15983  prmind2  16019  dvdsnprmd  16024  2mulprm  16027  isprm5  16041  isprm7  16042  divdenle  16079  zsqrtelqelz  16088  fermltl  16111  odzdvds  16122  modprm0  16132  iserodd  16162  difsqpwdvds  16213  pcfaclem  16224  prmreclem1  16242  4sqlem11  16281  4sqlem12  16282  ramub1lem1  16352  prmgaplem8  16384  2expltfac  16418  pgpfaclem2  19197  znidomb  20253  chfacfisf  21459  chfacfisfcpmat  21460  chfacfscmulgsum  21465  chfacfpmmulgsum  21469  nrginvrcnlem  23297  nmoid  23348  xrsmopn  23417  metnrmlem1a  23463  iccpnfhmeo  23550  lebnumii  23571  htpycc  23585  pcohtpylem  23624  pcoass  23629  pcorevlem  23631  nmhmcn  23725  cncmet  23926  ovoliunlem1  24106  dyadmaxlem  24201  vitalilem2  24213  mbfi1fseqlem6  24324  itg2mulc  24351  itg2monolem1  24354  itg2monolem3  24356  dveflem  24582  mvth  24595  dvlipcn  24597  lhop1lem  24616  dvfsumlem1  24629  dvfsumlem2  24630  dvfsumlem3  24631  dvfsumlem4  24632  dvfsum2  24637  fta1glem2  24767  plyeq0lem  24807  fta1lem  24903  vieta1lem2  24907  aalioulem3  24930  aalioulem4  24931  radcnvlem1  25008  radcnvlem2  25009  dvradcnv  25016  abelthlem2  25027  abelthlem5  25030  abelthlem7  25033  abelth2  25037  cos02pilt1  25118  cosne0  25121  rplogcl  25195  logdivlti  25211  logno1  25227  dvlog2lem  25243  advlog  25245  logtayllem  25250  cxplt  25285  cxple  25286  cxpaddlelem  25340  cxpaddle  25341  relogbf  25377  logbgt0b  25379  isosctrlem1  25404  isosctrlem2  25405  chordthmlem4  25421  heron  25424  atanlogaddlem  25499  bndatandm  25515  leibpi  25528  log2tlbnd  25531  birthdaylem3  25539  rlimcnp  25551  rlimcnp2  25552  efrlim  25555  cxp2limlem  25561  cxp2lim  25562  divsqrtsumo1  25569  jensenlem2  25573  logdiflbnd  25580  fsumharmonic  25597  lgamgulmlem2  25615  lgamgulmlem3  25616  lgamgulmlem4  25617  lgamgulmlem5  25618  lgamgulmlem6  25619  lgamcvg2  25640  regamcl  25646  wilthlem2  25654  ftalem2  25659  basellem9  25674  vma1  25751  ppieq0  25761  mumullem2  25765  fsumfldivdiaglem  25774  chpeq0  25792  chtub  25796  chpval2  25802  chpchtsum  25803  chpub  25804  logfacrlim  25808  logexprlim  25809  mersenne  25811  perfectlem2  25814  dchrelbas4  25827  bcmono  25861  bposlem1  25868  bposlem2  25869  zabsle1  25880  lgslem3  25883  lgsmod  25907  lgsdir2lem4  25912  lgsdirprm  25915  gausslemma2dlem1a  25949  gausslemma2d  25958  lgsquadlem2  25965  2sqlem8  26010  chebbnd1lem1  26053  chebbnd1lem2  26054  chtppilimlem1  26057  chebbnd2  26061  chto1lb  26062  chpchtlim  26063  chpo1ubb  26065  vmadivsum  26066  rplogsumlem1  26068  rpvmasumlem  26071  dchrisumlem3  26075  dchrmusumlema  26077  dchrmusum2  26078  dchrvmasumlem2  26082  dchrvmasumlem3  26083  dchrvmasumiflem1  26085  dchrvmasumiflem2  26086  dchrisum0flblem1  26092  dchrisum0flblem2  26093  dchrisum0fno1  26095  dchrisum0re  26097  dchrisum0lema  26098  dchrisum0lem1b  26099  dchrisum0lem2a  26101  dchrisum0lem2  26102  dchrisum0lem3  26103  rplogsum  26111  dirith2  26112  mudivsum  26114  mulogsumlem  26115  mulogsum  26116  mulog2sumlem1  26118  mulog2sumlem2  26119  vmalogdivsum2  26122  vmalogdivsum  26123  2vmadivsumlem  26124  log2sumbnd  26128  selberglem2  26130  selberg2lem  26134  chpdifbnd  26139  selberg3lem1  26141  selberg3  26143  selberg4lem1  26144  selberg4  26145  pntrmax  26148  pntrsumo1  26149  pntrsumbnd  26150  selberg3r  26153  selberg4r  26154  selberg34r  26155  pntrlog2bndlem1  26161  pntrlog2bndlem2  26162  pntrlog2bndlem3  26163  pntrlog2bndlem4  26164  pntrlog2bndlem5  26165  pntrlog2bndlem6  26167  pntrlog2bnd  26168  pntpbnd1a  26169  pntpbnd1  26170  pntibndlem2a  26174  pntibndlem2  26175  pntibnd  26177  pntlemc  26179  pntlemg  26182  pntlemr  26186  pntlemk  26190  pnt  26198  qabvle  26209  ostth2lem3  26219  ostth2  26221  trgcgrg  26309  tgcgr4  26325  ttgcontlem1  26679  axpaschlem  26734  axlowdimlem16  26751  axcontlem2  26759  axcontlem7  26764  nbusgrvtxm1  27169  upgrewlkle2  27396  pthdlem1  27555  crctcshwlkn0lem3  27598  crctcshwlkn0lem5  27600  wwlksm1edg  27667  wwlksnextproplem2  27696  clwlkclwwlklem2fv1  27780  clwlkclwwlklem2fv2  27781  clwlkclwwlklem2  27785  clwlkclwwlk2  27788  clwwisshclwwslem  27799  clwwlkf1  27834  clwwlkext2edg  27841  clwlknf1oclwwlknlem1  27866  clwwlknonex2lem2  27893  numclwwlk7  28176  frgrreggt1  28178  frgrogt3nreg  28182  smcnlem  28480  nmoub3i  28556  blocnilem  28587  ubthlem2  28654  minvecolem4  28663  htthlem  28700  nmcexi  29809  nmopcoi  29878  stadd3i  30031  cdj1i  30216  nnmulge  30500  nndiffz1  30535  fzsplit3  30543  wrdt2ind  30653  pmtrto1cl  30791  fzto1st1  30794  fzto1st  30795  psgnfzto1st  30797  cycpmco2lem6  30823  cycpmco2lem7  30824  cycpmrn  30835  qsidomlem1  31036  krull  31051  1smat1  31157  submateqlem1  31160  madjusmdetlem2  31181  unitdivcld  31254  sqsscirc1  31261  nexple  31378  indf1o  31393  esumdivc  31452  dya2ub  31638  dya2iocress  31642  dya2iocbrsiga  31643  dya2icobrsiga  31644  dya2icoseg  31645  dya2iocucvr  31652  sxbrsigalem2  31654  fibp1  31769  probmeasb  31798  dstrvprob  31839  dstfrvunirn  31842  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemsgt1  31878  ballotlemsel1i  31880  ballotlemfrcn0  31897  signsply0  31931  itgexpif  31987  reprlt  32000  chtvalz  32010  breprexplemc  32013  breprexp  32014  circlemeth  32021  tgoldbachgnn  32040  acycgr1v  32509  subfaclim  32548  cvmliftlem2  32646  cvmliftlem13  32656  snmlff  32689  bccolsum  33084  faclim  33091  nn0prpwlem  33783  dnibndlem10  33939  dnibndlem12  33941  knoppcnlem4  33948  unblimceq0  33959  knoppndvlem1  33964  knoppndvlem2  33965  knoppndvlem3  33966  knoppndvlem7  33970  knoppndvlem11  33974  knoppndvlem12  33975  knoppndvlem14  33977  knoppndvlem15  33978  knoppndvlem17  33980  knoppndvlem18  33981  knoppndvlem20  33983  irrdiff  34740  poimirlem6  35063  poimirlem7  35064  poimirlem15  35072  poimirlem19  35076  poimirlem29  35086  poimirlem30  35087  poimirlem31  35088  poimirlem32  35089  broucube  35091  itg2addnclem2  35109  itg2addnclem3  35110  areacirclem1  35145  areacirclem4  35148  incsequz  35186  totbndbnd  35227  bfplem2  35261  resdvopclptsd  39316  lcmineqlem2  39318  lcmineqlem3  39319  lcmineqlem10  39326  lcmineqlem12  39328  lcmineqlem15  39331  lcmineqlem18  39334  lcmineqlem19  39335  lcmineqlem20  39336  lcmineqlem22  39338  lcmineqlem23  39339  3lexlogpow5ineq2  39342  3lexlogpow5ineq3  39343  2np3bcnp1  39348  2ap1caineq  39349  metakunt1  39350  metakunt2  39351  metakunt7  39356  metakunt15  39364  metakunt16  39365  metakunt24  39373  metakunt28  39377  metakunt29  39378  2xp3dxp2ge1d  39387  factwoffsmonot  39388  sn-1ne2  39466  rtprmirr  39502  sn-00idlem2  39537  sn-0ne2  39544  sn-0tie0  39576  mulgt0b2d  39585  fltnlta  39619  3cubeslem1  39625  3cubeslem3r  39628  3cubeslem4  39630  lzenom  39711  irrapxlem1  39763  irrapxlem2  39764  irrapxlem4  39766  irrapxlem5  39767  pellexlem2  39771  pell1qrge1  39811  pell1qr1  39812  elpell1qr2  39813  pell14qrgapw  39817  pellfundgt1  39824  pellfundglb  39826  pellfundex  39827  pellfundrp  39829  pellfundne1  39830  rmspecsqrtnq  39847  rmspecnonsq  39848  rmspecfund  39850  rmspecpos  39857  monotoddzzfi  39883  rmygeid  39905  areaquad  40166  imo72b2lem0  40869  imo72b2lem1  40874  imo72b2  40878  cvgdvgrat  41017  radcnvrat  41018  hashnzfzclim  41026  lhe4.4ex1a  41033  binomcxplemnn0  41053  binomcxplemdvbinom  41057  binomcxplemnotnn0  41060  oddfl  41908  abscosbd  41909  zltlesub  41916  abssinbd  41927  monoords  41929  fzisoeu  41932  fzdifsuc2  41942  suplesup  41971  xralrple2  41986  infxr  41999  infleinflem2  42003  reclt0d  42022  xrralrecnnge  42026  sqrlearg  42190  iooiinioc  42193  fmul01  42222  fmul01lt1lem1  42226  fmul01lt1lem2  42227  climsuselem1  42249  sumnnodd  42272  0ellimcdiv  42291  dvmptidg  42559  dvcosax  42568  ioodvbdlimc1lem1  42573  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  dvxpaek  42582  dvnmul  42585  iblspltprt  42615  itgspltprt  42621  stoweidlem5  42647  stoweidlem7  42649  stoweidlem10  42652  stoweidlem11  42653  stoweidlem12  42654  stoweidlem13  42655  stoweidlem14  42656  stoweidlem16  42658  stoweidlem18  42660  stoweidlem20  42662  stoweidlem24  42666  stoweidlem25  42667  stoweidlem34  42676  stoweidlem36  42678  stoweidlem38  42680  stoweidlem40  42682  stoweidlem41  42683  stoweidlem42  42684  stoweidlem45  42687  stoweidlem51  42693  stoweidlem60  42702  wallispilem3  42709  wallispilem4  42710  wallispilem5  42711  wallispi  42712  wallispi2lem1  42713  wallispi2lem2  42714  wallispi2  42715  stirlinglem1  42716  stirlinglem3  42718  stirlinglem5  42720  stirlinglem6  42721  stirlinglem7  42722  stirlinglem8  42723  stirlinglem10  42725  stirlinglem11  42726  stirlinglem12  42727  stirlinglem13  42728  stirlinglem15  42730  dirker2re  42734  dirkerval2  42736  dirkerre  42737  dirkertrigeqlem1  42740  dirkertrigeqlem3  42742  dirkeritg  42744  dirkercncflem1  42745  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem5  42754  fourierdlem6  42755  fourierdlem11  42760  fourierdlem15  42764  fourierdlem19  42768  fourierdlem20  42769  fourierdlem24  42773  fourierdlem26  42775  fourierdlem28  42777  fourierdlem30  42779  fourierdlem39  42788  fourierdlem41  42790  fourierdlem43  42792  fourierdlem47  42795  fourierdlem48  42796  fourierdlem56  42804  fourierdlem60  42808  fourierdlem61  42809  fourierdlem62  42810  fourierdlem64  42812  fourierdlem65  42813  fourierdlem66  42814  fourierdlem68  42816  fourierdlem73  42821  fourierdlem78  42826  fourierdlem79  42827  fourierdlem87  42835  fourierdlem103  42851  fourierdlem104  42852  sqwvfoura  42870  fouriersw  42873  etransclem4  42880  etransclem23  42899  etransclem24  42900  etransclem31  42907  etransclem32  42908  etransclem35  42911  etransclem41  42917  etransclem46  42922  etransclem48  42924  etransc  42925  ioorrnopnxrlem  42948  nnfoctbdjlem  43094  iundjiun  43099  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem3  43236  hoidmvlelem4  43237  ovnhoilem1  43240  vonioolem2  43320  vonicclem2  43323  pimrecltneg  43358  smfrec  43421  smfmullem1  43423  smfmullem2  43424  smfdiv  43429  sigaradd  43480  p1lep2  43857  zm1nn  43859  m1mod0mod1  43886  iccpartiltu  43939  iccpartlt  43941  iccpartgt  43944  fmtnoge3  44047  fmtnodvds  44061  fmtnoprmfac2lem1  44083  2pwp1prm  44106  flsqrt  44110  sfprmdvdsmersenne  44121  lighneallem2  44124  lighneallem4a  44126  proththdlem  44131  proththd  44132  nnoALTV  44213  bgoldbtbndlem4  44326  cznnring  44580  divge1b  44921  divgt1b  44922  m1modmmod  44935  difmodm1lt  44936  nn0eo  44942  regt1loggt0  44950  rege1logbrege0  44972  logblt1b  44978  fllog2  44982  nnolog2flm1  45004  dignn0flhalflem1  45029  rrxlinesc  45149  rrxlinec  45150  eenglngeehlnmlem1  45151  eenglngeehlnmlem2  45152  line2ylem  45165  line2  45166  line2xlem  45167  reseccl  45279  recsccl  45280  amgmwlem  45330  amgmlemALT  45331