Theorem 1red 11259

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

Syntax hints:   → wi 4   ∈ wcel 2105  ℝcr 11151  1c1 11153

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-mulcl 11214  ax-mulrcl 11215  ax-i2m1 11220  ax-1ne0 11221  ax-rrecex 11224  ax-cnre 11225

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433

This theorem is referenced by:  recgt0  12110  mulgt1  12126  ltrec  12147  nnne0  12297  nn0p1gt0  12552  nn0ge2m1nn  12593  nn0le2is012  12679  suprzcl  12695  ledivge1le  13103  ge2halflem1  13147  qbtwnre  13237  lincmb01cmp  13531  iccf1o  13532  xov1plusxeqvd  13534  zltaddlt1le  13541  fznatpl1  13614  elfz1b  13629  elfzo0subge1  13741  fzonn0p1p1  13779  elfznelfzo  13807  elfznelfzob  13808  fladdz  13861  2tnp1ge0ge0  13865  flhalf  13866  ltdifltdiv  13870  fldiv4lem1div2uz2  13872  mulp1mod1  13948  m1modge3gt1  13955  modltm1p1mod  13960  addmodlteq  13983  ltexp2a  14202  expcan  14205  ltexp2  14206  leexp2  14207  leexp2a  14208  leexp2r  14210  nnlesq  14240  bernneq3  14266  expnbnd  14267  expnlbnd2  14269  expnngt1  14276  fzsdom2  14463  wrdlenge2n0  14586  swrd2lsw  14987  2swrd2eqwrdeq  14988  01sqrexlem7  15283  rddif  15375  reccn2  15629  rlimo1  15649  o1fsum  15845  abscvgcvg  15851  climcndslem1  15881  flo1  15886  harmonic  15891  geomulcvg  15908  fprodrecl  15985  fprodreclf  15991  fprodle  16028  bpoly4  16091  efcllem  16109  efgt1  16148  tanhlt1  16192  sinltx  16221  eirrlem  16236  p1modz1  16293  mod2eq1n2dvds  16380  oddge22np1  16382  ltoddhalfle  16394  nn0o1gt2  16414  nno  16415  nn0oddm1d2  16418  nnoddm1d2  16419  bitsfzolem  16467  bitsfzo  16468  bitsmod  16469  bitscmp  16471  bitsinv1lem  16474  smuval2  16515  coprmgcdb  16682  prmind2  16718  dvdsnprmd  16723  2mulprm  16726  isprm5  16740  isprm7  16741  divdenle  16782  zsqrtelqelz  16791  fermltl  16817  odzdvds  16828  modprm0  16838  iserodd  16868  difsqpwdvds  16920  pcfaclem  16931  prmreclem1  16949  4sqlem11  16988  4sqlem12  16989  ramub1lem1  17059  prmgaplem8  17091  2expltfac  17126  pgpfaclem2  20116  znidomb  21597  chfacfisf  22875  chfacfisfcpmat  22876  chfacfscmulgsum  22881  chfacfpmmulgsum  22885  nrginvrcnlem  24727  nmoid  24778  xrsmopn  24847  metnrmlem1a  24893  iihalf2cn  24975  iccpnfhmeo  24989  lebnumii  25011  htpycc  25025  pcohtpylem  25065  pcoass  25070  pcorevlem  25072  nmhmcn  25166  cncmet  25369  ovoliunlem1  25550  dyadmaxlem  25645  vitalilem2  25657  mbfi1fseqlem6  25769  itg2mulc  25796  itg2monolem1  25799  itg2monolem3  25801  dveflem  26031  mvth  26045  dvlipcn  26047  lhop1lem  26066  dvfsumlem1  26080  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem3  26083  dvfsumlem4  26084  dvfsum2  26089  fta1glem2  26222  plyeq0lem  26263  fta1lem  26363  vieta1lem2  26367  aalioulem3  26390  aalioulem4  26391  radcnvlem1  26470  radcnvlem2  26471  dvradcnv  26478  abelthlem2  26490  abelthlem5  26493  abelthlem7  26496  abelth2  26500  cos02pilt1  26582  cosne0  26585  rplogcl  26660  logdivlti  26676  logno1  26692  dvlog2lem  26708  advlog  26710  logtayllem  26715  cxplt  26750  cxple  26751  cxpaddlelem  26808  cxpaddle  26809  rtprmirr  26817  relogbf  26848  logbgt0b  26850  isosctrlem1  26875  isosctrlem2  26876  chordthmlem4  26892  heron  26895  atanlogaddlem  26970  bndatandm  26986  leibpi  26999  log2tlbnd  27002  birthdaylem3  27010  rlimcnp  27022  rlimcnp2  27023  efrlim  27026  efrlimOLD  27027  cxp2limlem  27033  cxp2lim  27034  divsqrtsumo1  27041  jensenlem2  27045  logdiflbnd  27052  fsumharmonic  27069  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamgulmlem4  27089  lgamgulmlem5  27090  lgamgulmlem6  27091  lgamcvg2  27112  regamcl  27118  wilthlem2  27126  ftalem2  27131  basellem9  27146  vma1  27223  ppieq0  27233  mumullem2  27237  fsumfldivdiaglem  27246  chpeq0  27266  chtub  27270  chpval2  27276  chpchtsum  27277  chpub  27278  logfacrlim  27282  logexprlim  27283  mersenne  27285  perfectlem2  27288  dchrelbas4  27301  bcmono  27335  bposlem1  27342  bposlem2  27343  zabsle1  27354  lgslem3  27357  lgsmod  27381  lgsdir2lem4  27386  lgsdirprm  27389  gausslemma2dlem1a  27423  gausslemma2d  27432  lgsquadlem2  27439  2sqlem8  27484  chebbnd1lem1  27527  chebbnd1lem2  27528  chtppilimlem1  27531  chebbnd2  27535  chto1lb  27536  chpchtlim  27537  chpo1ubb  27539  vmadivsum  27540  rplogsumlem1  27542  rpvmasumlem  27545  dchrisumlem3  27549  dchrmusumlema  27551  dchrmusum2  27552  dchrvmasumlem2  27556  dchrvmasumlem3  27557  dchrvmasumiflem1  27559  dchrvmasumiflem2  27560  dchrisum0flblem1  27566  dchrisum0flblem2  27567  dchrisum0fno1  27569  dchrisum0re  27571  dchrisum0lema  27572  dchrisum0lem1b  27573  dchrisum0lem2a  27575  dchrisum0lem2  27576  dchrisum0lem3  27577  rplogsum  27585  dirith2  27586  mudivsum  27588  mulogsumlem  27589  mulogsum  27590  mulog2sumlem1  27592  mulog2sumlem2  27593  vmalogdivsum2  27596  vmalogdivsum  27597  2vmadivsumlem  27598  log2sumbnd  27602  selberglem2  27604  selberg2lem  27608  chpdifbnd  27613  selberg3lem1  27615  selberg3  27617  selberg4lem1  27618  selberg4  27619  pntrmax  27622  pntrsumo1  27623  pntrsumbnd  27624  selberg3r  27627  selberg4r  27628  selberg34r  27629  pntrlog2bndlem1  27635  pntrlog2bndlem2  27636  pntrlog2bndlem3  27637  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntrlog2bndlem6  27641  pntrlog2bnd  27642  pntpbnd1a  27643  pntpbnd1  27644  pntibndlem2a  27648  pntibndlem2  27649  pntibnd  27651  pntlemc  27653  pntlemg  27656  pntlemr  27660  pntlemk  27664  pnt  27672  qabvle  27683  ostth2lem3  27693  ostth2  27695  trgcgrg  28537  tgcgr4  28553  ttgcontlem1  28913  axpaschlem  28969  axlowdimlem16  28986  axcontlem2  28994  axcontlem7  28999  nbusgrvtxm1  29410  upgrewlkle2  29638  pthdlem1  29798  crctcshwlkn0lem3  29841  crctcshwlkn0lem5  29843  wwlksm1edg  29910  wwlksnextproplem2  29939  clwlkclwwlklem2fv1  30023  clwlkclwwlklem2fv2  30024  clwlkclwwlklem2  30028  clwlkclwwlk2  30031  clwwisshclwwslem  30042  clwwlkf1  30077  clwwlkext2edg  30084  clwlknf1oclwwlknlem1  30109  clwwlknonex2lem2  30136  numclwwlk7  30419  frgrreggt1  30421  frgrogt3nreg  30425  smcnlem  30725  nmoub3i  30801  blocnilem  30832  ubthlem2  30899  minvecolem4  30908  htthlem  30945  nmcexi  32054  nmopcoi  32123  stadd3i  32276  cdj1i  32461  nnmulge  32755  nndiffz1  32794  fzsplit3  32801  wrdt2ind  32922  pmtrto1cl  33101  fzto1st1  33104  fzto1st  33105  psgnfzto1st  33107  cycpmco2lem6  33133  cycpmco2lem7  33134  cycpmrn  33145  qsidomlem1  33459  krull  33486  ply1degltel  33594  ply1degltlss  33596  1smat1  33764  submateqlem1  33767  madjusmdetlem2  33788  unitdivcld  33861  sqsscirc1  33868  nexple  33989  indf1o  34004  esumdivc  34063  dya2ub  34251  dya2iocress  34255  dya2iocbrsiga  34256  dya2icobrsiga  34257  dya2icoseg  34258  dya2iocucvr  34265  sxbrsigalem2  34267  fibp1  34382  probmeasb  34411  dstrvprob  34452  dstfrvunirn  34455  ballotlemfc0  34473  ballotlemfcc  34474  ballotlemsgt1  34491  ballotlemsel1i  34493  ballotlemfrcn0  34510  signsply0  34544  itgexpif  34599  reprlt  34612  chtvalz  34622  breprexplemc  34625  breprexp  34626  circlemeth  34633  tgoldbachgnn  34652  acycgr1v  35133  subfaclim  35172  cvmliftlem2  35270  cvmliftlem13  35280  snmlff  35313  bccolsum  35718  faclim  35725  nn0prpwlem  36304  dnibndlem10  36469  dnibndlem12  36471  knoppcnlem4  36478  unblimceq0  36489  knoppndvlem1  36494  knoppndvlem2  36495  knoppndvlem3  36496  knoppndvlem7  36500  knoppndvlem11  36504  knoppndvlem12  36505  knoppndvlem14  36507  knoppndvlem15  36508  knoppndvlem17  36510  knoppndvlem18  36511  knoppndvlem20  36513  irrdiff  37308  poimirlem6  37612  poimirlem7  37613  poimirlem15  37621  poimirlem19  37625  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimirlem32  37638  broucube  37640  itg2addnclem2  37658  itg2addnclem3  37659  areacirclem1  37694  areacirclem4  37697  incsequz  37734  totbndbnd  37775  bfplem2  37809  resdvopclptsd  42009  lcmineqlem2  42011  lcmineqlem3  42012  lcmineqlem10  42019  lcmineqlem12  42021  lcmineqlem15  42024  lcmineqlem18  42027  lcmineqlem19  42028  lcmineqlem20  42029  lcmineqlem22  42031  lcmineqlem23  42032  3lexlogpow5ineq2  42036  3lexlogpow5ineq4  42037  3lexlogpow5ineq3  42038  3lexlogpow2ineq1  42039  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1lem1  42043  dvrelog2  42045  dvrelog3  42046  dvrelog2b  42047  dvrelogpow2b  42049  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p2  42058  aks4d1p3  42059  aks4d1p5  42061  aks4d1p6  42062  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8d2  42066  aks4d1p8d3  42067  aks4d1p8  42068  aks4d1p9  42069  posbezout  42081  primrootlekpowne0  42086  primrootspoweq0  42087  aks6d1c1  42097  aks6d1c2p2  42100  hashscontpow1  42102  aks6d1c3  42104  aks6d1c2lem4  42108  aks6d1c2  42111  2np3bcnp1  42125  2ap1caineq  42126  sticksstones6  42132  sticksstones7  42133  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  sticksstones22  42149  aks6d1c6lem3  42153  aks6d1c6lem4  42154  bcled  42159  bcle2d  42160  aks6d1c7lem1  42161  aks6d1c7lem2  42162  unitscyglem2  42177  unitscyglem4  42179  unitscyglem5  42180  aks5lem8  42182  metakunt1  42186  metakunt2  42187  metakunt7  42192  metakunt15  42200  metakunt16  42201  metakunt24  42209  metakunt28  42213  metakunt29  42214  2xp3dxp2ge1d  42222  factwoffsmonot  42223  sn-1ne2  42278  redvmptabs  42368  sn-00idlem2  42405  sn-0ne2  42412  rei4  42429  sn-0tie0  42445  sn-nnne0  42454  mulgt0b2d  42466  sn-ltmulgt11d  42468  sn-0lt1  42469  sn-mulgt1d  42471  fimgmcyc  42520  flt4lem7  42645  fltnlta  42649  3cubeslem1  42671  3cubeslem3r  42674  3cubeslem4  42676  lzenom  42757  irrapxlem1  42809  irrapxlem2  42810  irrapxlem4  42812  irrapxlem5  42813  pellexlem2  42817  pell1qrge1  42857  pell1qr1  42858  elpell1qr2  42859  pell14qrgapw  42863  pellfundgt1  42870  pellfundglb  42872  pellfundex  42873  pellfundrp  42875  pellfundne1  42876  rmspecsqrtnq  42893  rmspecnonsq  42894  rmspecfund  42896  rmspecpos  42904  monotoddzzfi  42930  rmygeid  42952  areaquad  43204  imo72b2lem0  44154  imo72b2lem1  44158  imo72b2  44161  cvgdvgrat  44308  radcnvrat  44309  hashnzfzclim  44317  lhe4.4ex1a  44324  binomcxplemnn0  44344  binomcxplemdvbinom  44348  binomcxplemnotnn0  44351  oddfl  45227  abscosbd  45228  zltlesub  45235  abssinbd  45245  monoords  45247  fzisoeu  45250  fzdifsuc2  45260  suplesup  45288  xralrple2  45303  infxr  45316  infleinflem2  45320  reclt0d  45336  xrralrecnnge  45339  sqrlearg  45505  iooiinioc  45508  fmul01  45535  fmul01lt1lem1  45539  fmul01lt1lem2  45540  climsuselem1  45562  sumnnodd  45585  0ellimcdiv  45604  dvmptidg  45872  dvcosax  45881  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvxpaek  45895  dvnmul  45898  iblspltprt  45928  itgspltprt  45934  stoweidlem5  45960  stoweidlem7  45962  stoweidlem10  45965  stoweidlem11  45966  stoweidlem12  45967  stoweidlem13  45968  stoweidlem14  45969  stoweidlem16  45971  stoweidlem18  45973  stoweidlem20  45975  stoweidlem24  45979  stoweidlem25  45980  stoweidlem34  45989  stoweidlem36  45991  stoweidlem38  45993  stoweidlem40  45995  stoweidlem41  45996  stoweidlem42  45997  stoweidlem45  46000  stoweidlem51  46006  stoweidlem60  46015  wallispilem3  46022  wallispilem4  46023  wallispilem5  46024  wallispi  46025  wallispi2lem1  46026  wallispi2lem2  46027  wallispi2  46028  stirlinglem1  46029  stirlinglem3  46031  stirlinglem5  46033  stirlinglem6  46034  stirlinglem7  46035  stirlinglem8  46036  stirlinglem10  46038  stirlinglem11  46039  stirlinglem12  46040  stirlinglem13  46041  stirlinglem15  46043  dirker2re  46047  dirkerval2  46049  dirkerre  46050  dirkertrigeqlem1  46053  dirkertrigeqlem3  46055  dirkeritg  46057  dirkercncflem1  46058  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem5  46067  fourierdlem6  46068  fourierdlem11  46073  fourierdlem15  46077  fourierdlem19  46081  fourierdlem20  46082  fourierdlem24  46086  fourierdlem26  46088  fourierdlem28  46090  fourierdlem30  46092  fourierdlem39  46101  fourierdlem41  46103  fourierdlem43  46105  fourierdlem47  46108  fourierdlem48  46109  fourierdlem56  46117  fourierdlem60  46121  fourierdlem61  46122  fourierdlem62  46123  fourierdlem64  46125  fourierdlem65  46126  fourierdlem66  46127  fourierdlem68  46129  fourierdlem73  46134  fourierdlem78  46139  fourierdlem79  46140  fourierdlem87  46148  fourierdlem103  46164  fourierdlem104  46165  sqwvfoura  46183  fouriersw  46186  etransclem4  46193  etransclem23  46212  etransclem24  46213  etransclem31  46220  etransclem32  46221  etransclem35  46224  etransclem41  46230  etransclem46  46235  etransclem48  46237  etransc  46238  ioorrnopnxrlem  46261  nnfoctbdjlem  46410  iundjiun  46415  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  ovnhoilem1  46556  vonioolem2  46636  vonicclem2  46639  pimrecltneg  46679  smfrec  46744  smfmullem1  46746  smfmullem2  46747  smfdiv  46752  sigaradd  46821  p1lep2  47249  zm1nn  47251  addmodne  47283  m1mod0mod1  47293  iccpartiltu  47346  iccpartlt  47348  iccpartgt  47351  fmtnoge3  47454  fmtnodvds  47468  fmtnoprmfac2lem1  47490  2pwp1prm  47513  flsqrt  47517  sfprmdvdsmersenne  47527  lighneallem2  47530  lighneallem4a  47532  proththdlem  47537  proththd  47538  nnoALTV  47619  bgoldbtbndlem4  47732  2tceilhalfelfzo1  47952  gpgedgvtx0  47953  gpgvtxedg0  47955  gpg3nbgrvtxlem  47957  gpg5nbgrvtx03starlem2  47959  cznnring  48105  divge1b  48357  divgt1b  48358  m1modmmod  48370  difmodm1lt  48371  nn0eo  48377  regt1loggt0  48385  rege1logbrege0  48407  logblt1b  48413  fllog2  48417  nnolog2flm1  48439  dignn0flhalflem1  48464  rrxlinesc  48584  rrxlinec  48585  eenglngeehlnmlem1  48586  eenglngeehlnmlem2  48587  line2ylem  48600  line2  48601  line2xlem  48602  reseccl  48983  recsccl  48984  amgmwlem  49032  amgmlemALT  49033