Theorem 1red 10055

Description: 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)

Assertion

Ref	Expression
1red	⊢ (𝜑 → 1 ∈ ℝ)

Proof of Theorem 1red

Step	Hyp	Ref	Expression
1		1re 10039	. 2 ⊢ 1 ∈ ℝ
2	1	a1i 11	1 ⊢ (𝜑 → 1 ∈ ℝ)

Syntax hints:   → wi 4   ∈ wcel 1990  ℝcr 9935  1c1 9937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-mulcl 9998  ax-mulrcl 9999  ax-i2m1 10004  ax-1ne0 10005  ax-rrecex 10008  ax-cnre 10009

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  recgt0  10867  ltrec  10905  nn0p1gt0  11322  nn0ge2m1nn  11360  nn0le2is012  11441  suprzcl  11457  ledivge1le  11901  qbtwnre  12030  iccf1o  12316  xov1plusxeqvd  12318  zltaddlt1le  12324  fznatpl1  12395  elfz1b  12409  fzonn0p1p1  12546  elfzom1p1elfzo  12547  elfznelfzo  12573  elfznelfzob  12574  fladdz  12626  2tnp1ge0ge0  12630  flhalf  12631  ltdifltdiv  12635  fldiv4lem1div2uz2  12637  mulp1mod1  12711  m1modge3gt1  12717  modltm1p1mod  12722  addmodlteq  12745  ltexp2a  12912  expcan  12913  ltexp2  12914  leexp2  12915  leexp2a  12916  leexp2r  12918  nnlesq  12968  bernneq3  12992  expnbnd  12993  expnlbnd2  12995  fzsdom2  13215  wrdlenge2n0  13341  swrd2lsw  13695  2swrd2eqwrdeq  13696  rddif  14080  reccn2  14327  rlimo1  14347  o1fsum  14545  abscvgcvg  14551  climcndslem1  14581  flo1  14586  harmonic  14591  geomulcvg  14607  fprodrecl  14683  fprodle  14727  bpoly4  14790  efcllem  14808  efgt1  14846  tanhlt1  14890  sinltx  14919  eirrlem  14932  mod2eq1n2dvds  15071  oddge22np1  15073  ltoddhalfle  15085  nn0o1gt2  15097  nno  15098  nn0oddm1d2  15101  nnoddm1d2  15102  bitsfzolem  15156  bitsfzo  15157  bitsmod  15158  bitscmp  15160  bitsinv1lem  15163  smuval2  15204  coprmgcdb  15362  prmind2  15398  dvdsnprmd  15403  isprm5  15419  isprm7  15420  divdenle  15457  zsqrtelqelz  15466  fermltl  15489  odzdvds  15500  modprm0  15510  iserodd  15540  difsqpwdvds  15591  pcfaclem  15602  prmreclem1  15620  4sqlem11  15659  4sqlem12  15660  ramub1lem1  15730  prmgaplem8  15762  2expltfac  15799  pgpfaclem2  18481  znidomb  19910  chfacfisf  20659  chfacfisfcpmat  20660  chfacfscmulgsum  20665  chfacfpmmulgsum  20669  nrginvrcnlem  22495  nmoid  22546  xrsmopn  22615  metnrmlem1a  22661  iccpnfhmeo  22744  htpycc  22779  pcohtpylem  22819  pcoass  22824  pcorevlem  22826  nmhmcn  22920  cncmet  23119  ovoliunlem1  23270  dyadmaxlem  23365  vitalilem2  23378  mbfi1fseqlem6  23487  itg2mulc  23514  itg2monolem1  23517  itg2monolem3  23519  dveflem  23742  mvth  23755  dvlipcn  23757  lhop1lem  23776  dvfsumlem1  23789  dvfsumlem2  23790  dvfsumlem3  23791  dvfsumlem4  23792  dvfsum2  23797  fta1glem2  23926  plyeq0lem  23966  fta1lem  24062  vieta1lem2  24066  aalioulem3  24089  aalioulem4  24090  radcnvlem1  24167  radcnvlem2  24168  dvradcnv  24175  abelthlem2  24186  abelthlem5  24189  abelthlem7  24192  abelth2  24196  cosne0  24276  rplogcl  24350  logdivlti  24366  logno1  24382  advlog  24400  logtayllem  24405  cxplt  24440  cxple  24441  cxpaddlelem  24492  cxpaddle  24493  relogbf  24529  isosctrlem1  24548  isosctrlem2  24549  heron  24565  atanlogaddlem  24640  bndatandm  24656  leibpi  24669  log2tlbnd  24672  birthdaylem3  24680  rlimcnp  24692  rlimcnp2  24693  efrlim  24696  cxp2limlem  24702  divsqrtsumo1  24710  jensenlem2  24714  logdiflbnd  24721  fsumharmonic  24738  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem4  24758  lgamgulmlem5  24759  lgamgulmlem6  24760  lgamcvg2  24781  regamcl  24787  wilthlem2  24795  ftalem2  24800  basellem9  24815  vma1  24892  ppieq0  24902  mumullem2  24906  fsumfldivdiaglem  24915  chpeq0  24933  chtub  24937  chpval2  24943  chpchtsum  24944  chpub  24945  logfacrlim  24949  logexprlim  24950  mersenne  24952  perfectlem2  24955  dchrelbas4  24968  bcmono  25002  bposlem1  25009  bposlem2  25010  zabsle1  25021  lgslem3  25024  lgslem4  25025  lgsmod  25048  lgsdir2lem4  25053  lgsdirprm  25056  gausslemma2dlem1a  25090  gausslemma2d  25099  lgsquadlem2  25106  2sqlem8  25151  chebbnd1lem1  25158  chebbnd1lem2  25159  chtppilimlem1  25162  chebbnd2  25166  chto1lb  25167  chpchtlim  25168  chpo1ubb  25170  vmadivsum  25171  rplogsumlem1  25173  rpvmasumlem  25176  dchrisumlem3  25180  dchrmusumlema  25182  dchrmusum2  25183  dchrvmasumlem2  25187  dchrvmasumlem3  25188  dchrvmasumiflem1  25190  dchrvmasumiflem2  25191  dchrisum0flblem1  25197  dchrisum0flblem2  25198  dchrisum0fno1  25200  dchrisum0re  25202  dchrisum0lema  25203  dchrisum0lem1b  25204  dchrisum0lem2a  25206  dchrisum0lem2  25207  dchrisum0lem3  25208  rplogsum  25216  dirith2  25217  mudivsum  25219  mulogsumlem  25220  mulogsum  25221  mulog2sumlem1  25223  mulog2sumlem2  25224  vmalogdivsum2  25227  vmalogdivsum  25228  2vmadivsumlem  25229  log2sumbnd  25233  selberglem2  25235  selberg2lem  25239  chpdifbnd  25244  selberg3lem1  25246  selberg3  25248  selberg4lem1  25249  selberg4  25250  pntrmax  25253  pntrsumo1  25254  pntrsumbnd  25255  selberg3r  25258  selberg4r  25259  selberg34r  25260  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntrlog2bnd  25273  pntpbnd1a  25274  pntpbnd1  25275  pntibndlem2a  25279  pntibndlem2  25280  pntibnd  25282  pntlemc  25284  pntlemg  25287  pntlemr  25291  pntlemk  25295  qabvle  25314  ostth2lem3  25324  ostth2  25326  trgcgrg  25410  tgcgr4  25426  ttgcontlem1  25765  axpaschlem  25820  axlowdimlem16  25837  axcontlem2  25845  axcontlem7  25850  nbusgrvtxm1  26281  upgrewlkle2  26502  pthdlem1  26662  crctcshwlkn0lem3  26704  crctcshwlkn0lem5  26706  wwlksm1edg  26767  wwlksnextproplem2  26805  clwlkclwwlklem2fv1  26896  clwlkclwwlklem2fv2  26897  clwlkclwwlklem2  26901  clwlkclwwlk2  26904  clwwlksf1  26917  clwwlksext2edg  26923  clwwisshclwwslem  26927  numclwwlkovf2exlem2  27212  numclwlk1lem2f1  27227  numclwwlk7  27249  frgrreggt1  27251  frgrogt3nreg  27255  smcnlem  27552  nmoub3i  27628  blocnilem  27659  ubthlem2  27727  minvecolem4  27736  htthlem  27774  nmcexi  28885  nmopcoi  28954  stadd3i  29107  cdj1i  29292  nn0sqeq1  29513  nnmulge  29515  nndiffz1  29548  fzsplit3  29553  pmtrto1cl  29849  fzto1st1  29852  fzto1st  29853  psgnfzto1st  29855  1smat1  29870  submateqlem1  29873  madjusmdetlem2  29894  unitdivcld  29947  sqsscirc1  29954  nexple  30071  indf1o  30086  esumdivc  30145  dya2ub  30332  dya2iocress  30336  dya2iocbrsiga  30337  dya2icobrsiga  30338  dya2icoseg  30339  dya2iocucvr  30346  sxbrsigalem2  30348  fibp1  30463  probmeasb  30492  dstrvprob  30533  dstfrvunirn  30536  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemsgt1  30572  ballotlemsel1i  30574  ballotlemfrcn0  30591  signsply0  30628  itgexpif  30684  reprlt  30697  chtvalz  30707  breprexplemc  30710  breprexp  30711  circlemeth  30718  tgoldbachgnn  30737  subfaclim  31170  cvmliftlem2  31268  cvmliftlem13  31278  snmlff  31311  bccolsum  31625  faclim  31632  nn0prpwlem  32317  dnibndlem10  32477  dnibndlem12  32479  knoppcnlem4  32486  unblimceq0  32498  knoppndvlem1  32503  knoppndvlem2  32504  knoppndvlem3  32505  knoppndvlem7  32509  knoppndvlem11  32513  knoppndvlem12  32514  knoppndvlem14  32516  knoppndvlem15  32517  knoppndvlem17  32519  knoppndvlem18  32520  knoppndvlem20  32522  poimirlem6  33415  poimirlem7  33416  poimirlem15  33424  poimirlem19  33428  poimirlem29  33438  poimirlem30  33439  poimirlem31  33440  poimirlem32  33441  broucube  33443  itg2addnclem2  33462  itg2addnclem3  33463  areacirclem1  33500  areacirclem4  33503  incsequz  33544  totbndbnd  33588  bfplem2  33622  lzenom  37333  irrapxlem1  37386  irrapxlem2  37387  irrapxlem4  37389  irrapxlem5  37390  pellexlem2  37394  pell1qrge1  37434  pell1qr1  37435  elpell1qr2  37436  pell14qrgapw  37440  pellfundgt1  37447  pellfundglb  37449  pellfundex  37450  pellfundrp  37452  pellfundne1  37453  rmspecsqrtnq  37470  rmspecnonsq  37472  rmspecfund  37474  rmspecpos  37481  monotoddzzfi  37507  rmygeid  37531  areaquad  37802  imo72b2lem0  38465  imo72b2lem1  38471  imo72b2  38475  cvgdvgrat  38512  radcnvrat  38513  hashnzfzclim  38521  lhe4.4ex1a  38528  binomcxplemnn0  38548  binomcxplemdvbinom  38552  binomcxplemnotnn0  38555  oddfl  39489  abscosbd  39490  zltlesub  39497  abssinbd  39509  monoords  39511  fzisoeu  39514  fzdifsuc2  39525  suplesup  39555  xralrple2  39570  infxr  39583  infleinflem2  39587  reclt0d  39607  xrralrecnnge  39613  sqrlearg  39780  iooiinioc  39783  fmul01  39812  fmul01lt1lem1  39816  fmul01lt1lem2  39817  climsuselem1  39839  sumnnodd  39862  0ellimcdiv  39881  dvmptidg  40131  dvcosax  40141  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvxpaek  40155  dvnmul  40158  iblspltprt  40189  itgspltprt  40195  stoweidlem5  40222  stoweidlem7  40224  stoweidlem10  40227  stoweidlem11  40228  stoweidlem12  40229  stoweidlem13  40230  stoweidlem14  40231  stoweidlem16  40233  stoweidlem18  40235  stoweidlem20  40237  stoweidlem24  40241  stoweidlem25  40242  stoweidlem34  40251  stoweidlem36  40253  stoweidlem38  40255  stoweidlem40  40257  stoweidlem41  40258  stoweidlem42  40259  stoweidlem45  40262  stoweidlem51  40268  stoweidlem60  40277  wallispilem3  40284  wallispilem4  40285  wallispilem5  40286  wallispi  40287  wallispi2lem1  40288  wallispi2lem2  40289  wallispi2  40290  stirlinglem1  40291  stirlinglem3  40293  stirlinglem5  40295  stirlinglem6  40296  stirlinglem7  40297  stirlinglem8  40298  stirlinglem10  40300  stirlinglem11  40301  stirlinglem12  40302  stirlinglem13  40303  stirlinglem15  40305  dirker2re  40309  dirkerval2  40311  dirkerre  40312  dirkertrigeqlem1  40315  dirkertrigeqlem3  40317  dirkeritg  40319  dirkercncflem1  40320  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem5  40329  fourierdlem6  40330  fourierdlem11  40335  fourierdlem15  40339  fourierdlem19  40343  fourierdlem20  40344  fourierdlem24  40348  fourierdlem26  40350  fourierdlem28  40352  fourierdlem30  40354  fourierdlem39  40363  fourierdlem41  40365  fourierdlem43  40367  fourierdlem47  40370  fourierdlem48  40371  fourierdlem56  40379  fourierdlem60  40383  fourierdlem61  40384  fourierdlem62  40385  fourierdlem64  40387  fourierdlem65  40388  fourierdlem66  40389  fourierdlem68  40391  fourierdlem73  40396  fourierdlem78  40401  fourierdlem79  40402  fourierdlem87  40410  fourierdlem103  40426  fourierdlem104  40427  sqwvfoura  40445  fouriersw  40448  etransclem4  40455  etransclem23  40474  etransclem24  40475  etransclem31  40482  etransclem32  40483  etransclem35  40486  etransclem41  40492  etransclem46  40497  etransclem48  40499  etransc  40500  ioorrnopnxrlem  40526  nnfoctbdjlem  40672  iundjiun  40677  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem3  40811  hoidmvlelem4  40812  ovnhoilem1  40815  vonioolem2  40895  vonicclem2  40898  pimrecltneg  40933  smfrec  40996  smfmullem1  40998  smfmullem2  40999  smfdiv  41004  sigaradd  41055  p1lep2  41314  zm1nn  41316  m1mod0mod1  41339  iccpartiltu  41358  iccpartlt  41360  iccpartgt  41363  pfx2  41412  fmtnoge3  41442  fmtnodvds  41456  fmtnoprmfac2lem1  41478  2pwp1prm  41503  flsqrt  41508  sfprmdvdsmersenne  41520  lighneallem2  41523  lighneallem4a  41525  proththdlem  41530  proththd  41531  nnoALTV  41606  bgoldbtbndlem4  41696  cznnring  41956  divge1b  42302  divgt1b  42303  m1modmmod  42316  difmodm1lt  42317  nn0eo  42322  regt1loggt0  42330  rege1logbrege0  42352  logblt1b  42358  fllog2  42362  nnolog2flm1  42384  dignn0flhalflem1  42409  reseccl  42494  recsccl  42495  amgmwlem  42548  amgmlemALT  42549