Theorem 1red 11237

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℝcr 11127  1c1 11129

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-mulcl 11190  ax-mulrcl 11191  ax-i2m1 11196  ax-1ne0 11197  ax-rrecex 11200  ax-cnre 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420

This theorem is used by:  recgt0  12089  mulgt1  12104  ltrec  12125  nnne0  12298  nn0p1gt0  12561  nn0ge2m1nn  12602  nn0le2is012  12689  suprzcl  12705  ledivge1le  13119  ge2halflem1  13163  qbtwnre  13255  lincmb01cmp  13552  iccf1o  13553  xov1plusxeqvd  13555  zltaddlt1le  13562  nnge2recico01  13564  fznatpl1  13637  elfz1b  13652  elfzo0subge1  13765  fzonn0p1p1  13804  elfznelfzo  13833  elfznelfzob  13834  fladdz  13890  2tnp1ge0ge0  13894  flhalf  13895  ltdifltdiv  13899  fldiv4lem1div2uz2  13901  mulp1mod1  13979  m1modge3gt1  13986  modltm1p1mod  13991  addmodlteq  14014  ltexp2a  14234  expcan  14237  ltexp2  14238  leexp2  14239  leexp2a  14240  leexp2r  14242  nnlesq  14273  bernneq3  14299  expnbnd  14300  expnlbnd2  14302  expnngt1  14309  fzsdom2  14497  wrdlenge2n0  14621  swrd2lsw  15029  2swrd2eqwrdeq  15030  01sqrexlem7  15339  rddif  15432  reccn2  15688  rlimo1  15708  o1fsum  15904  abscvgcvg  15910  climcndslem1  15942  flo1  15947  harmonic  15952  geomulcvg  15969  fprodrecl  16046  fprodreclf  16052  fprodle  16089  bpoly4  16151  efcllem  16169  efgt1  16210  tanhlt1  16254  sinltx  16283  eirrlem  16298  p1modz1  16355  mod2eq1n2dvds  16443  oddge22np1  16445  ltoddhalfle  16457  nn0o1gt2  16477  nno  16478  nn0oddm1d2  16481  nnoddm1d2  16482  bitsfzolem  16530  bitsfzo  16531  bitsmod  16532  bitscmp  16534  bitsinv1lem  16537  smuval2  16578  coprmgcdb  16745  prmind2  16781  dvdsnprmd  16786  2mulprm  16789  isprm5  16804  isprm7  16805  divdenle  16846  zsqrtelqelz  16855  fermltl  16881  odzdvds  16893  modprm0  16903  iserodd  16933  difsqpwdvds  16985  pcfaclem  16996  prmreclem1  17014  4sqlem11  17053  4sqlem12  17054  ramub1lem1  17124  prmgaplem8  17156  2expltfac  17190  chnccat  18720  pgpfaclem2  20217  qsidomlem1  21549  znidomb  21780  psdmvr  22403  chfacfisf  23085  chfacfisfcpmat  23086  chfacfscmulgsum  23091  chfacfpmmulgsum  23095  nrginvrcnlem  24923  nmoid  24974  xrsmopn  25045  metnrmlem1a  25091  iihalf2cn  25168  iccpnfhmeo  25179  lebnumii  25200  htpycc  25214  pcohtpylem  25253  pcoass  25258  pcorevlem  25260  nmhmcn  25354  cncmet  25556  ovoliunlem1  25736  dyadmaxlem  25831  vitalilem2  25843  mbfi1fseqlem6  25954  itg2mulc  25981  itg2monolem1  25984  itg2monolem3  25986  dveflem  26213  mvth  26226  dvlipcn  26228  lhop1lem  26247  dvfsumlem1  26260  dvfsumlem2  26261  dvfsumlem3  26262  dvfsumlem4  26263  dvfsum2  26268  fta1glem2  26401  plyeq0lem  26443  fta1lem  26544  vieta1lem2  26550  aalioulem3  26577  aalioulem4  26578  radcnvlem1  26656  radcnvlem2  26657  dvradcnv  26664  abelthlem2  26675  abelthlem5  26678  abelthlem7  26681  abelth2  26685  cos02pilt1  26771  cosne0  26774  rplogcl  26849  logdivlti  26865  logno1  26881  dvlog2lem  26897  advlog  26899  logtayllem  26904  cxplt  26939  cxple  26940  cxpaddlelem  26996  cxpaddle  26997  rtprmirr  27005  relogbf  27036  logbgt0b  27038  isosctrlem1  27063  isosctrlem2  27064  chordthmlem4  27080  heron  27083  atanlogaddlem  27158  bndatandm  27174  leibpi  27187  log2tlbnd  27190  birthdaylem3  27198  rlimcnp  27210  rlimcnp2  27211  efrlim  27214  cxp2limlem  27220  cxp2lim  27221  divsqrtsumo1  27228  jensenlem2  27232  logdiflbnd  27239  fsumharmonic  27256  lgamgulmlem2  27274  lgamgulmlem3  27275  lgamgulmlem4  27276  lgamgulmlem5  27277  lgamgulmlem6  27278  lgamcvg2  27299  regamcl  27305  wilthlem2  27313  ftalem2  27318  basellem9  27333  vma1  27410  ppieq0  27420  mumullem2  27424  fsumfldivdiaglem  27433  ppiub  27448  chpeq0  27452  chtub  27456  chpval2  27462  chpchtsum  27463  chpub  27464  logfacrlim  27468  logexprlim  27469  mersenne  27471  perfectlem2  27474  dchrelbas4  27487  bcmono  27521  bposlem1  27528  bposlem2  27529  zabsle1  27540  lgslem3  27543  lgsmod  27567  lgsdir2lem4  27572  lgsdirprm  27575  gausslemma2dlem1a  27609  gausslemma2d  27618  lgsquadlem2  27625  2sqlem8  27670  chebbnd1lem1  27713  chebbnd1lem2  27714  chtppilimlem1  27717  chebbnd2  27721  chto1lb  27722  chpchtlim  27723  chpo1ubb  27725  vmadivsum  27726  rplogsumlem1  27728  rpvmasumlem  27731  dchrisumlem3  27735  dchrmusumlema  27737  dchrmusum2  27738  dchrvmasumlem2  27742  dchrvmasumlem3  27743  dchrvmasumiflem1  27745  dchrvmasumiflem2  27746  dchrisum0flblem1  27752  dchrisum0flblem2  27753  dchrisum0fno1  27755  dchrisum0re  27757  dchrisum0lema  27758  dchrisum0lem1b  27759  dchrisum0lem2a  27761  dchrisum0lem2  27762  dchrisum0lem3  27763  rplogsum  27771  dirith2  27772  mudivsum  27774  mulogsumlem  27775  mulogsum  27776  mulog2sumlem1  27778  mulog2sumlem2  27779  vmalogdivsum2  27782  vmalogdivsum  27783  2vmadivsumlem  27784  log2sumbnd  27788  selberglem2  27790  selberg2lem  27794  chpdifbnd  27799  selberg3lem1  27801  selberg3  27803  selberg4lem1  27804  selberg4  27805  pntrmax  27808  pntrsumo1  27809  pntrsumbnd  27810  selberg3r  27813  selberg4r  27814  selberg34r  27815  pntrlog2bndlem1  27821  pntrlog2bndlem2  27822  pntrlog2bndlem3  27823  pntrlog2bndlem4  27824  pntrlog2bndlem5  27825  pntrlog2bndlem6  27827  pntrlog2bnd  27828  pntpbnd1a  27829  pntpbnd1  27830  pntibndlem2a  27834  pntibndlem2  27835  pntibnd  27837  pntlemc  27839  pntlemg  27842  pntlemr  27846  pntlemk  27850  pnt  27858  qabvle  27869  ostth2lem3  27879  ostth2  27881  trgcgrg  28865  tgcgr4  28881  ttgcontlem1  29349  axpaschlem  29405  axlowdimlem16  29422  axcontlem2  29430  axcontlem7  29435  nbusgrvtxm1  29847  upgrewlkle2  30074  pthdlem1  30239  crctcshwlkn0lem3  30288  crctcshwlkn0lem5  30290  wwlksm1edg  30357  wwlksnextproplem2  30386  clwlkclwwlklem2fv1  30473  clwlkclwwlklem2fv2  30474  clwlkclwwlklem2  30478  clwlkclwwlk2  30481  clwwisshclwwslem  30492  clwwlkf1  30527  clwwlkext2edg  30534  clwlknf1oclwwlknlem1  30559  clwwlknonex2lem2  30586  numclwwlk7  30879  frgrreggt1  30881  frgrogt3nreg  30885  smcnlem  31186  nmoub3i  31262  blocnilem  31293  ubthlem2  31360  minvecolem4  31369  htthlem  31406  nmcexi  32515  nmopcoi  32584  stadd3i  32737  cdj1i  32922  nnmulge  33218  receqid  33223  nndiffz1  33265  fzsplit3  33272  nexple  33311  indf1o  33318  wrdt2ind  33403  pmtrto1cl  33547  fzto1st1  33550  fzto1st  33551  psgnfzto1st  33553  cycpmco2lem6  33579  cycpmco2lem7  33580  cycpmrn  33591  krull  33889  ply1degltel  34012  ply1degltlss  34014  constrnegcl  34281  constrdircl  34283  iconstr  34284  constrrecl  34287  constrmulcl  34289  constrreinvcl  34290  constrresqrtcl  34295  cos9thpiminplylem1  34300  cos9thpiminply  34306  cos9thpinconstrlem1  34307  1smat1  34322  submateqlem1  34325  madjusmdetlem2  34346  unitdivcld  34419  sqsscirc1  34426  esumdivc  34601  dya2ub  34789  dya2iocress  34793  dya2iocbrsiga  34794  dya2icobrsiga  34795  dya2icoseg  34796  dya2iocucvr  34803  sxbrsigalem2  34805  fibp1  34920  probmeasb  34949  dstrvprob  34991  dstfrvunirn  34994  ballotlemfc0  35012  ballotlemfcc  35013  ballotlemsgt1  35030  ballotlemsel1i  35032  ballotlemfrcn0  35049  signsply0  35067  itgexpif  35122  reprlt  35135  chtvalz  35145  breprexplemc  35148  breprexp  35149  circlemeth  35156  tgoldbachgnn  35175  acycgr1v  35736  subfaclim  35775  cvmliftlem2  35873  cvmliftlem13  35883  snmlff  35916  bccolsum  36326  faclim  36333  nn0prpwlem  36949  dnibndlem10  37192  dnibndlem12  37194  knoppcnlem4  37201  unblimceq0  37212  knoppndvlem1  37217  knoppndvlem2  37218  knoppndvlem3  37219  knoppndvlem7  37223  knoppndvlem11  37227  knoppndvlem12  37228  knoppndvlem14  37230  knoppndvlem15  37231  knoppndvlem17  37233  knoppndvlem18  37234  knoppndvlem20  37236  irrdiff  38086  poimirlem6  38383  poimirlem7  38384  poimirlem15  38392  poimirlem19  38396  poimirlem29  38406  poimirlem30  38407  poimirlem31  38408  poimirlem32  38409  broucube  38411  itg2addnclem2  38429  itg2addnclem3  38430  areacirclem1  38465  areacirclem4  38468  incsequz  38506  totbndbnd  38547  bfplem2  38581  resdvopclptsd  42902  lcmineqlem2  42904  lcmineqlem3  42905  lcmineqlem10  42912  lcmineqlem12  42914  lcmineqlem15  42917  lcmineqlem18  42920  lcmineqlem19  42921  lcmineqlem20  42922  lcmineqlem22  42924  lcmineqlem23  42925  3lexlogpow5ineq2  42929  3lexlogpow5ineq4  42930  3lexlogpow5ineq3  42931  3lexlogpow2ineq1  42932  3lexlogpow2ineq2  42933  3lexlogpow5ineq5  42934  aks4d1lem1  42936  dvrelog2  42938  dvrelog3  42939  dvrelog2b  42940  dvrelogpow2b  42942  aks4d1p1p3  42943  aks4d1p1p2  42944  aks4d1p1p4  42945  aks4d1p1p6  42947  aks4d1p1p7  42948  aks4d1p1p5  42949  aks4d1p1  42950  aks4d1p2  42951  aks4d1p3  42952  aks4d1p5  42954  aks4d1p6  42955  aks4d1p7d1  42956  aks4d1p7  42957  aks4d1p8d2  42959  aks4d1p8d3  42960  aks4d1p8  42961  aks4d1p9  42962  posbezout  42974  primrootlekpowne0  42979  primrootspoweq0  42980  aks6d1c1  42990  aks6d1c2p2  42993  hashscontpow1  42995  aks6d1c3  42997  aks6d1c2lem4  43001  aks6d1c2  43004  2np3bcnp1  43018  2ap1caineq  43019  sticksstones6  43025  sticksstones7  43026  sticksstones10  43029  sticksstones12a  43031  sticksstones12  43032  sticksstones22  43042  aks6d1c6lem3  43046  aks6d1c6lem4  43047  bcled  43052  bcle2d  43053  aks6d1c7lem1  43054  aks6d1c7lem2  43055  unitscyglem2  43070  unitscyglem4  43072  unitscyglem5  43073  aks5lem8  43075  sn-1ne2  43154  redvmptabs  43243  sn-00idlem2  43282  sn-0ne2  43289  rei4  43307  rediveq1d  43334  sn-rediv1d  43335  sn-rereccld  43338  rerecne0d  43339  rerecidd  43340  rerecrecd  43342  sn-0tie0  43347  sn-nnne0  43356  mulgt0b1d  43368  sn-ltmulgt11d  43370  sn-0lt1  43371  sn-mulgt1d  43375  fimgmcyc  43424  flt4lem7  43513  fltnlta  43517  3cubeslem1  43537  3cubeslem3r  43540  3cubeslem4  43542  lzenom  43623  irrapxlem1  43671  irrapxlem2  43672  irrapxlem4  43674  irrapxlem5  43675  pellexlem2  43679  pell1qrge1  43719  pell1qr1  43720  elpell1qr2  43721  pell14qrgapw  43725  pellfundgt1  43732  pellfundglb  43734  pellfundex  43735  pellfundrp  43737  pellfundne1  43738  rmspecsqrtnq  43755  rmspecnonsq  43756  rmspecfund  43758  rmspecpos  43765  monotoddzzfi  43791  rmygeid  43813  areaquad  44065  imo72b2lem0  45013  imo72b2lem1  45017  imo72b2  45020  cvgdvgrat  45145  radcnvrat  45146  hashnzfzclim  45154  lhe4.4ex1a  45161  binomcxplemnn0  45181  binomcxplemdvbinom  45185  binomcxplemnotnn0  45188  oddfl  46119  abscosbd  46120  zltlesub  46126  abssinbd  46136  monoords  46138  fzisoeu  46141  fzdifsuc2  46151  suplesup  46177  xralrple2  46192  infxr  46204  infleinflem2  46208  reclt0d  46224  xrralrecnnge  46227  sqrlearg  46391  iooiinioc  46394  fmul01  46418  fmul01lt1lem1  46422  fmul01lt1lem2  46423  climsuselem1  46445  sumnnodd  46468  0ellimcdiv  46485  dvmptidg  46753  dvcosax  46762  ioodvbdlimc1lem1  46767  ioodvbdlimc1lem2  46768  ioodvbdlimc2lem  46770  dvxpaek  46776  dvnmul  46779  iblspltprt  46809  itgspltprt  46815  stoweidlem5  46841  stoweidlem7  46843  stoweidlem10  46846  stoweidlem11  46847  stoweidlem12  46848  stoweidlem13  46849  stoweidlem14  46850  stoweidlem16  46852  stoweidlem18  46854  stoweidlem20  46856  stoweidlem24  46860  stoweidlem25  46861  stoweidlem34  46870  stoweidlem36  46872  stoweidlem38  46874  stoweidlem40  46876  stoweidlem41  46877  stoweidlem42  46878  stoweidlem45  46881  stoweidlem51  46887  stoweidlem60  46896  wallispilem3  46903  wallispilem4  46904  wallispilem5  46905  wallispi  46906  wallispi2lem1  46907  wallispi2lem2  46908  wallispi2  46909  stirlinglem1  46910  stirlinglem3  46912  stirlinglem5  46914  stirlinglem6  46915  stirlinglem7  46916  stirlinglem8  46917  stirlinglem10  46919  stirlinglem11  46920  stirlinglem12  46921  stirlinglem13  46922  stirlinglem15  46924  dirker2re  46928  dirkerval2  46930  dirkerre  46931  dirkertrigeqlem1  46934  dirkertrigeqlem3  46936  dirkeritg  46938  dirkercncflem1  46939  dirkercncflem2  46940  dirkercncflem4  46942  fourierdlem5  46948  fourierdlem6  46949  fourierdlem11  46954  fourierdlem15  46958  fourierdlem19  46962  fourierdlem20  46963  fourierdlem24  46967  fourierdlem26  46969  fourierdlem28  46971  fourierdlem30  46973  fourierdlem39  46982  fourierdlem41  46984  fourierdlem43  46986  fourierdlem47  46989  fourierdlem48  46990  fourierdlem56  46998  fourierdlem60  47002  fourierdlem61  47003  fourierdlem62  47004  fourierdlem64  47006  fourierdlem65  47007  fourierdlem66  47008  fourierdlem68  47010  fourierdlem73  47015  fourierdlem78  47020  fourierdlem79  47021  fourierdlem87  47029  fourierdlem103  47045  fourierdlem104  47046  sqwvfoura  47064  fouriersw  47067  etransclem4  47074  etransclem23  47093  etransclem24  47094  etransclem31  47101  etransclem32  47102  etransclem35  47105  etransclem41  47111  etransclem46  47116  etransclem48  47118  etransc  47119  ioorrnopnxrlem  47142  nnfoctbdjlem  47291  iundjiun  47296  hoidmvlelem1  47431  hoidmvlelem2  47432  hoidmvlelem3  47433  hoidmvlelem4  47434  ovnhoilem1  47437  vonioolem2  47517  vonicclem2  47520  pimrecltneg  47560  smfrec  47625  smfmullem1  47627  smfmullem2  47628  smfdiv  47633  sigaradd  47702  ormkglobd  47713  cjnpoly  47765  p1lep2  48196  zm1nn  48198  ceilhalfgt1  48229  2tceilhalfelfzo1  48232  ceilbi  48233  rehalfge1  48235  ceilhalfnn  48236  flmrecm1  48239  addmodne  48246  m1mod0mod1  48256  m1modmmod  48260  difmodm1lt  48261  modmknepk  48264  modp2nep1  48269  modm1nem2  48271  2timesltsqm1  48275  muldvdsfacm1  48283  iccpartiltu  48330  iccpartlt  48332  iccpartgt  48335  fmtnoge3  48441  fmtnodvds  48455  fmtnoprmfac2lem1  48477  2pwp1prm  48500  flsqrt  48504  sfprmdvdsmersenne  48514  lighneallem2  48517  lighneallem4a  48519  proththdlem  48524  proththd  48525  nprmdvdsfacm1lem4  48534  nnoALTV  48619  bgoldbtbndlem4  48732  gpgprismgrusgra  48982  gpgedgvtx0  48985  gpgvtxedg0  48987  gpg5nbgrvtx03starlem2  48993  gpg3kgrtriexlem4  49010  gpg3kgrtriexlem6  49012  cznnring  49185  divge1b  49450  divgt1b  49451  nn0eo  49466  regt1loggt0  49474  rege1logbrege0  49496  logblt1b  49502  fllog2  49506  nnolog2flm1  49528  dignn0flhalflem1  49553  rrxlinesc  49673  rrxlinec  49674  eenglngeehlnmlem1  49675  eenglngeehlnmlem2  49676  line2ylem  49689  line2  49690  line2xlem  49691  reseccl  50687  recsccl  50688  amgmwlem  50828  amgmlemALT  50829