Theorem 1red 11227

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℝcr 11117  1c1 11119

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 2148  ax-9 2156  ax-ext 2738  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-mulcl 11180  ax-mulrcl 11181  ax-i2m1 11186  ax-1ne0 11187  ax-rrecex 11190  ax-cnre 11191

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 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6499  df-fv 6551  df-ov 7426

This theorem is used by:  recgt0  12079  mulgt1  12094  ltrec  12115  nnne0  12288  nn0p1gt0  12551  nn0ge2m1nn  12592  nn0le2is012  12678  suprzcl  12694  ledivge1le  13107  ge2halflem1  13151  qbtwnre  13243  lincmb01cmp  13540  iccf1o  13541  xov1plusxeqvd  13543  zltaddlt1le  13550  nnge2recico01  13552  fznatpl1  13625  elfz1b  13640  elfzo0subge1  13753  fzonn0p1p1  13792  elfznelfzo  13821  elfznelfzob  13822  fladdz  13878  2tnp1ge0ge0  13882  flhalf  13883  ltdifltdiv  13887  fldiv4lem1div2uz2  13889  mulp1mod1  13967  m1modge3gt1  13974  modltm1p1mod  13979  addmodlteq  14002  ltexp2a  14222  expcan  14225  ltexp2  14226  leexp2  14227  leexp2a  14228  leexp2r  14230  nnlesq  14261  bernneq3  14287  expnbnd  14288  expnlbnd2  14290  expnngt1  14297  fzsdom2  14485  wrdlenge2n0  14609  swrd2lsw  15015  2swrd2eqwrdeq  15016  01sqrexlem7  15325  rddif  15418  reccn2  15674  rlimo1  15694  o1fsum  15891  abscvgcvg  15897  climcndslem1  15929  flo1  15934  harmonic  15939  geomulcvg  15956  fprodrecl  16033  fprodreclf  16039  fprodle  16076  bpoly4  16138  efcllem  16156  efgt1  16197  tanhlt1  16241  sinltx  16270  eirrlem  16285  p1modz1  16342  mod2eq1n2dvds  16430  oddge22np1  16432  ltoddhalfle  16444  nn0o1gt2  16464  nno  16465  nn0oddm1d2  16468  nnoddm1d2  16469  bitsfzolem  16517  bitsfzo  16518  bitsmod  16519  bitscmp  16521  bitsinv1lem  16524  smuval2  16565  coprmgcdb  16732  prmind2  16768  dvdsnprmd  16773  2mulprm  16776  isprm5  16791  isprm7  16792  divdenle  16833  zsqrtelqelz  16842  fermltl  16868  odzdvds  16880  modprm0  16890  iserodd  16920  difsqpwdvds  16972  pcfaclem  16983  prmreclem1  17001  4sqlem11  17040  4sqlem12  17041  ramub1lem1  17111  prmgaplem8  17143  2expltfac  17177  chnccat  18707  pgpfaclem2  20185  qsidomlem1  21517  znidomb  21748  psdmvr  22369  chfacfisf  23048  chfacfisfcpmat  23049  chfacfscmulgsum  23054  chfacfpmmulgsum  23058  nrginvrcnlem  24885  nmoid  24936  xrsmopn  25007  metnrmlem1a  25053  iihalf2cn  25130  iccpnfhmeo  25141  lebnumii  25162  htpycc  25176  pcohtpylem  25215  pcoass  25220  pcorevlem  25222  nmhmcn  25316  cncmet  25518  ovoliunlem1  25698  dyadmaxlem  25793  vitalilem2  25805  mbfi1fseqlem6  25916  itg2mulc  25943  itg2monolem1  25946  itg2monolem3  25948  dveflem  26175  mvth  26188  dvlipcn  26190  lhop1lem  26209  dvfsumlem1  26222  dvfsumlem2  26223  dvfsumlem3  26224  dvfsumlem4  26225  dvfsum2  26230  fta1glem2  26363  plyeq0lem  26404  fta1lem  26505  vieta1lem2  26509  aalioulem3  26534  aalioulem4  26535  radcnvlem1  26613  radcnvlem2  26614  dvradcnv  26621  abelthlem2  26632  abelthlem5  26635  abelthlem7  26638  abelth2  26642  cos02pilt1  26728  cosne0  26731  rplogcl  26806  logdivlti  26822  logno1  26838  dvlog2lem  26854  advlog  26856  logtayllem  26861  cxplt  26896  cxple  26897  cxpaddlelem  26953  cxpaddle  26954  rtprmirr  26962  relogbf  26993  logbgt0b  26995  isosctrlem1  27020  isosctrlem2  27021  chordthmlem4  27037  heron  27040  atanlogaddlem  27115  bndatandm  27131  leibpi  27144  log2tlbnd  27147  birthdaylem3  27155  rlimcnp  27167  rlimcnp2  27168  efrlim  27171  cxp2limlem  27177  cxp2lim  27178  divsqrtsumo1  27185  jensenlem2  27189  logdiflbnd  27196  fsumharmonic  27213  lgamgulmlem2  27231  lgamgulmlem3  27232  lgamgulmlem4  27233  lgamgulmlem5  27234  lgamgulmlem6  27235  lgamcvg2  27256  regamcl  27262  wilthlem2  27270  ftalem2  27275  basellem9  27290  vma1  27367  ppieq0  27377  mumullem2  27381  fsumfldivdiaglem  27390  ppiub  27405  chpeq0  27409  chtub  27413  chpval2  27419  chpchtsum  27420  chpub  27421  logfacrlim  27425  logexprlim  27426  mersenne  27428  perfectlem2  27431  dchrelbas4  27444  bcmono  27478  bposlem1  27485  bposlem2  27486  zabsle1  27497  lgslem3  27500  lgsmod  27524  lgsdir2lem4  27529  lgsdirprm  27532  gausslemma2dlem1a  27566  gausslemma2d  27575  lgsquadlem2  27582  2sqlem8  27627  chebbnd1lem1  27670  chebbnd1lem2  27671  chtppilimlem1  27674  chebbnd2  27678  chto1lb  27679  chpchtlim  27680  chpo1ubb  27682  vmadivsum  27683  rplogsumlem1  27685  rpvmasumlem  27688  dchrisumlem3  27692  dchrmusumlema  27694  dchrmusum2  27695  dchrvmasumlem2  27699  dchrvmasumlem3  27700  dchrvmasumiflem1  27702  dchrvmasumiflem2  27703  dchrisum0flblem1  27709  dchrisum0flblem2  27710  dchrisum0fno1  27712  dchrisum0re  27714  dchrisum0lema  27715  dchrisum0lem1b  27716  dchrisum0lem2a  27718  dchrisum0lem2  27719  dchrisum0lem3  27720  rplogsum  27728  dirith2  27729  mudivsum  27731  mulogsumlem  27732  mulogsum  27733  mulog2sumlem1  27735  mulog2sumlem2  27736  vmalogdivsum2  27739  vmalogdivsum  27740  2vmadivsumlem  27741  log2sumbnd  27745  selberglem2  27747  selberg2lem  27751  chpdifbnd  27756  selberg3lem1  27758  selberg3  27760  selberg4lem1  27761  selberg4  27762  pntrmax  27765  pntrsumo1  27766  pntrsumbnd  27767  selberg3r  27770  selberg4r  27771  selberg34r  27772  pntrlog2bndlem1  27778  pntrlog2bndlem2  27779  pntrlog2bndlem3  27780  pntrlog2bndlem4  27781  pntrlog2bndlem5  27782  pntrlog2bndlem6  27784  pntrlog2bnd  27785  pntpbnd1a  27786  pntpbnd1  27787  pntibndlem2a  27791  pntibndlem2  27792  pntibnd  27794  pntlemc  27796  pntlemg  27799  pntlemr  27803  pntlemk  27807  pnt  27815  qabvle  27826  ostth2lem3  27836  ostth2  27838  trgcgrg  28821  tgcgr4  28837  ttgcontlem1  29271  axpaschlem  29327  axlowdimlem16  29344  axcontlem2  29352  axcontlem7  29357  nbusgrvtxm1  29766  upgrewlkle2  29993  pthdlem1  30152  crctcshwlkn0lem3  30198  crctcshwlkn0lem5  30200  wwlksm1edg  30267  wwlksnextproplem2  30296  clwlkclwwlklem2fv1  30383  clwlkclwwlklem2fv2  30384  clwlkclwwlklem2  30388  clwlkclwwlk2  30391  clwwisshclwwslem  30402  clwwlkf1  30437  clwwlkext2edg  30444  clwlknf1oclwwlknlem1  30469  clwwlknonex2lem2  30496  numclwwlk7  30779  frgrreggt1  30781  frgrogt3nreg  30785  smcnlem  31086  nmoub3i  31162  blocnilem  31193  ubthlem2  31260  minvecolem4  31269  htthlem  31306  nmcexi  32415  nmopcoi  32484  stadd3i  32637  cdj1i  32822  nnmulge  33121  receqid  33126  nndiffz1  33168  fzsplit3  33175  nexple  33214  indf1o  33221  wrdt2ind  33306  pmtrto1cl  33450  fzto1st1  33453  fzto1st  33454  psgnfzto1st  33456  cycpmco2lem6  33482  cycpmco2lem7  33483  cycpmrn  33494  krull  33792  ply1degltel  33915  ply1degltlss  33917  constrnegcl  34184  constrdircl  34186  iconstr  34187  constrrecl  34190  constrmulcl  34192  constrreinvcl  34193  constrresqrtcl  34198  cos9thpiminplylem1  34203  cos9thpiminply  34209  cos9thpinconstrlem1  34210  1smat1  34225  submateqlem1  34228  madjusmdetlem2  34249  unitdivcld  34322  sqsscirc1  34329  esumdivc  34504  dya2ub  34691  dya2iocress  34695  dya2iocbrsiga  34696  dya2icobrsiga  34697  dya2icoseg  34698  dya2iocucvr  34705  sxbrsigalem2  34707  fibp1  34822  probmeasb  34851  dstrvprob  34893  dstfrvunirn  34896  ballotlemfc0  34914  ballotlemfcc  34915  ballotlemsgt1  34932  ballotlemsel1i  34934  ballotlemfrcn0  34951  signsply0  34969  itgexpif  35024  reprlt  35037  chtvalz  35047  breprexplemc  35050  breprexp  35051  circlemeth  35058  tgoldbachgnn  35077  acycgr1v  35661  subfaclim  35700  cvmliftlem2  35798  cvmliftlem13  35808  snmlff  35841  bccolsum  36251  faclim  36258  nn0prpwlem  36873  dnibndlem10  37116  dnibndlem12  37118  knoppcnlem4  37125  unblimceq0  37136  knoppndvlem1  37141  knoppndvlem2  37142  knoppndvlem3  37143  knoppndvlem7  37147  knoppndvlem11  37151  knoppndvlem12  37152  knoppndvlem14  37154  knoppndvlem15  37155  knoppndvlem17  37157  knoppndvlem18  37158  knoppndvlem20  37160  irrdiff  38010  poimirlem6  38317  poimirlem7  38318  poimirlem15  38326  poimirlem19  38330  poimirlem29  38340  poimirlem30  38341  poimirlem31  38342  poimirlem32  38343  broucube  38345  itg2addnclem2  38363  itg2addnclem3  38364  areacirclem1  38399  areacirclem4  38402  incsequz  38439  totbndbnd  38480  bfplem2  38514  resdvopclptsd  42835  lcmineqlem2  42837  lcmineqlem3  42838  lcmineqlem10  42845  lcmineqlem12  42847  lcmineqlem15  42850  lcmineqlem18  42853  lcmineqlem19  42854  lcmineqlem20  42855  lcmineqlem22  42857  lcmineqlem23  42858  3lexlogpow5ineq2  42862  3lexlogpow5ineq4  42863  3lexlogpow5ineq3  42864  3lexlogpow2ineq1  42865  3lexlogpow2ineq2  42866  3lexlogpow5ineq5  42867  aks4d1lem1  42869  dvrelog2  42871  dvrelog3  42872  dvrelog2b  42873  dvrelogpow2b  42875  aks4d1p1p3  42876  aks4d1p1p2  42877  aks4d1p1p4  42878  aks4d1p1p6  42880  aks4d1p1p7  42881  aks4d1p1p5  42882  aks4d1p1  42883  aks4d1p2  42884  aks4d1p3  42885  aks4d1p5  42887  aks4d1p6  42888  aks4d1p7d1  42889  aks4d1p7  42890  aks4d1p8d2  42892  aks4d1p8d3  42893  aks4d1p8  42894  aks4d1p9  42895  posbezout  42907  primrootlekpowne0  42912  primrootspoweq0  42913  aks6d1c1  42923  aks6d1c2p2  42926  hashscontpow1  42928  aks6d1c3  42930  aks6d1c2lem4  42934  aks6d1c2  42937  2np3bcnp1  42951  2ap1caineq  42952  sticksstones6  42958  sticksstones7  42959  sticksstones10  42962  sticksstones12a  42964  sticksstones12  42965  sticksstones22  42975  aks6d1c6lem3  42979  aks6d1c6lem4  42980  bcled  42985  bcle2d  42986  aks6d1c7lem1  42987  aks6d1c7lem2  42988  unitscyglem2  43003  unitscyglem4  43005  unitscyglem5  43006  aks5lem8  43008  sn-1ne2  43072  redvmptabs  43161  sn-00idlem2  43200  sn-0ne2  43207  rei4  43225  rediveq1d  43252  sn-rediv1d  43253  sn-rereccld  43256  rerecne0d  43257  rerecidd  43258  rerecrecd  43260  sn-0tie0  43265  sn-nnne0  43274  mulgt0b1d  43286  sn-ltmulgt11d  43288  sn-0lt1  43289  sn-mulgt1d  43293  fimgmcyc  43342  flt4lem7  43431  fltnlta  43435  3cubeslem1  43455  3cubeslem3r  43458  3cubeslem4  43460  lzenom  43541  irrapxlem1  43589  irrapxlem2  43590  irrapxlem4  43592  irrapxlem5  43593  pellexlem2  43597  pell1qrge1  43637  pell1qr1  43638  elpell1qr2  43639  pell14qrgapw  43643  pellfundgt1  43650  pellfundglb  43652  pellfundex  43653  pellfundrp  43655  pellfundne1  43656  rmspecsqrtnq  43673  rmspecnonsq  43674  rmspecfund  43676  rmspecpos  43683  monotoddzzfi  43709  rmygeid  43731  areaquad  43983  imo72b2lem0  44931  imo72b2lem1  44935  imo72b2  44938  cvgdvgrat  45063  radcnvrat  45064  hashnzfzclim  45072  lhe4.4ex1a  45079  binomcxplemnn0  45099  binomcxplemdvbinom  45103  binomcxplemnotnn0  45106  oddfl  46037  abscosbd  46038  zltlesub  46044  abssinbd  46054  monoords  46056  fzisoeu  46059  fzdifsuc2  46069  suplesup  46095  xralrple2  46110  infxr  46122  infleinflem2  46126  reclt0d  46142  xrralrecnnge  46145  sqrlearg  46309  iooiinioc  46312  fmul01  46336  fmul01lt1lem1  46340  fmul01lt1lem2  46341  climsuselem1  46363  sumnnodd  46386  0ellimcdiv  46403  dvmptidg  46671  dvcosax  46680  ioodvbdlimc1lem1  46685  ioodvbdlimc1lem2  46686  ioodvbdlimc2lem  46688  dvxpaek  46694  dvnmul  46697  iblspltprt  46727  itgspltprt  46733  stoweidlem5  46759  stoweidlem7  46761  stoweidlem10  46764  stoweidlem11  46765  stoweidlem12  46766  stoweidlem13  46767  stoweidlem14  46768  stoweidlem16  46770  stoweidlem18  46772  stoweidlem20  46774  stoweidlem24  46778  stoweidlem25  46779  stoweidlem34  46788  stoweidlem36  46790  stoweidlem38  46792  stoweidlem40  46794  stoweidlem41  46795  stoweidlem42  46796  stoweidlem45  46799  stoweidlem51  46805  stoweidlem60  46814  wallispilem3  46821  wallispilem4  46822  wallispilem5  46823  wallispi  46824  wallispi2lem1  46825  wallispi2lem2  46826  wallispi2  46827  stirlinglem1  46828  stirlinglem3  46830  stirlinglem5  46832  stirlinglem6  46833  stirlinglem7  46834  stirlinglem8  46835  stirlinglem10  46837  stirlinglem11  46838  stirlinglem12  46839  stirlinglem13  46840  stirlinglem15  46842  dirker2re  46846  dirkerval2  46848  dirkerre  46849  dirkertrigeqlem1  46852  dirkertrigeqlem3  46854  dirkeritg  46856  dirkercncflem1  46857  dirkercncflem2  46858  dirkercncflem4  46860  fourierdlem5  46866  fourierdlem6  46867  fourierdlem11  46872  fourierdlem15  46876  fourierdlem19  46880  fourierdlem20  46881  fourierdlem24  46885  fourierdlem26  46887  fourierdlem28  46889  fourierdlem30  46891  fourierdlem39  46900  fourierdlem41  46902  fourierdlem43  46904  fourierdlem47  46907  fourierdlem48  46908  fourierdlem56  46916  fourierdlem60  46920  fourierdlem61  46921  fourierdlem62  46922  fourierdlem64  46924  fourierdlem65  46925  fourierdlem66  46926  fourierdlem68  46928  fourierdlem73  46933  fourierdlem78  46938  fourierdlem79  46939  fourierdlem87  46947  fourierdlem103  46963  fourierdlem104  46964  sqwvfoura  46982  fouriersw  46985  etransclem4  46992  etransclem23  47011  etransclem24  47012  etransclem31  47019  etransclem32  47020  etransclem35  47023  etransclem41  47029  etransclem46  47034  etransclem48  47036  etransc  47037  ioorrnopnxrlem  47060  nnfoctbdjlem  47209  iundjiun  47214  hoidmvlelem1  47349  hoidmvlelem2  47350  hoidmvlelem3  47351  hoidmvlelem4  47352  ovnhoilem1  47355  vonioolem2  47435  vonicclem2  47438  pimrecltneg  47478  smfrec  47543  smfmullem1  47545  smfmullem2  47546  smfdiv  47551  sigaradd  47620  ormkglobd  47631  cjnpoly  47666  p1lep2  48077  zm1nn  48079  ceilhalfgt1  48110  2tceilhalfelfzo1  48113  ceilbi  48114  rehalfge1  48116  ceilhalfnn  48117  flmrecm1  48120  addmodne  48127  m1mod0mod1  48137  m1modmmod  48141  difmodm1lt  48142  modmknepk  48145  modp2nep1  48150  modm1nem2  48152  2timesltsqm1  48156  muldvdsfacm1  48164  iccpartiltu  48211  iccpartlt  48213  iccpartgt  48216  fmtnoge3  48322  fmtnodvds  48336  fmtnoprmfac2lem1  48358  2pwp1prm  48381  flsqrt  48385  sfprmdvdsmersenne  48395  lighneallem2  48398  lighneallem4a  48400  proththdlem  48405  proththd  48406  nprmdvdsfacm1lem4  48415  nnoALTV  48500  bgoldbtbndlem4  48613  gpgprismgrusgra  48863  gpgedgvtx0  48866  gpgvtxedg0  48868  gpg5nbgrvtx03starlem2  48874  gpg3kgrtriexlem4  48891  gpg3kgrtriexlem6  48893  cznnring  49067  divge1b  49332  divgt1b  49333  nn0eo  49348  regt1loggt0  49356  rege1logbrege0  49378  logblt1b  49384  fllog2  49388  nnolog2flm1  49410  dignn0flhalflem1  49435  rrxlinesc  49555  rrxlinec  49556  eenglngeehlnmlem1  49557  eenglngeehlnmlem2  49558  line2ylem  49571  line2  49572  line2xlem  49573  reseccl  50571  recsccl  50572  amgmwlem  50690  amgmlemALT  50691