Theorem 1red 11262

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 11154  1c1 11156

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434

This theorem is referenced by:  recgt0  12113  mulgt1  12129  ltrec  12150  nnne0  12300  nn0p1gt0  12555  nn0ge2m1nn  12596  nn0le2is012  12682  suprzcl  12698  ledivge1le  13106  ge2halflem1  13150  qbtwnre  13241  lincmb01cmp  13535  iccf1o  13536  xov1plusxeqvd  13538  zltaddlt1le  13545  fznatpl1  13618  elfz1b  13633  elfzo0subge1  13745  fzonn0p1p1  13783  elfznelfzo  13811  elfznelfzob  13812  fladdz  13865  2tnp1ge0ge0  13869  flhalf  13870  ltdifltdiv  13874  fldiv4lem1div2uz2  13876  mulp1mod1  13952  m1modge3gt1  13959  modltm1p1mod  13964  addmodlteq  13987  ltexp2a  14206  expcan  14209  ltexp2  14210  leexp2  14211  leexp2a  14212  leexp2r  14214  nnlesq  14244  bernneq3  14270  expnbnd  14271  expnlbnd2  14273  expnngt1  14280  fzsdom2  14467  wrdlenge2n0  14590  swrd2lsw  14991  2swrd2eqwrdeq  14992  01sqrexlem7  15287  rddif  15379  reccn2  15633  rlimo1  15653  o1fsum  15849  abscvgcvg  15855  climcndslem1  15885  flo1  15890  harmonic  15895  geomulcvg  15912  fprodrecl  15989  fprodreclf  15995  fprodle  16032  bpoly4  16095  efcllem  16113  efgt1  16152  tanhlt1  16196  sinltx  16225  eirrlem  16240  p1modz1  16297  mod2eq1n2dvds  16384  oddge22np1  16386  ltoddhalfle  16398  nn0o1gt2  16418  nno  16419  nn0oddm1d2  16422  nnoddm1d2  16423  bitsfzolem  16471  bitsfzo  16472  bitsmod  16473  bitscmp  16475  bitsinv1lem  16478  smuval2  16519  coprmgcdb  16686  prmind2  16722  dvdsnprmd  16727  2mulprm  16730  isprm5  16744  isprm7  16745  divdenle  16786  zsqrtelqelz  16795  fermltl  16821  odzdvds  16833  modprm0  16843  iserodd  16873  difsqpwdvds  16925  pcfaclem  16936  prmreclem1  16954  4sqlem11  16993  4sqlem12  16994  ramub1lem1  17064  prmgaplem8  17096  2expltfac  17130  pgpfaclem2  20102  znidomb  21580  psdmvr  22173  chfacfisf  22860  chfacfisfcpmat  22861  chfacfscmulgsum  22866  chfacfpmmulgsum  22870  nrginvrcnlem  24712  nmoid  24763  xrsmopn  24834  metnrmlem1a  24880  iihalf2cn  24962  iccpnfhmeo  24976  lebnumii  24998  htpycc  25012  pcohtpylem  25052  pcoass  25057  pcorevlem  25059  nmhmcn  25153  cncmet  25356  ovoliunlem1  25537  dyadmaxlem  25632  vitalilem2  25644  mbfi1fseqlem6  25755  itg2mulc  25782  itg2monolem1  25785  itg2monolem3  25787  dveflem  26017  mvth  26031  dvlipcn  26033  lhop1lem  26052  dvfsumlem1  26066  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem3  26069  dvfsumlem4  26070  dvfsum2  26075  fta1glem2  26208  plyeq0lem  26249  fta1lem  26349  vieta1lem2  26353  aalioulem3  26376  aalioulem4  26377  radcnvlem1  26456  radcnvlem2  26457  dvradcnv  26464  abelthlem2  26476  abelthlem5  26479  abelthlem7  26482  abelth2  26486  cos02pilt1  26568  cosne0  26571  rplogcl  26646  logdivlti  26662  logno1  26678  dvlog2lem  26694  advlog  26696  logtayllem  26701  cxplt  26736  cxple  26737  cxpaddlelem  26794  cxpaddle  26795  rtprmirr  26803  relogbf  26834  logbgt0b  26836  isosctrlem1  26861  isosctrlem2  26862  chordthmlem4  26878  heron  26881  atanlogaddlem  26956  bndatandm  26972  leibpi  26985  log2tlbnd  26988  birthdaylem3  26996  rlimcnp  27008  rlimcnp2  27009  efrlim  27012  efrlimOLD  27013  cxp2limlem  27019  cxp2lim  27020  divsqrtsumo1  27027  jensenlem2  27031  logdiflbnd  27038  fsumharmonic  27055  lgamgulmlem2  27073  lgamgulmlem3  27074  lgamgulmlem4  27075  lgamgulmlem5  27076  lgamgulmlem6  27077  lgamcvg2  27098  regamcl  27104  wilthlem2  27112  ftalem2  27117  basellem9  27132  vma1  27209  ppieq0  27219  mumullem2  27223  fsumfldivdiaglem  27232  chpeq0  27252  chtub  27256  chpval2  27262  chpchtsum  27263  chpub  27264  logfacrlim  27268  logexprlim  27269  mersenne  27271  perfectlem2  27274  dchrelbas4  27287  bcmono  27321  bposlem1  27328  bposlem2  27329  zabsle1  27340  lgslem3  27343  lgsmod  27367  lgsdir2lem4  27372  lgsdirprm  27375  gausslemma2dlem1a  27409  gausslemma2d  27418  lgsquadlem2  27425  2sqlem8  27470  chebbnd1lem1  27513  chebbnd1lem2  27514  chtppilimlem1  27517  chebbnd2  27521  chto1lb  27522  chpchtlim  27523  chpo1ubb  27525  vmadivsum  27526  rplogsumlem1  27528  rpvmasumlem  27531  dchrisumlem3  27535  dchrmusumlema  27537  dchrmusum2  27538  dchrvmasumlem2  27542  dchrvmasumlem3  27543  dchrvmasumiflem1  27545  dchrvmasumiflem2  27546  dchrisum0flblem1  27552  dchrisum0flblem2  27553  dchrisum0fno1  27555  dchrisum0re  27557  dchrisum0lema  27558  dchrisum0lem1b  27559  dchrisum0lem2a  27561  dchrisum0lem2  27562  dchrisum0lem3  27563  rplogsum  27571  dirith2  27572  mudivsum  27574  mulogsumlem  27575  mulogsum  27576  mulog2sumlem1  27578  mulog2sumlem2  27579  vmalogdivsum2  27582  vmalogdivsum  27583  2vmadivsumlem  27584  log2sumbnd  27588  selberglem2  27590  selberg2lem  27594  chpdifbnd  27599  selberg3lem1  27601  selberg3  27603  selberg4lem1  27604  selberg4  27605  pntrmax  27608  pntrsumo1  27609  pntrsumbnd  27610  selberg3r  27613  selberg4r  27614  selberg34r  27615  pntrlog2bndlem1  27621  pntrlog2bndlem2  27622  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntrlog2bndlem6  27627  pntrlog2bnd  27628  pntpbnd1a  27629  pntpbnd1  27630  pntibndlem2a  27634  pntibndlem2  27635  pntibnd  27637  pntlemc  27639  pntlemg  27642  pntlemr  27646  pntlemk  27650  pnt  27658  qabvle  27669  ostth2lem3  27679  ostth2  27681  trgcgrg  28523  tgcgr4  28539  ttgcontlem1  28899  axpaschlem  28955  axlowdimlem16  28972  axcontlem2  28980  axcontlem7  28985  nbusgrvtxm1  29396  upgrewlkle2  29624  pthdlem1  29786  crctcshwlkn0lem3  29832  crctcshwlkn0lem5  29834  wwlksm1edg  29901  wwlksnextproplem2  29930  clwlkclwwlklem2fv1  30014  clwlkclwwlklem2fv2  30015  clwlkclwwlklem2  30019  clwlkclwwlk2  30022  clwwisshclwwslem  30033  clwwlkf1  30068  clwwlkext2edg  30075  clwlknf1oclwwlknlem1  30100  clwwlknonex2lem2  30127  numclwwlk7  30410  frgrreggt1  30412  frgrogt3nreg  30416  smcnlem  30716  nmoub3i  30792  blocnilem  30823  ubthlem2  30890  minvecolem4  30899  htthlem  30936  nmcexi  32045  nmopcoi  32114  stadd3i  32267  cdj1i  32452  nnmulge  32749  nndiffz1  32788  fzsplit3  32795  nexple  32833  indf1o  32849  wrdt2ind  32938  pmtrto1cl  33119  fzto1st1  33122  fzto1st  33123  psgnfzto1st  33125  cycpmco2lem6  33151  cycpmco2lem7  33152  cycpmrn  33163  qsidomlem1  33480  krull  33507  ply1degltel  33615  ply1degltlss  33617  1smat1  33803  submateqlem1  33806  madjusmdetlem2  33827  unitdivcld  33900  sqsscirc1  33907  esumdivc  34084  dya2ub  34272  dya2iocress  34276  dya2iocbrsiga  34277  dya2icobrsiga  34278  dya2icoseg  34279  dya2iocucvr  34286  sxbrsigalem2  34288  fibp1  34403  probmeasb  34432  dstrvprob  34474  dstfrvunirn  34477  ballotlemfc0  34495  ballotlemfcc  34496  ballotlemsgt1  34513  ballotlemsel1i  34515  ballotlemfrcn0  34532  signsply0  34566  itgexpif  34621  reprlt  34634  chtvalz  34644  breprexplemc  34647  breprexp  34648  circlemeth  34655  tgoldbachgnn  34674  acycgr1v  35154  subfaclim  35193  cvmliftlem2  35291  cvmliftlem13  35301  snmlff  35334  bccolsum  35739  faclim  35746  nn0prpwlem  36323  dnibndlem10  36488  dnibndlem12  36490  knoppcnlem4  36497  unblimceq0  36508  knoppndvlem1  36513  knoppndvlem2  36514  knoppndvlem3  36515  knoppndvlem7  36519  knoppndvlem11  36523  knoppndvlem12  36524  knoppndvlem14  36526  knoppndvlem15  36527  knoppndvlem17  36529  knoppndvlem18  36530  knoppndvlem20  36532  irrdiff  37327  poimirlem6  37633  poimirlem7  37634  poimirlem15  37642  poimirlem19  37646  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimirlem32  37659  broucube  37661  itg2addnclem2  37679  itg2addnclem3  37680  areacirclem1  37715  areacirclem4  37718  incsequz  37755  totbndbnd  37796  bfplem2  37830  resdvopclptsd  42029  lcmineqlem2  42031  lcmineqlem3  42032  lcmineqlem10  42039  lcmineqlem12  42041  lcmineqlem15  42044  lcmineqlem18  42047  lcmineqlem19  42048  lcmineqlem20  42049  lcmineqlem22  42051  lcmineqlem23  42052  3lexlogpow5ineq2  42056  3lexlogpow5ineq4  42057  3lexlogpow5ineq3  42058  3lexlogpow2ineq1  42059  3lexlogpow2ineq2  42060  3lexlogpow5ineq5  42061  aks4d1lem1  42063  dvrelog2  42065  dvrelog3  42066  dvrelog2b  42067  dvrelogpow2b  42069  aks4d1p1p3  42070  aks4d1p1p2  42071  aks4d1p1p4  42072  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1p5  42076  aks4d1p1  42077  aks4d1p2  42078  aks4d1p3  42079  aks4d1p5  42081  aks4d1p6  42082  aks4d1p7d1  42083  aks4d1p7  42084  aks4d1p8d2  42086  aks4d1p8d3  42087  aks4d1p8  42088  aks4d1p9  42089  posbezout  42101  primrootlekpowne0  42106  primrootspoweq0  42107  aks6d1c1  42117  aks6d1c2p2  42120  hashscontpow1  42122  aks6d1c3  42124  aks6d1c2lem4  42128  aks6d1c2  42131  2np3bcnp1  42145  2ap1caineq  42146  sticksstones6  42152  sticksstones7  42153  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  sticksstones22  42169  aks6d1c6lem3  42173  aks6d1c6lem4  42174  bcled  42179  bcle2d  42180  aks6d1c7lem1  42181  aks6d1c7lem2  42182  unitscyglem2  42197  unitscyglem4  42199  unitscyglem5  42200  aks5lem8  42202  metakunt1  42206  metakunt2  42207  metakunt7  42212  metakunt15  42220  metakunt16  42221  metakunt24  42229  metakunt28  42233  metakunt29  42234  2xp3dxp2ge1d  42242  factwoffsmonot  42243  sn-1ne2  42300  redvmptabs  42390  sn-00idlem2  42429  sn-0ne2  42436  rei4  42453  sn-0tie0  42469  sn-nnne0  42478  mulgt0b2d  42490  sn-ltmulgt11d  42492  sn-0lt1  42493  sn-mulgt1d  42495  fimgmcyc  42544  flt4lem7  42669  fltnlta  42673  3cubeslem1  42695  3cubeslem3r  42698  3cubeslem4  42700  lzenom  42781  irrapxlem1  42833  irrapxlem2  42834  irrapxlem4  42836  irrapxlem5  42837  pellexlem2  42841  pell1qrge1  42881  pell1qr1  42882  elpell1qr2  42883  pell14qrgapw  42887  pellfundgt1  42894  pellfundglb  42896  pellfundex  42897  pellfundrp  42899  pellfundne1  42900  rmspecsqrtnq  42917  rmspecnonsq  42918  rmspecfund  42920  rmspecpos  42928  monotoddzzfi  42954  rmygeid  42976  areaquad  43228  imo72b2lem0  44178  imo72b2lem1  44182  imo72b2  44185  cvgdvgrat  44332  radcnvrat  44333  hashnzfzclim  44341  lhe4.4ex1a  44348  binomcxplemnn0  44368  binomcxplemdvbinom  44372  binomcxplemnotnn0  44375  oddfl  45289  abscosbd  45290  zltlesub  45297  abssinbd  45307  monoords  45309  fzisoeu  45312  fzdifsuc2  45322  suplesup  45350  xralrple2  45365  infxr  45378  infleinflem2  45382  reclt0d  45398  xrralrecnnge  45401  sqrlearg  45566  iooiinioc  45569  fmul01  45595  fmul01lt1lem1  45599  fmul01lt1lem2  45600  climsuselem1  45622  sumnnodd  45645  0ellimcdiv  45664  dvmptidg  45932  dvcosax  45941  ioodvbdlimc1lem1  45946  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvxpaek  45955  dvnmul  45958  iblspltprt  45988  itgspltprt  45994  stoweidlem5  46020  stoweidlem7  46022  stoweidlem10  46025  stoweidlem11  46026  stoweidlem12  46027  stoweidlem13  46028  stoweidlem14  46029  stoweidlem16  46031  stoweidlem18  46033  stoweidlem20  46035  stoweidlem24  46039  stoweidlem25  46040  stoweidlem34  46049  stoweidlem36  46051  stoweidlem38  46053  stoweidlem40  46055  stoweidlem41  46056  stoweidlem42  46057  stoweidlem45  46060  stoweidlem51  46066  stoweidlem60  46075  wallispilem3  46082  wallispilem4  46083  wallispilem5  46084  wallispi  46085  wallispi2lem1  46086  wallispi2lem2  46087  wallispi2  46088  stirlinglem1  46089  stirlinglem3  46091  stirlinglem5  46093  stirlinglem6  46094  stirlinglem7  46095  stirlinglem8  46096  stirlinglem10  46098  stirlinglem11  46099  stirlinglem12  46100  stirlinglem13  46101  stirlinglem15  46103  dirker2re  46107  dirkerval2  46109  dirkerre  46110  dirkertrigeqlem1  46113  dirkertrigeqlem3  46115  dirkeritg  46117  dirkercncflem1  46118  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem5  46127  fourierdlem6  46128  fourierdlem11  46133  fourierdlem15  46137  fourierdlem19  46141  fourierdlem20  46142  fourierdlem24  46146  fourierdlem26  46148  fourierdlem28  46150  fourierdlem30  46152  fourierdlem39  46161  fourierdlem41  46163  fourierdlem43  46165  fourierdlem47  46168  fourierdlem48  46169  fourierdlem56  46177  fourierdlem60  46181  fourierdlem61  46182  fourierdlem62  46183  fourierdlem64  46185  fourierdlem65  46186  fourierdlem66  46187  fourierdlem68  46189  fourierdlem73  46194  fourierdlem78  46199  fourierdlem79  46200  fourierdlem87  46208  fourierdlem103  46224  fourierdlem104  46225  sqwvfoura  46243  fouriersw  46246  etransclem4  46253  etransclem23  46272  etransclem24  46273  etransclem31  46280  etransclem32  46281  etransclem35  46284  etransclem41  46290  etransclem46  46295  etransclem48  46297  etransc  46298  ioorrnopnxrlem  46321  nnfoctbdjlem  46470  iundjiun  46475  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  ovnhoilem1  46616  vonioolem2  46696  vonicclem2  46699  pimrecltneg  46739  smfrec  46804  smfmullem1  46806  smfmullem2  46807  smfdiv  46812  sigaradd  46881  ormkglobd  46890  p1lep2  47312  zm1nn  47314  addmodne  47346  m1mod0mod1  47356  iccpartiltu  47409  iccpartlt  47411  iccpartgt  47414  fmtnoge3  47517  fmtnodvds  47531  fmtnoprmfac2lem1  47553  2pwp1prm  47576  flsqrt  47580  sfprmdvdsmersenne  47590  lighneallem2  47593  lighneallem4a  47595  proththdlem  47600  proththd  47601  nnoALTV  47682  bgoldbtbndlem4  47795  2tceilhalfelfzo1  48018  gpgedgvtx0  48019  gpgvtxedg0  48021  gpg3nbgrvtxlem  48023  gpg5nbgrvtx03starlem2  48025  gpg3kgrtriexlem4  48042  gpg3kgrtriexlem6  48044  cznnring  48178  divge1b  48429  divgt1b  48430  m1modmmod  48442  difmodm1lt  48443  nn0eo  48449  regt1loggt0  48457  rege1logbrege0  48479  logblt1b  48485  fllog2  48489  nnolog2flm1  48511  dignn0flhalflem1  48536  rrxlinesc  48656  rrxlinec  48657  eenglngeehlnmlem1  48658  eenglngeehlnmlem2  48659  line2ylem  48672  line2  48673  line2xlem  48674  reseccl  49272  recsccl  49273  amgmwlem  49321  amgmlemALT  49322