Theorem 1red 11211

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11105  1c1 11107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-mulcl 11168  ax-mulrcl 11169  ax-i2m1 11174  ax-1ne0 11175  ax-rrecex 11178  ax-cnre 11179

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7407

This theorem is referenced by:  recgt0  12056  ltrec  12092  nnne0  12242  nn0p1gt0  12497  nn0ge2m1nn  12537  nn0le2is012  12622  suprzcl  12638  ledivge1le  13041  qbtwnre  13174  lincmb01cmp  13468  iccf1o  13469  xov1plusxeqvd  13471  zltaddlt1le  13478  fznatpl1  13551  elfz1b  13566  fzonn0p1p1  13707  elfznelfzo  13733  elfznelfzob  13734  fladdz  13786  2tnp1ge0ge0  13790  flhalf  13791  ltdifltdiv  13795  fldiv4lem1div2uz2  13797  mulp1mod1  13873  m1modge3gt1  13879  modltm1p1mod  13884  addmodlteq  13907  ltexp2a  14127  expcan  14130  ltexp2  14131  leexp2  14132  leexp2a  14133  leexp2r  14135  nnlesq  14165  bernneq3  14190  expnbnd  14191  expnlbnd2  14193  expnngt1  14200  fzsdom2  14384  wrdlenge2n0  14498  swrd2lsw  14899  2swrd2eqwrdeq  14900  01sqrexlem7  15191  rddif  15283  reccn2  15537  rlimo1  15557  o1fsum  15755  abscvgcvg  15761  climcndslem1  15791  flo1  15796  harmonic  15801  geomulcvg  15818  fprodrecl  15893  fprodreclf  15899  fprodle  15936  bpoly4  15999  efcllem  16017  efgt1  16055  tanhlt1  16099  sinltx  16128  eirrlem  16143  p1modz1  16200  mod2eq1n2dvds  16286  oddge22np1  16288  ltoddhalfle  16300  nn0o1gt2  16320  nno  16321  nn0oddm1d2  16324  nnoddm1d2  16325  bitsfzolem  16371  bitsfzo  16372  bitsmod  16373  bitscmp  16375  bitsinv1lem  16378  smuval2  16419  coprmgcdb  16582  prmind2  16618  dvdsnprmd  16623  2mulprm  16626  isprm5  16640  isprm7  16641  divdenle  16681  zsqrtelqelz  16690  fermltl  16713  odzdvds  16724  modprm0  16734  iserodd  16764  difsqpwdvds  16816  pcfaclem  16827  prmreclem1  16845  4sqlem11  16884  4sqlem12  16885  ramub1lem1  16955  prmgaplem8  16987  2expltfac  17022  pgpfaclem2  19944  znidomb  21101  chfacfisf  22338  chfacfisfcpmat  22339  chfacfscmulgsum  22344  chfacfpmmulgsum  22348  nrginvrcnlem  24190  nmoid  24241  xrsmopn  24310  metnrmlem1a  24356  iccpnfhmeo  24443  lebnumii  24464  htpycc  24478  pcohtpylem  24517  pcoass  24522  pcorevlem  24524  nmhmcn  24618  cncmet  24821  ovoliunlem1  25001  dyadmaxlem  25096  vitalilem2  25108  mbfi1fseqlem6  25220  itg2mulc  25247  itg2monolem1  25250  itg2monolem3  25252  dveflem  25478  mvth  25491  dvlipcn  25493  lhop1lem  25512  dvfsumlem1  25525  dvfsumlem2  25526  dvfsumlem3  25527  dvfsumlem4  25528  dvfsum2  25533  fta1glem2  25666  plyeq0lem  25706  fta1lem  25802  vieta1lem2  25806  aalioulem3  25829  aalioulem4  25830  radcnvlem1  25907  radcnvlem2  25908  dvradcnv  25915  abelthlem2  25926  abelthlem5  25929  abelthlem7  25932  abelth2  25936  cos02pilt1  26017  cosne0  26020  rplogcl  26094  logdivlti  26110  logno1  26126  dvlog2lem  26142  advlog  26144  logtayllem  26149  cxplt  26184  cxple  26185  cxpaddlelem  26239  cxpaddle  26240  relogbf  26276  logbgt0b  26278  isosctrlem1  26303  isosctrlem2  26304  chordthmlem4  26320  heron  26323  atanlogaddlem  26398  bndatandm  26414  leibpi  26427  log2tlbnd  26430  birthdaylem3  26438  rlimcnp  26450  rlimcnp2  26451  efrlim  26454  cxp2limlem  26460  cxp2lim  26461  divsqrtsumo1  26468  jensenlem2  26472  logdiflbnd  26479  fsumharmonic  26496  lgamgulmlem2  26514  lgamgulmlem3  26515  lgamgulmlem4  26516  lgamgulmlem5  26517  lgamgulmlem6  26518  lgamcvg2  26539  regamcl  26545  wilthlem2  26553  ftalem2  26558  basellem9  26573  vma1  26650  ppieq0  26660  mumullem2  26664  fsumfldivdiaglem  26673  chpeq0  26691  chtub  26695  chpval2  26701  chpchtsum  26702  chpub  26703  logfacrlim  26707  logexprlim  26708  mersenne  26710  perfectlem2  26713  dchrelbas4  26726  bcmono  26760  bposlem1  26767  bposlem2  26768  zabsle1  26779  lgslem3  26782  lgsmod  26806  lgsdir2lem4  26811  lgsdirprm  26814  gausslemma2dlem1a  26848  gausslemma2d  26857  lgsquadlem2  26864  2sqlem8  26909  chebbnd1lem1  26952  chebbnd1lem2  26953  chtppilimlem1  26956  chebbnd2  26960  chto1lb  26961  chpchtlim  26962  chpo1ubb  26964  vmadivsum  26965  rplogsumlem1  26967  rpvmasumlem  26970  dchrisumlem3  26974  dchrmusumlema  26976  dchrmusum2  26977  dchrvmasumlem2  26981  dchrvmasumlem3  26982  dchrvmasumiflem1  26984  dchrvmasumiflem2  26985  dchrisum0flblem1  26991  dchrisum0flblem2  26992  dchrisum0fno1  26994  dchrisum0re  26996  dchrisum0lema  26997  dchrisum0lem1b  26998  dchrisum0lem2a  27000  dchrisum0lem2  27001  dchrisum0lem3  27002  rplogsum  27010  dirith2  27011  mudivsum  27013  mulogsumlem  27014  mulogsum  27015  mulog2sumlem1  27017  mulog2sumlem2  27018  vmalogdivsum2  27021  vmalogdivsum  27022  2vmadivsumlem  27023  log2sumbnd  27027  selberglem2  27029  selberg2lem  27033  chpdifbnd  27038  selberg3lem1  27040  selberg3  27042  selberg4lem1  27043  selberg4  27044  pntrmax  27047  pntrsumo1  27048  pntrsumbnd  27049  selberg3r  27052  selberg4r  27053  selberg34r  27054  pntrlog2bndlem1  27060  pntrlog2bndlem2  27061  pntrlog2bndlem3  27062  pntrlog2bndlem4  27063  pntrlog2bndlem5  27064  pntrlog2bndlem6  27066  pntrlog2bnd  27067  pntpbnd1a  27068  pntpbnd1  27069  pntibndlem2a  27073  pntibndlem2  27074  pntibnd  27076  pntlemc  27078  pntlemg  27081  pntlemr  27085  pntlemk  27089  pnt  27097  qabvle  27108  ostth2lem3  27118  ostth2  27120  trgcgrg  27746  tgcgr4  27762  ttgcontlem1  28122  axpaschlem  28178  axlowdimlem16  28195  axcontlem2  28203  axcontlem7  28208  nbusgrvtxm1  28616  upgrewlkle2  28843  pthdlem1  29003  crctcshwlkn0lem3  29046  crctcshwlkn0lem5  29048  wwlksm1edg  29115  wwlksnextproplem2  29144  clwlkclwwlklem2fv1  29228  clwlkclwwlklem2fv2  29229  clwlkclwwlklem2  29233  clwlkclwwlk2  29236  clwwisshclwwslem  29247  clwwlkf1  29282  clwwlkext2edg  29289  clwlknf1oclwwlknlem1  29314  clwwlknonex2lem2  29341  numclwwlk7  29624  frgrreggt1  29626  frgrogt3nreg  29630  smcnlem  29928  nmoub3i  30004  blocnilem  30035  ubthlem2  30102  minvecolem4  30111  htthlem  30148  nmcexi  31257  nmopcoi  31326  stadd3i  31479  cdj1i  31664  nnmulge  31941  nndiffz1  31975  fzsplit3  31983  wrdt2ind  32095  pmtrto1cl  32236  fzto1st1  32239  fzto1st  32240  psgnfzto1st  32242  cycpmco2lem6  32268  cycpmco2lem7  32269  cycpmrn  32280  qsidomlem1  32529  krull  32547  ply1degltel  32613  ply1degltlss  32614  1smat1  32722  submateqlem1  32725  madjusmdetlem2  32746  unitdivcld  32819  sqsscirc1  32826  nexple  32945  indf1o  32960  esumdivc  33019  dya2ub  33207  dya2iocress  33211  dya2iocbrsiga  33212  dya2icobrsiga  33213  dya2icoseg  33214  dya2iocucvr  33221  sxbrsigalem2  33223  fibp1  33338  probmeasb  33367  dstrvprob  33408  dstfrvunirn  33411  ballotlemfc0  33429  ballotlemfcc  33430  ballotlemsgt1  33447  ballotlemsel1i  33449  ballotlemfrcn0  33466  signsply0  33500  itgexpif  33556  reprlt  33569  chtvalz  33579  breprexplemc  33582  breprexp  33583  circlemeth  33590  tgoldbachgnn  33609  acycgr1v  34078  subfaclim  34117  cvmliftlem2  34215  cvmliftlem13  34225  snmlff  34258  bccolsum  34647  faclim  34654  gg-dvfsumlem2  35121  nn0prpwlem  35145  dnibndlem10  35301  dnibndlem12  35303  knoppcnlem4  35310  unblimceq0  35321  knoppndvlem1  35326  knoppndvlem2  35327  knoppndvlem3  35328  knoppndvlem7  35332  knoppndvlem11  35336  knoppndvlem12  35337  knoppndvlem14  35339  knoppndvlem15  35340  knoppndvlem17  35342  knoppndvlem18  35343  knoppndvlem20  35345  irrdiff  36145  poimirlem6  36432  poimirlem7  36433  poimirlem15  36441  poimirlem19  36445  poimirlem29  36455  poimirlem30  36456  poimirlem31  36457  poimirlem32  36458  broucube  36460  itg2addnclem2  36478  itg2addnclem3  36479  areacirclem1  36514  areacirclem4  36517  incsequz  36554  totbndbnd  36595  bfplem2  36629  resdvopclptsd  40831  lcmineqlem2  40833  lcmineqlem3  40834  lcmineqlem10  40841  lcmineqlem12  40843  lcmineqlem15  40846  lcmineqlem18  40849  lcmineqlem19  40850  lcmineqlem20  40851  lcmineqlem22  40853  lcmineqlem23  40854  3lexlogpow5ineq2  40858  3lexlogpow5ineq4  40859  3lexlogpow5ineq3  40860  3lexlogpow2ineq1  40861  3lexlogpow2ineq2  40862  3lexlogpow5ineq5  40863  aks4d1lem1  40865  dvrelog2  40867  dvrelog3  40868  dvrelog2b  40869  dvrelogpow2b  40871  aks4d1p1p3  40872  aks4d1p1p2  40873  aks4d1p1p4  40874  aks4d1p1p6  40876  aks4d1p1p7  40877  aks4d1p1p5  40878  aks4d1p1  40879  aks4d1p2  40880  aks4d1p3  40881  aks4d1p5  40883  aks4d1p6  40884  aks4d1p7d1  40885  aks4d1p7  40886  aks4d1p8d2  40888  aks4d1p8d3  40889  aks4d1p8  40890  aks4d1p9  40891  aks6d1c2p2  40895  2np3bcnp1  40898  2ap1caineq  40899  sticksstones6  40905  sticksstones7  40906  sticksstones10  40909  sticksstones12a  40911  sticksstones12  40912  sticksstones22  40922  metakunt1  40923  metakunt2  40924  metakunt7  40929  metakunt15  40937  metakunt16  40938  metakunt24  40946  metakunt28  40950  metakunt29  40951  2xp3dxp2ge1d  40960  factwoffsmonot  40961  sn-1ne2  41129  rtprmirr  41181  sn-00idlem2  41216  sn-0ne2  41223  rei4  41240  sn-0tie0  41256  sn-nnne0  41265  mulgt0b2d  41277  sn-0lt1  41279  flt4lem7  41345  fltnlta  41349  3cubeslem1  41355  3cubeslem3r  41358  3cubeslem4  41360  lzenom  41441  irrapxlem1  41493  irrapxlem2  41494  irrapxlem4  41496  irrapxlem5  41497  pellexlem2  41501  pell1qrge1  41541  pell1qr1  41542  elpell1qr2  41543  pell14qrgapw  41547  pellfundgt1  41554  pellfundglb  41556  pellfundex  41557  pellfundrp  41559  pellfundne1  41560  rmspecsqrtnq  41577  rmspecnonsq  41578  rmspecfund  41580  rmspecpos  41588  monotoddzzfi  41614  rmygeid  41636  areaquad  41898  imo72b2lem0  42850  imo72b2lem1  42854  imo72b2  42857  cvgdvgrat  43005  radcnvrat  43006  hashnzfzclim  43014  lhe4.4ex1a  43021  binomcxplemnn0  43041  binomcxplemdvbinom  43045  binomcxplemnotnn0  43048  oddfl  43922  abscosbd  43923  zltlesub  43930  abssinbd  43940  monoords  43942  fzisoeu  43945  fzdifsuc2  43955  suplesup  43984  xralrple2  43999  infxr  44012  infleinflem2  44016  reclt0d  44032  xrralrecnnge  44035  sqrlearg  44201  iooiinioc  44204  fmul01  44231  fmul01lt1lem1  44235  fmul01lt1lem2  44236  climsuselem1  44258  sumnnodd  44281  0ellimcdiv  44300  dvmptidg  44568  dvcosax  44577  ioodvbdlimc1lem1  44582  ioodvbdlimc1lem2  44583  ioodvbdlimc2lem  44585  dvxpaek  44591  dvnmul  44594  iblspltprt  44624  itgspltprt  44630  stoweidlem5  44656  stoweidlem7  44658  stoweidlem10  44661  stoweidlem11  44662  stoweidlem12  44663  stoweidlem13  44664  stoweidlem14  44665  stoweidlem16  44667  stoweidlem18  44669  stoweidlem20  44671  stoweidlem24  44675  stoweidlem25  44676  stoweidlem34  44685  stoweidlem36  44687  stoweidlem38  44689  stoweidlem40  44691  stoweidlem41  44692  stoweidlem42  44693  stoweidlem45  44696  stoweidlem51  44702  stoweidlem60  44711  wallispilem3  44718  wallispilem4  44719  wallispilem5  44720  wallispi  44721  wallispi2lem1  44722  wallispi2lem2  44723  wallispi2  44724  stirlinglem1  44725  stirlinglem3  44727  stirlinglem5  44729  stirlinglem6  44730  stirlinglem7  44731  stirlinglem8  44732  stirlinglem10  44734  stirlinglem11  44735  stirlinglem12  44736  stirlinglem13  44737  stirlinglem15  44739  dirker2re  44743  dirkerval2  44745  dirkerre  44746  dirkertrigeqlem1  44749  dirkertrigeqlem3  44751  dirkeritg  44753  dirkercncflem1  44754  dirkercncflem2  44755  dirkercncflem4  44757  fourierdlem5  44763  fourierdlem6  44764  fourierdlem11  44769  fourierdlem15  44773  fourierdlem19  44777  fourierdlem20  44778  fourierdlem24  44782  fourierdlem26  44784  fourierdlem28  44786  fourierdlem30  44788  fourierdlem39  44797  fourierdlem41  44799  fourierdlem43  44801  fourierdlem47  44804  fourierdlem48  44805  fourierdlem56  44813  fourierdlem60  44817  fourierdlem61  44818  fourierdlem62  44819  fourierdlem64  44821  fourierdlem65  44822  fourierdlem66  44823  fourierdlem68  44825  fourierdlem73  44830  fourierdlem78  44835  fourierdlem79  44836  fourierdlem87  44844  fourierdlem103  44860  fourierdlem104  44861  sqwvfoura  44879  fouriersw  44882  etransclem4  44889  etransclem23  44908  etransclem24  44909  etransclem31  44916  etransclem32  44917  etransclem35  44920  etransclem41  44926  etransclem46  44931  etransclem48  44933  etransc  44934  ioorrnopnxrlem  44957  nnfoctbdjlem  45106  iundjiun  45111  hoidmvlelem1  45246  hoidmvlelem2  45247  hoidmvlelem3  45248  hoidmvlelem4  45249  ovnhoilem1  45252  vonioolem2  45332  vonicclem2  45335  pimrecltneg  45375  smfrec  45440  smfmullem1  45442  smfmullem2  45443  smfdiv  45448  sigaradd  45517  p1lep2  45943  zm1nn  45945  m1mod0mod1  45972  iccpartiltu  46025  iccpartlt  46027  iccpartgt  46030  fmtnoge3  46133  fmtnodvds  46147  fmtnoprmfac2lem1  46169  2pwp1prm  46192  flsqrt  46196  sfprmdvdsmersenne  46206  lighneallem2  46209  lighneallem4a  46211  proththdlem  46216  proththd  46217  nnoALTV  46298  bgoldbtbndlem4  46411  cznnring  46756  divge1b  47095  divgt1b  47096  m1modmmod  47109  difmodm1lt  47110  nn0eo  47116  regt1loggt0  47124  rege1logbrege0  47146  logblt1b  47152  fllog2  47156  nnolog2flm1  47178  dignn0flhalflem1  47203  rrxlinesc  47323  rrxlinec  47324  eenglngeehlnmlem1  47325  eenglngeehlnmlem2  47326  line2ylem  47339  line2  47340  line2xlem  47341  reseccl  47700  recsccl  47701  amgmwlem  47751  amgmlemALT  47752