Theorem 1red 11182

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11074  1c1 11076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rrecex 11147  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  recgt0  12035  mulgt1  12051  ltrec  12072  nnne0  12227  nn0p1gt0  12478  nn0ge2m1nn  12519  nn0le2is012  12605  suprzcl  12621  ledivge1le  13031  ge2halflem1  13075  qbtwnre  13166  lincmb01cmp  13463  iccf1o  13464  xov1plusxeqvd  13466  zltaddlt1le  13473  fznatpl1  13546  elfz1b  13561  elfzo0subge1  13673  fzonn0p1p1  13712  elfznelfzo  13740  elfznelfzob  13741  fladdz  13794  2tnp1ge0ge0  13798  flhalf  13799  ltdifltdiv  13803  fldiv4lem1div2uz2  13805  mulp1mod1  13883  m1modge3gt1  13890  modltm1p1mod  13895  addmodlteq  13918  ltexp2a  14138  expcan  14141  ltexp2  14142  leexp2  14143  leexp2a  14144  leexp2r  14146  nnlesq  14177  bernneq3  14203  expnbnd  14204  expnlbnd2  14206  expnngt1  14213  fzsdom2  14400  wrdlenge2n0  14524  swrd2lsw  14925  2swrd2eqwrdeq  14926  01sqrexlem7  15221  rddif  15314  reccn2  15570  rlimo1  15590  o1fsum  15786  abscvgcvg  15792  climcndslem1  15822  flo1  15827  harmonic  15832  geomulcvg  15849  fprodrecl  15926  fprodreclf  15932  fprodle  15969  bpoly4  16032  efcllem  16050  efgt1  16091  tanhlt1  16135  sinltx  16164  eirrlem  16179  p1modz1  16236  mod2eq1n2dvds  16324  oddge22np1  16326  ltoddhalfle  16338  nn0o1gt2  16358  nno  16359  nn0oddm1d2  16362  nnoddm1d2  16363  bitsfzolem  16411  bitsfzo  16412  bitsmod  16413  bitscmp  16415  bitsinv1lem  16418  smuval2  16459  coprmgcdb  16626  prmind2  16662  dvdsnprmd  16667  2mulprm  16670  isprm5  16684  isprm7  16685  divdenle  16726  zsqrtelqelz  16735  fermltl  16761  odzdvds  16773  modprm0  16783  iserodd  16813  difsqpwdvds  16865  pcfaclem  16876  prmreclem1  16894  4sqlem11  16933  4sqlem12  16934  ramub1lem1  17004  prmgaplem8  17036  2expltfac  17070  pgpfaclem2  20021  znidomb  21478  psdmvr  22063  chfacfisf  22748  chfacfisfcpmat  22749  chfacfscmulgsum  22754  chfacfpmmulgsum  22758  nrginvrcnlem  24586  nmoid  24637  xrsmopn  24708  metnrmlem1a  24754  iihalf2cn  24836  iccpnfhmeo  24850  lebnumii  24872  htpycc  24886  pcohtpylem  24926  pcoass  24931  pcorevlem  24933  nmhmcn  25027  cncmet  25229  ovoliunlem1  25410  dyadmaxlem  25505  vitalilem2  25517  mbfi1fseqlem6  25628  itg2mulc  25655  itg2monolem1  25658  itg2monolem3  25660  dveflem  25890  mvth  25904  dvlipcn  25906  lhop1lem  25925  dvfsumlem1  25939  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem3  25942  dvfsumlem4  25943  dvfsum2  25948  fta1glem2  26081  plyeq0lem  26122  fta1lem  26222  vieta1lem2  26226  aalioulem3  26249  aalioulem4  26250  radcnvlem1  26329  radcnvlem2  26330  dvradcnv  26337  abelthlem2  26349  abelthlem5  26352  abelthlem7  26355  abelth2  26359  cos02pilt1  26442  cosne0  26445  rplogcl  26520  logdivlti  26536  logno1  26552  dvlog2lem  26568  advlog  26570  logtayllem  26575  cxplt  26610  cxple  26611  cxpaddlelem  26668  cxpaddle  26669  rtprmirr  26677  relogbf  26708  logbgt0b  26710  isosctrlem1  26735  isosctrlem2  26736  chordthmlem4  26752  heron  26755  atanlogaddlem  26830  bndatandm  26846  leibpi  26859  log2tlbnd  26862  birthdaylem3  26870  rlimcnp  26882  rlimcnp2  26883  efrlim  26886  efrlimOLD  26887  cxp2limlem  26893  cxp2lim  26894  divsqrtsumo1  26901  jensenlem2  26905  logdiflbnd  26912  fsumharmonic  26929  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamgulmlem4  26949  lgamgulmlem5  26950  lgamgulmlem6  26951  lgamcvg2  26972  regamcl  26978  wilthlem2  26986  ftalem2  26991  basellem9  27006  vma1  27083  ppieq0  27093  mumullem2  27097  fsumfldivdiaglem  27106  chpeq0  27126  chtub  27130  chpval2  27136  chpchtsum  27137  chpub  27138  logfacrlim  27142  logexprlim  27143  mersenne  27145  perfectlem2  27148  dchrelbas4  27161  bcmono  27195  bposlem1  27202  bposlem2  27203  zabsle1  27214  lgslem3  27217  lgsmod  27241  lgsdir2lem4  27246  lgsdirprm  27249  gausslemma2dlem1a  27283  gausslemma2d  27292  lgsquadlem2  27299  2sqlem8  27344  chebbnd1lem1  27387  chebbnd1lem2  27388  chtppilimlem1  27391  chebbnd2  27395  chto1lb  27396  chpchtlim  27397  chpo1ubb  27399  vmadivsum  27400  rplogsumlem1  27402  rpvmasumlem  27405  dchrisumlem3  27409  dchrmusumlema  27411  dchrmusum2  27412  dchrvmasumlem2  27416  dchrvmasumlem3  27417  dchrvmasumiflem1  27419  dchrvmasumiflem2  27420  dchrisum0flblem1  27426  dchrisum0flblem2  27427  dchrisum0fno1  27429  dchrisum0re  27431  dchrisum0lema  27432  dchrisum0lem1b  27433  dchrisum0lem2a  27435  dchrisum0lem2  27436  dchrisum0lem3  27437  rplogsum  27445  dirith2  27446  mudivsum  27448  mulogsumlem  27449  mulogsum  27450  mulog2sumlem1  27452  mulog2sumlem2  27453  vmalogdivsum2  27456  vmalogdivsum  27457  2vmadivsumlem  27458  log2sumbnd  27462  selberglem2  27464  selberg2lem  27468  chpdifbnd  27473  selberg3lem1  27475  selberg3  27477  selberg4lem1  27478  selberg4  27479  pntrmax  27482  pntrsumo1  27483  pntrsumbnd  27484  selberg3r  27487  selberg4r  27488  selberg34r  27489  pntrlog2bndlem1  27495  pntrlog2bndlem2  27496  pntrlog2bndlem3  27497  pntrlog2bndlem4  27498  pntrlog2bndlem5  27499  pntrlog2bndlem6  27501  pntrlog2bnd  27502  pntpbnd1a  27503  pntpbnd1  27504  pntibndlem2a  27508  pntibndlem2  27509  pntibnd  27511  pntlemc  27513  pntlemg  27516  pntlemr  27520  pntlemk  27524  pnt  27532  qabvle  27543  ostth2lem3  27553  ostth2  27555  trgcgrg  28449  tgcgr4  28465  ttgcontlem1  28819  axpaschlem  28874  axlowdimlem16  28891  axcontlem2  28899  axcontlem7  28904  nbusgrvtxm1  29313  upgrewlkle2  29541  pthdlem1  29703  crctcshwlkn0lem3  29749  crctcshwlkn0lem5  29751  wwlksm1edg  29818  wwlksnextproplem2  29847  clwlkclwwlklem2fv1  29931  clwlkclwwlklem2fv2  29932  clwlkclwwlklem2  29936  clwlkclwwlk2  29939  clwwisshclwwslem  29950  clwwlkf1  29985  clwwlkext2edg  29992  clwlknf1oclwwlknlem1  30017  clwwlknonex2lem2  30044  numclwwlk7  30327  frgrreggt1  30329  frgrogt3nreg  30333  smcnlem  30633  nmoub3i  30709  blocnilem  30740  ubthlem2  30807  minvecolem4  30816  htthlem  30853  nmcexi  31962  nmopcoi  32031  stadd3i  32184  cdj1i  32369  nnmulge  32669  receqid  32675  nndiffz1  32716  fzsplit3  32723  nexple  32776  indf1o  32794  wrdt2ind  32882  pmtrto1cl  33063  fzto1st1  33066  fzto1st  33067  psgnfzto1st  33069  cycpmco2lem6  33095  cycpmco2lem7  33096  cycpmrn  33107  qsidomlem1  33430  krull  33457  ply1degltel  33567  ply1degltlss  33569  constrnegcl  33760  constrdircl  33762  iconstr  33763  constrrecl  33766  constrmulcl  33768  constrreinvcl  33769  constrresqrtcl  33774  cos9thpiminplylem1  33779  cos9thpiminply  33785  cos9thpinconstrlem1  33786  1smat1  33801  submateqlem1  33804  madjusmdetlem2  33825  unitdivcld  33898  sqsscirc1  33905  esumdivc  34080  dya2ub  34268  dya2iocress  34272  dya2iocbrsiga  34273  dya2icobrsiga  34274  dya2icoseg  34275  dya2iocucvr  34282  sxbrsigalem2  34284  fibp1  34399  probmeasb  34428  dstrvprob  34470  dstfrvunirn  34473  ballotlemfc0  34491  ballotlemfcc  34492  ballotlemsgt1  34509  ballotlemsel1i  34511  ballotlemfrcn0  34528  signsply0  34549  itgexpif  34604  reprlt  34617  chtvalz  34627  breprexplemc  34630  breprexp  34631  circlemeth  34638  tgoldbachgnn  34657  acycgr1v  35143  subfaclim  35182  cvmliftlem2  35280  cvmliftlem13  35290  snmlff  35323  bccolsum  35733  faclim  35740  nn0prpwlem  36317  dnibndlem10  36482  dnibndlem12  36484  knoppcnlem4  36491  unblimceq0  36502  knoppndvlem1  36507  knoppndvlem2  36508  knoppndvlem3  36509  knoppndvlem7  36513  knoppndvlem11  36517  knoppndvlem12  36518  knoppndvlem14  36520  knoppndvlem15  36521  knoppndvlem17  36523  knoppndvlem18  36524  knoppndvlem20  36526  irrdiff  37321  poimirlem6  37627  poimirlem7  37628  poimirlem15  37636  poimirlem19  37640  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimirlem32  37653  broucube  37655  itg2addnclem2  37673  itg2addnclem3  37674  areacirclem1  37709  areacirclem4  37712  incsequz  37749  totbndbnd  37790  bfplem2  37824  resdvopclptsd  42023  lcmineqlem2  42025  lcmineqlem3  42026  lcmineqlem10  42033  lcmineqlem12  42035  lcmineqlem15  42038  lcmineqlem18  42041  lcmineqlem19  42042  lcmineqlem20  42043  lcmineqlem22  42045  lcmineqlem23  42046  3lexlogpow5ineq2  42050  3lexlogpow5ineq4  42051  3lexlogpow5ineq3  42052  3lexlogpow2ineq1  42053  3lexlogpow2ineq2  42054  3lexlogpow5ineq5  42055  aks4d1lem1  42057  dvrelog2  42059  dvrelog3  42060  dvrelog2b  42061  dvrelogpow2b  42063  aks4d1p1p3  42064  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p6  42068  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  aks4d1p2  42072  aks4d1p3  42073  aks4d1p5  42075  aks4d1p6  42076  aks4d1p7d1  42077  aks4d1p7  42078  aks4d1p8d2  42080  aks4d1p8d3  42081  aks4d1p8  42082  aks4d1p9  42083  posbezout  42095  primrootlekpowne0  42100  primrootspoweq0  42101  aks6d1c1  42111  aks6d1c2p2  42114  hashscontpow1  42116  aks6d1c3  42118  aks6d1c2lem4  42122  aks6d1c2  42125  2np3bcnp1  42139  2ap1caineq  42140  sticksstones6  42146  sticksstones7  42147  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  sticksstones22  42163  aks6d1c6lem3  42167  aks6d1c6lem4  42168  bcled  42173  bcle2d  42174  aks6d1c7lem1  42175  aks6d1c7lem2  42176  unitscyglem2  42191  unitscyglem4  42193  unitscyglem5  42194  aks5lem8  42196  sn-1ne2  42260  redvmptabs  42355  sn-00idlem2  42394  sn-0ne2  42401  rei4  42419  sn-rereccld  42443  rerecid  42444  sn-0tie0  42446  sn-nnne0  42455  mulgt0b1d  42467  sn-ltmulgt11d  42469  sn-0lt1  42470  sn-mulgt1d  42474  fimgmcyc  42529  flt4lem7  42654  fltnlta  42658  3cubeslem1  42679  3cubeslem3r  42682  3cubeslem4  42684  lzenom  42765  irrapxlem1  42817  irrapxlem2  42818  irrapxlem4  42820  irrapxlem5  42821  pellexlem2  42825  pell1qrge1  42865  pell1qr1  42866  elpell1qr2  42867  pell14qrgapw  42871  pellfundgt1  42878  pellfundglb  42880  pellfundex  42881  pellfundrp  42883  pellfundne1  42884  rmspecsqrtnq  42901  rmspecnonsq  42902  rmspecfund  42904  rmspecpos  42912  monotoddzzfi  42938  rmygeid  42960  areaquad  43212  imo72b2lem0  44161  imo72b2lem1  44165  imo72b2  44168  cvgdvgrat  44309  radcnvrat  44310  hashnzfzclim  44318  lhe4.4ex1a  44325  binomcxplemnn0  44345  binomcxplemdvbinom  44349  binomcxplemnotnn0  44352  oddfl  45283  abscosbd  45284  zltlesub  45290  abssinbd  45300  monoords  45302  fzisoeu  45305  fzdifsuc2  45315  suplesup  45342  xralrple2  45357  infxr  45370  infleinflem2  45374  reclt0d  45390  xrralrecnnge  45393  sqrlearg  45558  iooiinioc  45561  fmul01  45585  fmul01lt1lem1  45589  fmul01lt1lem2  45590  climsuselem1  45612  sumnnodd  45635  0ellimcdiv  45654  dvmptidg  45922  dvcosax  45931  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvxpaek  45945  dvnmul  45948  iblspltprt  45978  itgspltprt  45984  stoweidlem5  46010  stoweidlem7  46012  stoweidlem10  46015  stoweidlem11  46016  stoweidlem12  46017  stoweidlem13  46018  stoweidlem14  46019  stoweidlem16  46021  stoweidlem18  46023  stoweidlem20  46025  stoweidlem24  46029  stoweidlem25  46030  stoweidlem34  46039  stoweidlem36  46041  stoweidlem38  46043  stoweidlem40  46045  stoweidlem41  46046  stoweidlem42  46047  stoweidlem45  46050  stoweidlem51  46056  stoweidlem60  46065  wallispilem3  46072  wallispilem4  46073  wallispilem5  46074  wallispi  46075  wallispi2lem1  46076  wallispi2lem2  46077  wallispi2  46078  stirlinglem1  46079  stirlinglem3  46081  stirlinglem5  46083  stirlinglem6  46084  stirlinglem7  46085  stirlinglem8  46086  stirlinglem10  46088  stirlinglem11  46089  stirlinglem12  46090  stirlinglem13  46091  stirlinglem15  46093  dirker2re  46097  dirkerval2  46099  dirkerre  46100  dirkertrigeqlem1  46103  dirkertrigeqlem3  46105  dirkeritg  46107  dirkercncflem1  46108  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem5  46117  fourierdlem6  46118  fourierdlem11  46123  fourierdlem15  46127  fourierdlem19  46131  fourierdlem20  46132  fourierdlem24  46136  fourierdlem26  46138  fourierdlem28  46140  fourierdlem30  46142  fourierdlem39  46151  fourierdlem41  46153  fourierdlem43  46155  fourierdlem47  46158  fourierdlem48  46159  fourierdlem56  46167  fourierdlem60  46171  fourierdlem61  46172  fourierdlem62  46173  fourierdlem64  46175  fourierdlem65  46176  fourierdlem66  46177  fourierdlem68  46179  fourierdlem73  46184  fourierdlem78  46189  fourierdlem79  46190  fourierdlem87  46198  fourierdlem103  46214  fourierdlem104  46215  sqwvfoura  46233  fouriersw  46236  etransclem4  46243  etransclem23  46262  etransclem24  46263  etransclem31  46270  etransclem32  46271  etransclem35  46274  etransclem41  46280  etransclem46  46285  etransclem48  46287  etransc  46288  ioorrnopnxrlem  46311  nnfoctbdjlem  46460  iundjiun  46465  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  ovnhoilem1  46606  vonioolem2  46686  vonicclem2  46689  pimrecltneg  46729  smfrec  46794  smfmullem1  46796  smfmullem2  46797  smfdiv  46802  sigaradd  46871  ormkglobd  46880  p1lep2  47305  zm1nn  47307  ceilhalfgt1  47334  2tceilhalfelfzo1  47337  ceilbi  47338  rehalfge1  47340  ceilhalfnn  47341  addmodne  47349  m1mod0mod1  47359  m1modmmod  47363  difmodm1lt  47364  modmknepk  47367  modp2nep1  47372  modm1nem2  47374  iccpartiltu  47427  iccpartlt  47429  iccpartgt  47432  fmtnoge3  47535  fmtnodvds  47549  fmtnoprmfac2lem1  47571  2pwp1prm  47594  flsqrt  47598  sfprmdvdsmersenne  47608  lighneallem2  47611  lighneallem4a  47613  proththdlem  47618  proththd  47619  nnoALTV  47700  bgoldbtbndlem4  47813  gpgprismgrusgra  48053  gpgedgvtx0  48056  gpgvtxedg0  48058  gpg5nbgrvtx03starlem2  48064  gpg3kgrtriexlem4  48081  gpg3kgrtriexlem6  48083  cznnring  48254  divge1b  48505  divgt1b  48506  nn0eo  48521  regt1loggt0  48529  rege1logbrege0  48551  logblt1b  48557  fllog2  48561  nnolog2flm1  48583  dignn0flhalflem1  48608  rrxlinesc  48728  rrxlinec  48729  eenglngeehlnmlem1  48730  eenglngeehlnmlem2  48731  line2ylem  48744  line2  48745  line2xlem  48746  reseccl  49746  recsccl  49747  amgmwlem  49795  amgmlemALT  49796