Theorem 1red 11336

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℝcr 11226  1c1 11228

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11285  ax-icn 11286  ax-addcl 11287  ax-mulcl 11289  ax-mulrcl 11290  ax-i2m1 11295  ax-1ne0 11296  ax-rrecex 11299  ax-cnre 11300

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446

This theorem is used by:  recgt0  12190  mulgt1  12205  ltrec  12226  nnne0  12399  nn0p1gt0  12662  nn0ge2m1nn  12703  nn0le2is012  12790  suprzcl  12806  ledivge1le  13220  ge2halflem1  13264  qbtwnre  13356  lincmb01cmp  13653  iccf1o  13654  xov1plusxeqvd  13656  zltaddlt1le  13663  nnge2recico01  13665  fznatpl1  13739  elfz1b  13754  elfzo0subge1  13867  fzonn0p1p1  13906  elfznelfzo  13935  elfznelfzob  13936  fladdz  13992  2tnp1ge0ge0  13996  flhalf  13997  ltdifltdiv  14001  mulp1mod1  14081  m1modge3gt1  14088  modltm1p1mod  14093  addmodlteq  14116  ltexp2a  14336  expcan  14339  ltexp2  14340  leexp2  14341  leexp2a  14342  leexp2r  14344  nnlesq  14376  bernneq3  14402  expnbnd  14403  expnlbnd2  14405  expnngt1  14412  fzsdom2  14600  wrdlenge2n0  14724  swrd2lsw  15134  2swrd2eqwrdeq  15135  01sqrexlem7  15444  rddif  15537  reccn2  15793  rlimo1  15813  o1fsum  16009  abscvgcvg  16015  climcndslem1  16047  flo1  16052  harmonic  16057  geomulcvg  16074  fprodrecl  16149  fprodreclf  16155  fprodle  16192  bpoly4  16254  efcllem  16272  efgt1  16313  tanhlt1  16357  sinltx  16386  eirrlem  16401  p1modz1  16458  mod2eq1n2dvds  16546  oddge22np1  16548  ltoddhalfle  16560  nn0o1gt2  16580  nno  16581  nn0oddm1d2  16584  nnoddm1d2  16585  bitsfzolem  16633  bitsfzo  16634  bitsmod  16635  bitscmp  16637  bitsinv1lem  16640  smuval2  16681  coprmgcdb  16853  prmind2  16889  dvdsnprmd  16894  2mulprm  16897  isprm5  16912  isprm7  16913  divdenle  16954  zsqrtelqelz  16963  fermltl  16990  odzdvds  17002  modprm0  17012  iserodd  17042  difsqpwdvds  17094  pcfaclem  17105  prmreclem1  17123  4sqlem11  17162  4sqlem12  17163  ramub1lem1  17233  prmgaplem8  17265  2expltfac  17299  chnccat  18829  pgpfaclem2  20328  qsidomlem1  21666  znidomb  21897  psdmvr  22520  chfacfisf  23202  chfacfisfcpmat  23203  chfacfscmulgsum  23208  chfacfpmmulgsum  23212  nrginvrcnlem  25040  nmoid  25091  xrsmopn  25162  metnrmlem1a  25208  iihalf2cn  25285  iccpnfhmeo  25296  lebnumii  25317  htpycc  25331  pcohtpylem  25370  pcoass  25375  pcorevlem  25377  nmhmcn  25471  cncmet  25673  ovoliunlem1  25853  dyadmaxlem  25948  vitalilem2  25960  mbfi1fseqlem6  26071  itg2mulc  26098  itg2monolem1  26101  itg2monolem3  26103  dveflem  26329  mvth  26342  dvlipcn  26344  lhop1lem  26363  dvfsumlem1  26376  dvfsumlem2  26377  dvfsumlem3  26378  dvfsumlem4  26379  dvfsum2  26384  fta1glem2  26517  plyeq0lem  26559  fta1lem  26658  vieta1lem2  26664  aalioulem3  26691  aalioulem4  26692  radcnvlem1  26770  radcnvlem2  26771  dvradcnv  26778  abelthlem2  26789  abelthlem5  26792  abelthlem7  26795  abelth2  26799  cos02pilt1  26884  cosne0  26887  rplogcl  26962  logdivlti  26978  logno1  26994  dvlog2lem  27010  advlog  27012  logtayllem  27017  cxplt  27052  cxple  27053  cxpaddlelem  27109  cxpaddle  27110  rtprmirr  27118  relogbf  27149  logbgt0b  27151  isosctrlem1  27176  isosctrlem2  27177  chordthmlem4  27193  heron  27196  atanlogaddlem  27271  bndatandm  27287  leibpi  27300  log2tlbnd  27303  birthdaylem3  27311  rlimcnp  27323  rlimcnp2  27324  efrlim  27327  cxp2limlem  27333  cxp2lim  27334  divsqrtsumo1  27341  jensenlem2  27345  logdiflbnd  27352  fsumharmonic  27369  lgamgulmlem2  27387  lgamgulmlem3  27388  lgamgulmlem4  27389  lgamgulmlem5  27390  lgamgulmlem6  27391  lgamcvg2  27412  regamcl  27418  wilthlem2  27426  ftalem2  27431  basellem9  27446  vma1  27523  ppieq0  27533  mumullem2  27537  fsumfldivdiaglem  27546  ppiub  27561  chpeq0  27565  chtub  27569  chpval2  27575  chpchtsum  27576  chpub  27577  logfacrlim  27581  logexprlim  27582  mersenne  27584  perfectlem2  27587  dchrelbas4  27600  bcmono  27634  bposlem1  27641  bposlem2  27642  zabsle1  27653  lgslem3  27656  lgsmod  27680  lgsdir2lem4  27685  lgsdirprm  27688  gausslemma2dlem1a  27722  gausslemma2d  27731  lgsquadlem2  27738  2sqlem8  27783  chebbnd1lem1  27826  chebbnd1lem2  27827  chtppilimlem1  27830  chebbnd2  27834  chto1lb  27835  chpchtlim  27836  chpo1ubb  27838  vmadivsum  27839  rplogsumlem1  27841  rpvmasumlem  27844  dchrisumlem3  27848  dchrmusumlema  27850  dchrmusum2  27851  dchrvmasumlem2  27855  dchrvmasumlem3  27856  dchrvmasumiflem1  27858  dchrvmasumiflem2  27859  dchrisum0flblem1  27865  dchrisum0flblem2  27866  dchrisum0fno1  27868  dchrisum0re  27870  dchrisum0lema  27871  dchrisum0lem1b  27872  dchrisum0lem2a  27874  dchrisum0lem2  27875  dchrisum0lem3  27876  rplogsum  27884  dirith2  27885  mudivsum  27887  mulogsumlem  27888  mulogsum  27889  mulog2sumlem1  27891  mulog2sumlem2  27892  vmalogdivsum2  27895  vmalogdivsum  27896  2vmadivsumlem  27897  log2sumbnd  27901  selberglem2  27903  selberg2lem  27907  chpdifbnd  27912  selberg3lem1  27914  selberg3  27916  selberg4lem1  27917  selberg4  27918  pntrmax  27921  pntrsumo1  27922  pntrsumbnd  27923  selberg3r  27926  selberg4r  27927  selberg34r  27928  pntrlog2bndlem1  27934  pntrlog2bndlem2  27935  pntrlog2bndlem3  27936  pntrlog2bndlem4  27937  pntrlog2bndlem5  27938  pntrlog2bndlem6  27940  pntrlog2bnd  27941  pntpbnd1a  27942  pntpbnd1  27943  pntibndlem2a  27947  pntibndlem2  27948  pntibnd  27950  pntlemc  27952  pntlemg  27955  pntlemr  27959  pntlemk  27963  pnt  27971  qabvle  27982  ostth2lem3  27992  ostth2  27994  flt4lem7  28019  trgcgrg  29008  tgcgr4  29024  ttgcontlem1  29492  axpaschlem  29548  axlowdimlem16  29565  axcontlem2  29573  axcontlem7  29578  nbusgrvtxm1  29990  upgrewlkle2  30217  pthdlem1  30382  crctcshwlkn0lem3  30431  crctcshwlkn0lem5  30433  wwlksm1edg  30500  wwlksnextproplem2  30529  clwlkclwwlklem2fv1  30616  clwlkclwwlklem2fv2  30617  clwlkclwwlklem2  30621  clwlkclwwlk2  30624  clwwisshclwwslem  30635  clwwlkf1  30670  clwwlkext2edg  30677  clwlknf1oclwwlknlem1  30702  clwwlknonex2lem2  30729  numclwwlk7  31022  frgrreggt1  31024  frgrogt3nreg  31028  smcnlem  31329  nmoub3i  31405  blocnilem  31436  ubthlem2  31503  minvecolem4  31512  htthlem  31549  nmcexi  32658  nmopcoi  32727  stadd3i  32880  cdj1i  33065  nnmulge  33401  receqid  33406  nndiffz1  33448  fzsplit3  33455  nexple  33494  indf1o  33501  wrdt2ind  33586  pmtrto1cl  33730  fzto1st1  33733  fzto1st  33734  psgnfzto1st  33736  cycpmco2lem6  33762  cycpmco2lem7  33763  cycpmrn  33774  krull  34073  ply1degltel  34196  ply1degltlss  34198  constrnegcl  34465  constrdircl  34467  iconstr  34468  constrrecl  34471  constrmulcl  34473  constrreinvcl  34474  constrresqrtcl  34479  cos9thpiminplylem1  34484  cos9thpiminply  34490  cos9thpinconstrlem1  34491  1smat1  34506  submateqlem1  34509  madjusmdetlem2  34530  unitdivcld  34603  sqsscirc1  34610  esumdivc  34785  dya2ub  34972  dya2iocress  34976  dya2iocbrsiga  34977  dya2icobrsiga  34978  dya2icoseg  34979  dya2iocucvr  34986  sxbrsigalem2  34988  omssubadd  35002  fibp1  35103  probmeasb  35132  dstrvprob  35174  dstfrvunirn  35177  ballotlemfc0  35195  ballotlemfcc  35196  ballotlemsgt1  35213  ballotlemsel1i  35215  ballotlemfrcn0  35232  signsply0  35250  itgexpif  35305  reprlt  35318  chtvalz  35328  breprexplemc  35331  breprexp  35332  circlemeth  35339  tgoldbachgnn  35358  acycgr1v  36071  subfaclim  36120  cvmliftlem2  36218  cvmliftlem13  36228  snmlff  36261  bccolsum  36682  faclim  36689  nn0prpwlem  37288  dnibndlem10  37531  dnibndlem12  37533  knoppcnlem4  37540  unblimceq0  37551  knoppndvlem1  37556  knoppndvlem2  37557  knoppndvlem3  37558  knoppndvlem7  37562  knoppndvlem11  37566  knoppndvlem12  37567  knoppndvlem14  37569  knoppndvlem15  37570  knoppndvlem17  37572  knoppndvlem18  37573  knoppndvlem20  37575  irrdiff  38439  poimirlem6  38736  poimirlem7  38737  poimirlem15  38745  poimirlem19  38749  poimirlem29  38759  poimirlem30  38760  poimirlem31  38761  poimirlem32  38762  broucube  38764  itg2addnclem2  38782  itg2addnclem3  38783  areacirclem1  38818  areacirclem4  38821  incsequz  38874  totbndbnd  38915  bfplem2  38949  resdvopclptsd  43270  lcmineqlem2  43272  lcmineqlem3  43273  lcmineqlem10  43280  lcmineqlem12  43282  lcmineqlem15  43285  lcmineqlem18  43288  lcmineqlem19  43289  lcmineqlem20  43290  lcmineqlem22  43292  lcmineqlem23  43293  3lexlogpow5ineq2  43297  3lexlogpow5ineq4  43298  3lexlogpow5ineq3  43299  3lexlogpow2ineq1  43300  3lexlogpow2ineq2  43301  3lexlogpow5ineq5  43302  aks4d1lem1  43304  dvrelog2  43306  dvrelog3  43307  dvrelog2b  43308  dvrelogpow2b  43310  aks4d1p1p3  43311  aks4d1p1p2  43312  aks4d1p1p4  43313  aks4d1p1p6  43315  aks4d1p1p7  43316  aks4d1p1p5  43317  aks4d1p1  43318  aks4d1p2  43319  aks4d1p3  43320  aks4d1p5  43322  aks4d1p6  43323  aks4d1p7d1  43324  aks4d1p7  43325  aks4d1p8d2  43327  aks4d1p8d3  43328  aks4d1p8  43329  aks4d1p9  43330  posbezout  43342  primrootlekpowne0  43347  primrootspoweq0  43348  aks6d1c1  43358  aks6d1c2p2  43361  hashscontpow1  43363  aks6d1c3  43365  aks6d1c2lem4  43369  aks6d1c2  43372  2np3bcnp1  43386  2ap1caineq  43387  sticksstones6  43393  sticksstones7  43394  sticksstones10  43397  sticksstones12a  43399  sticksstones12  43400  sticksstones22  43410  aks6d1c6lem3  43414  aks6d1c6lem4  43415  bcled  43420  bcle2d  43421  aks6d1c7lem1  43422  aks6d1c7lem2  43423  unitscyglem2  43438  unitscyglem4  43440  unitscyglem5  43441  aks5lem8  43443  sn-1ne2  43523  redvmptabs  43604  sn-00idlem2  43643  sn-0ne2  43650  rei4  43668  rediveq1d  43695  sn-rediv1d  43696  sn-rereccld  43699  rerecne0d  43700  rerecidd  43701  rerecrecd  43703  sn-0tie0  43708  sn-nnne0  43717  mulgt0b1d  43729  sn-ltmulgt11d  43731  sn-0lt1  43732  sn-mulgt1d  43736  fimgmcyc  43791  fltnlta  43867  3cubeslem1  43887  3cubeslem3r  43890  3cubeslem4  43892  lzenom  43974  irrapxlem1  44022  irrapxlem2  44023  irrapxlem4  44025  irrapxlem5  44026  pellexlem2  44030  pell1qrge1  44070  pell1qr1  44071  elpell1qr2  44072  pell14qrgapw  44076  pellfundgt1  44083  pellfundglb  44085  pellfundex  44086  pellfundrp  44088  pellfundne1  44089  rmspecsqrtnq  44106  rmspecnonsq  44107  rmspecfund  44109  rmspecpos  44116  monotoddzzfi  44142  rmygeid  44164  areaquad  44410  imo72b2lem0  45357  imo72b2lem1  45361  imo72b2  45364  cvgdvgrat  45489  radcnvrat  45490  hashnzfzclim  45498  lhe4.4ex1a  45505  binomcxplemnn0  45525  binomcxplemdvbinom  45529  binomcxplemnotnn0  45532  oddfl  46499  abscosbd  46500  zltlesub  46506  abssinbd  46516  monoords  46518  fzisoeu  46521  fzdifsuc2  46531  suplesup  46556  xralrple2  46571  infxr  46583  infleinflem2  46587  reclt0d  46603  xrralrecnnge  46606  sqrlearg  46770  iooiinioc  46773  fmul01  46797  fmul01lt1lem1  46801  fmul01lt1lem2  46802  climsuselem1  46824  sumnnodd  46847  0ellimcdiv  46864  dvmptidg  47132  dvcosax  47141  ioodvbdlimc1lem1  47146  ioodvbdlimc1lem2  47147  ioodvbdlimc2lem  47149  dvxpaek  47155  dvnmul  47158  iblspltprt  47188  itgspltprt  47194  stoweidlem5  47220  stoweidlem7  47222  stoweidlem10  47225  stoweidlem11  47226  stoweidlem12  47227  stoweidlem13  47228  stoweidlem14  47229  stoweidlem16  47231  stoweidlem18  47233  stoweidlem20  47235  stoweidlem24  47239  stoweidlem25  47240  stoweidlem34  47249  stoweidlem36  47251  stoweidlem38  47253  stoweidlem40  47255  stoweidlem41  47256  stoweidlem42  47257  stoweidlem45  47260  stoweidlem51  47266  stoweidlem60  47275  wallispilem3  47282  wallispilem4  47283  wallispilem5  47284  wallispi  47285  wallispi2lem1  47286  wallispi2lem2  47287  wallispi2  47288  stirlinglem1  47289  stirlinglem3  47291  stirlinglem5  47293  stirlinglem6  47294  stirlinglem7  47295  stirlinglem8  47296  stirlinglem10  47298  stirlinglem11  47299  stirlinglem12  47300  stirlinglem13  47301  stirlinglem15  47303  dirker2re  47307  dirkerval2  47309  dirkerre  47310  dirkertrigeqlem1  47313  dirkertrigeqlem3  47315  dirkeritg  47317  dirkercncflem1  47318  dirkercncflem2  47319  dirkercncflem4  47321  fourierdlem5  47327  fourierdlem6  47328  fourierdlem11  47333  fourierdlem15  47337  fourierdlem19  47341  fourierdlem20  47342  fourierdlem24  47346  fourierdlem26  47348  fourierdlem28  47350  fourierdlem30  47352  fourierdlem39  47361  fourierdlem41  47363  fourierdlem43  47365  fourierdlem47  47368  fourierdlem48  47369  fourierdlem56  47377  fourierdlem60  47381  fourierdlem61  47382  fourierdlem62  47383  fourierdlem64  47385  fourierdlem65  47386  fourierdlem66  47387  fourierdlem68  47389  fourierdlem73  47394  fourierdlem78  47399  fourierdlem79  47400  fourierdlem87  47408  fourierdlem103  47424  fourierdlem104  47425  sqwvfoura  47443  fouriersw  47446  etransclem4  47453  etransclem23  47472  etransclem24  47473  etransclem31  47480  etransclem32  47481  etransclem35  47484  etransclem41  47490  etransclem46  47495  etransclem48  47497  etransc  47498  ioorrnopnxrlem  47521  nnfoctbdjlem  47670  iundjiun  47675  hoidmvlelem1  47810  hoidmvlelem2  47811  hoidmvlelem3  47812  hoidmvlelem4  47813  ovnhoilem1  47816  vonioolem2  47896  vonicclem2  47899  pimrecltneg  47939  smfrec  48004  smfmullem1  48006  smfmullem2  48007  smfdiv  48012  sigaradd  48081  ormkglobd  48092  cjnpoly  48144  p1lep2  48575  zm1nn  48577  ceilhalfgt1  48608  2tceilhalfelfzo1  48611  ceilbi  48612  rehalfge1  48614  ceilhalfnn  48615  flmrecm1  48618  addmodne  48625  m1mod0mod1  48635  m1modmmod  48639  difmodm1lt  48640  modmknepk  48643  modp2nep1  48648  modm1nem2  48650  2timesltsqm1  48654  muldvdsfacm1  48662  iccpartiltu  48709  iccpartlt  48711  iccpartgt  48714  fmtnoge3  48820  fmtnodvds  48834  fmtnoprmfac2lem1  48856  2pwp1prm  48879  flsqrt  48883  sfprmdvdsmersenne  48893  lighneallem2  48896  lighneallem4a  48898  proththdlem  48903  proththd  48904  nprmdvdsfacm1lem4  48913  nnoALTV  48998  bgoldbtbndlem4  49111  gpgprismgrusgra  49361  gpgedgvtx0  49364  gpgvtxedg0  49366  gpg5nbgrvtx03starlem2  49372  gpg3kgrtriexlem4  49389  gpg3kgrtriexlem6  49391  cznnring  49564  divge1b  49829  divgt1b  49830  nn0eo  49845  regt1loggt0  49853  rege1logbrege0  49875  logblt1b  49881  fllog2  49885  nnolog2flm1  49907  dignn0flhalflem1  49932  rrxlinesc  50053  rrxlinec  50054  eenglngeehlnmlem1  50055  eenglngeehlnmlem2  50056  line2ylem  50068  line2  50069  line2xlem  50070  reseccl  51126  recsccl  51127  amgmwlem  51267  amgmlemALT  51268