Theorem 1red 11215

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

Syntax hints:   → wi 4   ∈ wcel 2107  ℝcr 11109  1c1 11111

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 11168  ax-icn 11169  ax-addcl 11170  ax-mulcl 11172  ax-mulrcl 11173  ax-i2m1 11178  ax-1ne0 11179  ax-rrecex 11182  ax-cnre 11183

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 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412

This theorem is referenced by:  recgt0  12060  ltrec  12096  nnne0  12246  nn0p1gt0  12501  nn0ge2m1nn  12541  nn0le2is012  12626  suprzcl  12642  ledivge1le  13045  qbtwnre  13178  lincmb01cmp  13472  iccf1o  13473  xov1plusxeqvd  13475  zltaddlt1le  13482  fznatpl1  13555  elfz1b  13570  fzonn0p1p1  13711  elfznelfzo  13737  elfznelfzob  13738  fladdz  13790  2tnp1ge0ge0  13794  flhalf  13795  ltdifltdiv  13799  fldiv4lem1div2uz2  13801  mulp1mod1  13877  m1modge3gt1  13883  modltm1p1mod  13888  addmodlteq  13911  ltexp2a  14131  expcan  14134  ltexp2  14135  leexp2  14136  leexp2a  14137  leexp2r  14139  nnlesq  14169  bernneq3  14194  expnbnd  14195  expnlbnd2  14197  expnngt1  14204  fzsdom2  14388  wrdlenge2n0  14502  swrd2lsw  14903  2swrd2eqwrdeq  14904  01sqrexlem7  15195  rddif  15287  reccn2  15541  rlimo1  15561  o1fsum  15759  abscvgcvg  15765  climcndslem1  15795  flo1  15800  harmonic  15805  geomulcvg  15822  fprodrecl  15897  fprodreclf  15903  fprodle  15940  bpoly4  16003  efcllem  16021  efgt1  16059  tanhlt1  16103  sinltx  16132  eirrlem  16147  p1modz1  16204  mod2eq1n2dvds  16290  oddge22np1  16292  ltoddhalfle  16304  nn0o1gt2  16324  nno  16325  nn0oddm1d2  16328  nnoddm1d2  16329  bitsfzolem  16375  bitsfzo  16376  bitsmod  16377  bitscmp  16379  bitsinv1lem  16382  smuval2  16423  coprmgcdb  16586  prmind2  16622  dvdsnprmd  16627  2mulprm  16630  isprm5  16644  isprm7  16645  divdenle  16685  zsqrtelqelz  16694  fermltl  16717  odzdvds  16728  modprm0  16738  iserodd  16768  difsqpwdvds  16820  pcfaclem  16831  prmreclem1  16849  4sqlem11  16888  4sqlem12  16889  ramub1lem1  16959  prmgaplem8  16991  2expltfac  17026  pgpfaclem2  19952  znidomb  21117  chfacfisf  22356  chfacfisfcpmat  22357  chfacfscmulgsum  22362  chfacfpmmulgsum  22366  nrginvrcnlem  24208  nmoid  24259  xrsmopn  24328  metnrmlem1a  24374  iccpnfhmeo  24461  lebnumii  24482  htpycc  24496  pcohtpylem  24535  pcoass  24540  pcorevlem  24542  nmhmcn  24636  cncmet  24839  ovoliunlem1  25019  dyadmaxlem  25114  vitalilem2  25126  mbfi1fseqlem6  25238  itg2mulc  25265  itg2monolem1  25268  itg2monolem3  25270  dveflem  25496  mvth  25509  dvlipcn  25511  lhop1lem  25530  dvfsumlem1  25543  dvfsumlem2  25544  dvfsumlem3  25545  dvfsumlem4  25546  dvfsum2  25551  fta1glem2  25684  plyeq0lem  25724  fta1lem  25820  vieta1lem2  25824  aalioulem3  25847  aalioulem4  25848  radcnvlem1  25925  radcnvlem2  25926  dvradcnv  25933  abelthlem2  25944  abelthlem5  25947  abelthlem7  25950  abelth2  25954  cos02pilt1  26035  cosne0  26038  rplogcl  26112  logdivlti  26128  logno1  26144  dvlog2lem  26160  advlog  26162  logtayllem  26167  cxplt  26202  cxple  26203  cxpaddlelem  26259  cxpaddle  26260  relogbf  26296  logbgt0b  26298  isosctrlem1  26323  isosctrlem2  26324  chordthmlem4  26340  heron  26343  atanlogaddlem  26418  bndatandm  26434  leibpi  26447  log2tlbnd  26450  birthdaylem3  26458  rlimcnp  26470  rlimcnp2  26471  efrlim  26474  cxp2limlem  26480  cxp2lim  26481  divsqrtsumo1  26488  jensenlem2  26492  logdiflbnd  26499  fsumharmonic  26516  lgamgulmlem2  26534  lgamgulmlem3  26535  lgamgulmlem4  26536  lgamgulmlem5  26537  lgamgulmlem6  26538  lgamcvg2  26559  regamcl  26565  wilthlem2  26573  ftalem2  26578  basellem9  26593  vma1  26670  ppieq0  26680  mumullem2  26684  fsumfldivdiaglem  26693  chpeq0  26711  chtub  26715  chpval2  26721  chpchtsum  26722  chpub  26723  logfacrlim  26727  logexprlim  26728  mersenne  26730  perfectlem2  26733  dchrelbas4  26746  bcmono  26780  bposlem1  26787  bposlem2  26788  zabsle1  26799  lgslem3  26802  lgsmod  26826  lgsdir2lem4  26831  lgsdirprm  26834  gausslemma2dlem1a  26868  gausslemma2d  26877  lgsquadlem2  26884  2sqlem8  26929  chebbnd1lem1  26972  chebbnd1lem2  26973  chtppilimlem1  26976  chebbnd2  26980  chto1lb  26981  chpchtlim  26982  chpo1ubb  26984  vmadivsum  26985  rplogsumlem1  26987  rpvmasumlem  26990  dchrisumlem3  26994  dchrmusumlema  26996  dchrmusum2  26997  dchrvmasumlem2  27001  dchrvmasumlem3  27002  dchrvmasumiflem1  27004  dchrvmasumiflem2  27005  dchrisum0flblem1  27011  dchrisum0flblem2  27012  dchrisum0fno1  27014  dchrisum0re  27016  dchrisum0lema  27017  dchrisum0lem1b  27018  dchrisum0lem2a  27020  dchrisum0lem2  27021  dchrisum0lem3  27022  rplogsum  27030  dirith2  27031  mudivsum  27033  mulogsumlem  27034  mulogsum  27035  mulog2sumlem1  27037  mulog2sumlem2  27038  vmalogdivsum2  27041  vmalogdivsum  27042  2vmadivsumlem  27043  log2sumbnd  27047  selberglem2  27049  selberg2lem  27053  chpdifbnd  27058  selberg3lem1  27060  selberg3  27062  selberg4lem1  27063  selberg4  27064  pntrmax  27067  pntrsumo1  27068  pntrsumbnd  27069  selberg3r  27072  selberg4r  27073  selberg34r  27074  pntrlog2bndlem1  27080  pntrlog2bndlem2  27081  pntrlog2bndlem3  27082  pntrlog2bndlem4  27083  pntrlog2bndlem5  27084  pntrlog2bndlem6  27086  pntrlog2bnd  27087  pntpbnd1a  27088  pntpbnd1  27089  pntibndlem2a  27093  pntibndlem2  27094  pntibnd  27096  pntlemc  27098  pntlemg  27101  pntlemr  27105  pntlemk  27109  pnt  27117  qabvle  27128  ostth2lem3  27138  ostth2  27140  trgcgrg  27766  tgcgr4  27782  ttgcontlem1  28142  axpaschlem  28198  axlowdimlem16  28215  axcontlem2  28223  axcontlem7  28228  nbusgrvtxm1  28636  upgrewlkle2  28863  pthdlem1  29023  crctcshwlkn0lem3  29066  crctcshwlkn0lem5  29068  wwlksm1edg  29135  wwlksnextproplem2  29164  clwlkclwwlklem2fv1  29248  clwlkclwwlklem2fv2  29249  clwlkclwwlklem2  29253  clwlkclwwlk2  29256  clwwisshclwwslem  29267  clwwlkf1  29302  clwwlkext2edg  29309  clwlknf1oclwwlknlem1  29334  clwwlknonex2lem2  29361  numclwwlk7  29644  frgrreggt1  29646  frgrogt3nreg  29650  smcnlem  29950  nmoub3i  30026  blocnilem  30057  ubthlem2  30124  minvecolem4  30133  htthlem  30170  nmcexi  31279  nmopcoi  31348  stadd3i  31501  cdj1i  31686  nnmulge  31963  nndiffz1  31997  fzsplit3  32005  wrdt2ind  32117  pmtrto1cl  32258  fzto1st1  32261  fzto1st  32262  psgnfzto1st  32264  cycpmco2lem6  32290  cycpmco2lem7  32291  cycpmrn  32302  qsidomlem1  32571  krull  32594  ply1degltel  32666  ply1degltlss  32667  1smat1  32784  submateqlem1  32787  madjusmdetlem2  32808  unitdivcld  32881  sqsscirc1  32888  nexple  33007  indf1o  33022  esumdivc  33081  dya2ub  33269  dya2iocress  33273  dya2iocbrsiga  33274  dya2icobrsiga  33275  dya2icoseg  33276  dya2iocucvr  33283  sxbrsigalem2  33285  fibp1  33400  probmeasb  33429  dstrvprob  33470  dstfrvunirn  33473  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemsgt1  33509  ballotlemsel1i  33511  ballotlemfrcn0  33528  signsply0  33562  itgexpif  33618  reprlt  33631  chtvalz  33641  breprexplemc  33644  breprexp  33645  circlemeth  33652  tgoldbachgnn  33671  acycgr1v  34140  subfaclim  34179  cvmliftlem2  34277  cvmliftlem13  34287  snmlff  34320  bccolsum  34709  faclim  34716  gg-dvfsumlem2  35183  nn0prpwlem  35207  dnibndlem10  35363  dnibndlem12  35365  knoppcnlem4  35372  unblimceq0  35383  knoppndvlem1  35388  knoppndvlem2  35389  knoppndvlem3  35390  knoppndvlem7  35394  knoppndvlem11  35398  knoppndvlem12  35399  knoppndvlem14  35401  knoppndvlem15  35402  knoppndvlem17  35404  knoppndvlem18  35405  knoppndvlem20  35407  irrdiff  36207  poimirlem6  36494  poimirlem7  36495  poimirlem15  36503  poimirlem19  36507  poimirlem29  36517  poimirlem30  36518  poimirlem31  36519  poimirlem32  36520  broucube  36522  itg2addnclem2  36540  itg2addnclem3  36541  areacirclem1  36576  areacirclem4  36579  incsequz  36616  totbndbnd  36657  bfplem2  36691  resdvopclptsd  40893  lcmineqlem2  40895  lcmineqlem3  40896  lcmineqlem10  40903  lcmineqlem12  40905  lcmineqlem15  40908  lcmineqlem18  40911  lcmineqlem19  40912  lcmineqlem20  40913  lcmineqlem22  40915  lcmineqlem23  40916  3lexlogpow5ineq2  40920  3lexlogpow5ineq4  40921  3lexlogpow5ineq3  40922  3lexlogpow2ineq1  40923  3lexlogpow2ineq2  40924  3lexlogpow5ineq5  40925  aks4d1lem1  40927  dvrelog2  40929  dvrelog3  40930  dvrelog2b  40931  dvrelogpow2b  40933  aks4d1p1p3  40934  aks4d1p1p2  40935  aks4d1p1p4  40936  aks4d1p1p6  40938  aks4d1p1p7  40939  aks4d1p1p5  40940  aks4d1p1  40941  aks4d1p2  40942  aks4d1p3  40943  aks4d1p5  40945  aks4d1p6  40946  aks4d1p7d1  40947  aks4d1p7  40948  aks4d1p8d2  40950  aks4d1p8d3  40951  aks4d1p8  40952  aks4d1p9  40953  aks6d1c2p2  40957  2np3bcnp1  40960  2ap1caineq  40961  sticksstones6  40967  sticksstones7  40968  sticksstones10  40971  sticksstones12a  40973  sticksstones12  40974  sticksstones22  40984  metakunt1  40985  metakunt2  40986  metakunt7  40991  metakunt15  40999  metakunt16  41000  metakunt24  41008  metakunt28  41012  metakunt29  41013  2xp3dxp2ge1d  41022  factwoffsmonot  41023  sn-1ne2  41179  rtprmirr  41237  sn-00idlem2  41272  sn-0ne2  41279  rei4  41296  sn-0tie0  41312  sn-nnne0  41321  mulgt0b2d  41333  sn-0lt1  41335  flt4lem7  41401  fltnlta  41405  3cubeslem1  41422  3cubeslem3r  41425  3cubeslem4  41427  lzenom  41508  irrapxlem1  41560  irrapxlem2  41561  irrapxlem4  41563  irrapxlem5  41564  pellexlem2  41568  pell1qrge1  41608  pell1qr1  41609  elpell1qr2  41610  pell14qrgapw  41614  pellfundgt1  41621  pellfundglb  41623  pellfundex  41624  pellfundrp  41626  pellfundne1  41627  rmspecsqrtnq  41644  rmspecnonsq  41645  rmspecfund  41647  rmspecpos  41655  monotoddzzfi  41681  rmygeid  41703  areaquad  41965  imo72b2lem0  42917  imo72b2lem1  42921  imo72b2  42924  cvgdvgrat  43072  radcnvrat  43073  hashnzfzclim  43081  lhe4.4ex1a  43088  binomcxplemnn0  43108  binomcxplemdvbinom  43112  binomcxplemnotnn0  43115  oddfl  43987  abscosbd  43988  zltlesub  43995  abssinbd  44005  monoords  44007  fzisoeu  44010  fzdifsuc2  44020  suplesup  44049  xralrple2  44064  infxr  44077  infleinflem2  44081  reclt0d  44097  xrralrecnnge  44100  sqrlearg  44266  iooiinioc  44269  fmul01  44296  fmul01lt1lem1  44300  fmul01lt1lem2  44301  climsuselem1  44323  sumnnodd  44346  0ellimcdiv  44365  dvmptidg  44633  dvcosax  44642  ioodvbdlimc1lem1  44647  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvxpaek  44656  dvnmul  44659  iblspltprt  44689  itgspltprt  44695  stoweidlem5  44721  stoweidlem7  44723  stoweidlem10  44726  stoweidlem11  44727  stoweidlem12  44728  stoweidlem13  44729  stoweidlem14  44730  stoweidlem16  44732  stoweidlem18  44734  stoweidlem20  44736  stoweidlem24  44740  stoweidlem25  44741  stoweidlem34  44750  stoweidlem36  44752  stoweidlem38  44754  stoweidlem40  44756  stoweidlem41  44757  stoweidlem42  44758  stoweidlem45  44761  stoweidlem51  44767  stoweidlem60  44776  wallispilem3  44783  wallispilem4  44784  wallispilem5  44785  wallispi  44786  wallispi2lem1  44787  wallispi2lem2  44788  wallispi2  44789  stirlinglem1  44790  stirlinglem3  44792  stirlinglem5  44794  stirlinglem6  44795  stirlinglem7  44796  stirlinglem8  44797  stirlinglem10  44799  stirlinglem11  44800  stirlinglem12  44801  stirlinglem13  44802  stirlinglem15  44804  dirker2re  44808  dirkerval2  44810  dirkerre  44811  dirkertrigeqlem1  44814  dirkertrigeqlem3  44816  dirkeritg  44818  dirkercncflem1  44819  dirkercncflem2  44820  dirkercncflem4  44822  fourierdlem5  44828  fourierdlem6  44829  fourierdlem11  44834  fourierdlem15  44838  fourierdlem19  44842  fourierdlem20  44843  fourierdlem24  44847  fourierdlem26  44849  fourierdlem28  44851  fourierdlem30  44853  fourierdlem39  44862  fourierdlem41  44864  fourierdlem43  44866  fourierdlem47  44869  fourierdlem48  44870  fourierdlem56  44878  fourierdlem60  44882  fourierdlem61  44883  fourierdlem62  44884  fourierdlem64  44886  fourierdlem65  44887  fourierdlem66  44888  fourierdlem68  44890  fourierdlem73  44895  fourierdlem78  44900  fourierdlem79  44901  fourierdlem87  44909  fourierdlem103  44925  fourierdlem104  44926  sqwvfoura  44944  fouriersw  44947  etransclem4  44954  etransclem23  44973  etransclem24  44974  etransclem31  44981  etransclem32  44982  etransclem35  44985  etransclem41  44991  etransclem46  44996  etransclem48  44998  etransc  44999  ioorrnopnxrlem  45022  nnfoctbdjlem  45171  iundjiun  45176  hoidmvlelem1  45311  hoidmvlelem2  45312  hoidmvlelem3  45313  hoidmvlelem4  45314  ovnhoilem1  45317  vonioolem2  45397  vonicclem2  45400  pimrecltneg  45440  smfrec  45505  smfmullem1  45507  smfmullem2  45508  smfdiv  45513  sigaradd  45582  p1lep2  46008  zm1nn  46010  m1mod0mod1  46037  iccpartiltu  46090  iccpartlt  46092  iccpartgt  46095  fmtnoge3  46198  fmtnodvds  46212  fmtnoprmfac2lem1  46234  2pwp1prm  46257  flsqrt  46261  sfprmdvdsmersenne  46271  lighneallem2  46274  lighneallem4a  46276  proththdlem  46281  proththd  46282  nnoALTV  46363  bgoldbtbndlem4  46476  cznnring  46854  divge1b  47193  divgt1b  47194  m1modmmod  47207  difmodm1lt  47208  nn0eo  47214  regt1loggt0  47222  rege1logbrege0  47244  logblt1b  47250  fllog2  47254  nnolog2flm1  47276  dignn0flhalflem1  47301  rrxlinesc  47421  rrxlinec  47422  eenglngeehlnmlem1  47423  eenglngeehlnmlem2  47424  line2ylem  47437  line2  47438  line2xlem  47439  reseccl  47798  recsccl  47799  amgmwlem  47849  amgmlemALT  47850