Theorem 1red 10907

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℝcr 10801  1c1 10803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-mulcl 10864  ax-mulrcl 10865  ax-i2m1 10870  ax-1ne0 10871  ax-rrecex 10874  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258

This theorem is referenced by:  recgt0  11751  ltrec  11787  nnne0  11937  nn0p1gt0  12192  nn0ge2m1nn  12232  nn0le2is012  12314  suprzcl  12330  ledivge1le  12730  qbtwnre  12862  lincmb01cmp  13156  iccf1o  13157  xov1plusxeqvd  13159  zltaddlt1le  13166  fznatpl1  13239  elfz1b  13254  fzonn0p1p1  13394  elfznelfzo  13420  elfznelfzob  13421  fladdz  13473  2tnp1ge0ge0  13477  flhalf  13478  ltdifltdiv  13482  fldiv4lem1div2uz2  13484  mulp1mod1  13560  m1modge3gt1  13566  modltm1p1mod  13571  addmodlteq  13594  ltexp2a  13812  expcan  13815  ltexp2  13816  leexp2  13817  leexp2a  13818  leexp2r  13820  nnlesq  13850  bernneq3  13874  expnbnd  13875  expnlbnd2  13877  expnngt1  13884  fzsdom2  14071  wrdlenge2n0  14183  swrd2lsw  14593  2swrd2eqwrdeq  14594  sqrlem7  14888  rddif  14980  reccn2  15234  rlimo1  15254  o1fsum  15453  abscvgcvg  15459  climcndslem1  15489  flo1  15494  harmonic  15499  geomulcvg  15516  fprodrecl  15591  fprodreclf  15597  fprodle  15634  bpoly4  15697  efcllem  15715  efgt1  15753  tanhlt1  15797  sinltx  15826  eirrlem  15841  p1modz1  15898  mod2eq1n2dvds  15984  oddge22np1  15986  ltoddhalfle  15998  nn0o1gt2  16018  nno  16019  nn0oddm1d2  16022  nnoddm1d2  16023  bitsfzolem  16069  bitsfzo  16070  bitsmod  16071  bitscmp  16073  bitsinv1lem  16076  smuval2  16117  coprmgcdb  16282  prmind2  16318  dvdsnprmd  16323  2mulprm  16326  isprm5  16340  isprm7  16341  divdenle  16381  zsqrtelqelz  16390  fermltl  16413  odzdvds  16424  modprm0  16434  iserodd  16464  difsqpwdvds  16516  pcfaclem  16527  prmreclem1  16545  4sqlem11  16584  4sqlem12  16585  ramub1lem1  16655  prmgaplem8  16687  2expltfac  16722  pgpfaclem2  19600  znidomb  20681  chfacfisf  21911  chfacfisfcpmat  21912  chfacfscmulgsum  21917  chfacfpmmulgsum  21921  nrginvrcnlem  23761  nmoid  23812  xrsmopn  23881  metnrmlem1a  23927  iccpnfhmeo  24014  lebnumii  24035  htpycc  24049  pcohtpylem  24088  pcoass  24093  pcorevlem  24095  nmhmcn  24189  cncmet  24391  ovoliunlem1  24571  dyadmaxlem  24666  vitalilem2  24678  mbfi1fseqlem6  24790  itg2mulc  24817  itg2monolem1  24820  itg2monolem3  24822  dveflem  25048  mvth  25061  dvlipcn  25063  lhop1lem  25082  dvfsumlem1  25095  dvfsumlem2  25096  dvfsumlem3  25097  dvfsumlem4  25098  dvfsum2  25103  fta1glem2  25236  plyeq0lem  25276  fta1lem  25372  vieta1lem2  25376  aalioulem3  25399  aalioulem4  25400  radcnvlem1  25477  radcnvlem2  25478  dvradcnv  25485  abelthlem2  25496  abelthlem5  25499  abelthlem7  25502  abelth2  25506  cos02pilt1  25587  cosne0  25590  rplogcl  25664  logdivlti  25680  logno1  25696  dvlog2lem  25712  advlog  25714  logtayllem  25719  cxplt  25754  cxple  25755  cxpaddlelem  25809  cxpaddle  25810  relogbf  25846  logbgt0b  25848  isosctrlem1  25873  isosctrlem2  25874  chordthmlem4  25890  heron  25893  atanlogaddlem  25968  bndatandm  25984  leibpi  25997  log2tlbnd  26000  birthdaylem3  26008  rlimcnp  26020  rlimcnp2  26021  efrlim  26024  cxp2limlem  26030  cxp2lim  26031  divsqrtsumo1  26038  jensenlem2  26042  logdiflbnd  26049  fsumharmonic  26066  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem4  26086  lgamgulmlem5  26087  lgamgulmlem6  26088  lgamcvg2  26109  regamcl  26115  wilthlem2  26123  ftalem2  26128  basellem9  26143  vma1  26220  ppieq0  26230  mumullem2  26234  fsumfldivdiaglem  26243  chpeq0  26261  chtub  26265  chpval2  26271  chpchtsum  26272  chpub  26273  logfacrlim  26277  logexprlim  26278  mersenne  26280  perfectlem2  26283  dchrelbas4  26296  bcmono  26330  bposlem1  26337  bposlem2  26338  zabsle1  26349  lgslem3  26352  lgsmod  26376  lgsdir2lem4  26381  lgsdirprm  26384  gausslemma2dlem1a  26418  gausslemma2d  26427  lgsquadlem2  26434  2sqlem8  26479  chebbnd1lem1  26522  chebbnd1lem2  26523  chtppilimlem1  26526  chebbnd2  26530  chto1lb  26531  chpchtlim  26532  chpo1ubb  26534  vmadivsum  26535  rplogsumlem1  26537  rpvmasumlem  26540  dchrisumlem3  26544  dchrmusumlema  26546  dchrmusum2  26547  dchrvmasumlem2  26551  dchrvmasumlem3  26552  dchrvmasumiflem1  26554  dchrvmasumiflem2  26555  dchrisum0flblem1  26561  dchrisum0flblem2  26562  dchrisum0fno1  26564  dchrisum0re  26566  dchrisum0lema  26567  dchrisum0lem1b  26568  dchrisum0lem2a  26570  dchrisum0lem2  26571  dchrisum0lem3  26572  rplogsum  26580  dirith2  26581  mudivsum  26583  mulogsumlem  26584  mulogsum  26585  mulog2sumlem1  26587  mulog2sumlem2  26588  vmalogdivsum2  26591  vmalogdivsum  26592  2vmadivsumlem  26593  log2sumbnd  26597  selberglem2  26599  selberg2lem  26603  chpdifbnd  26608  selberg3lem1  26610  selberg3  26612  selberg4lem1  26613  selberg4  26614  pntrmax  26617  pntrsumo1  26618  pntrsumbnd  26619  selberg3r  26622  selberg4r  26623  selberg34r  26624  pntrlog2bndlem1  26630  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntrlog2bndlem6  26636  pntrlog2bnd  26637  pntpbnd1a  26638  pntpbnd1  26639  pntibndlem2a  26643  pntibndlem2  26644  pntibnd  26646  pntlemc  26648  pntlemg  26651  pntlemr  26655  pntlemk  26659  pnt  26667  qabvle  26678  ostth2lem3  26688  ostth2  26690  trgcgrg  26780  tgcgr4  26796  ttgcontlem1  27155  axpaschlem  27211  axlowdimlem16  27228  axcontlem2  27236  axcontlem7  27241  nbusgrvtxm1  27649  upgrewlkle2  27876  pthdlem1  28035  crctcshwlkn0lem3  28078  crctcshwlkn0lem5  28080  wwlksm1edg  28147  wwlksnextproplem2  28176  clwlkclwwlklem2fv1  28260  clwlkclwwlklem2fv2  28261  clwlkclwwlklem2  28265  clwlkclwwlk2  28268  clwwisshclwwslem  28279  clwwlkf1  28314  clwwlkext2edg  28321  clwlknf1oclwwlknlem1  28346  clwwlknonex2lem2  28373  numclwwlk7  28656  frgrreggt1  28658  frgrogt3nreg  28662  smcnlem  28960  nmoub3i  29036  blocnilem  29067  ubthlem2  29134  minvecolem4  29143  htthlem  29180  nmcexi  30289  nmopcoi  30358  stadd3i  30511  cdj1i  30696  nnmulge  30975  nndiffz1  31009  fzsplit3  31017  wrdt2ind  31127  pmtrto1cl  31268  fzto1st1  31271  fzto1st  31272  psgnfzto1st  31274  cycpmco2lem6  31300  cycpmco2lem7  31301  cycpmrn  31312  qsidomlem1  31530  krull  31545  1smat1  31656  submateqlem1  31659  madjusmdetlem2  31680  unitdivcld  31753  sqsscirc1  31760  nexple  31877  indf1o  31892  esumdivc  31951  dya2ub  32137  dya2iocress  32141  dya2iocbrsiga  32142  dya2icobrsiga  32143  dya2icoseg  32144  dya2iocucvr  32151  sxbrsigalem2  32153  fibp1  32268  probmeasb  32297  dstrvprob  32338  dstfrvunirn  32341  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemsgt1  32377  ballotlemsel1i  32379  ballotlemfrcn0  32396  signsply0  32430  itgexpif  32486  reprlt  32499  chtvalz  32509  breprexplemc  32512  breprexp  32513  circlemeth  32520  tgoldbachgnn  32539  acycgr1v  33011  subfaclim  33050  cvmliftlem2  33148  cvmliftlem13  33158  snmlff  33191  bccolsum  33611  faclim  33618  nn0prpwlem  34438  dnibndlem10  34594  dnibndlem12  34596  knoppcnlem4  34603  unblimceq0  34614  knoppndvlem1  34619  knoppndvlem2  34620  knoppndvlem3  34621  knoppndvlem7  34625  knoppndvlem11  34629  knoppndvlem12  34630  knoppndvlem14  34632  knoppndvlem15  34633  knoppndvlem17  34635  knoppndvlem18  34636  knoppndvlem20  34638  irrdiff  35424  poimirlem6  35710  poimirlem7  35711  poimirlem15  35719  poimirlem19  35723  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimirlem32  35736  broucube  35738  itg2addnclem2  35756  itg2addnclem3  35757  areacirclem1  35792  areacirclem4  35795  incsequz  35833  totbndbnd  35874  bfplem2  35908  resdvopclptsd  39964  lcmineqlem2  39966  lcmineqlem3  39967  lcmineqlem10  39974  lcmineqlem12  39976  lcmineqlem15  39979  lcmineqlem18  39982  lcmineqlem19  39983  lcmineqlem20  39984  lcmineqlem22  39986  lcmineqlem23  39987  3lexlogpow5ineq2  39991  3lexlogpow5ineq4  39992  3lexlogpow5ineq3  39993  3lexlogpow2ineq1  39994  3lexlogpow2ineq2  39995  3lexlogpow5ineq5  39996  aks4d1lem1  39998  dvrelog2  40000  dvrelog3  40001  dvrelog2b  40002  dvrelogpow2b  40004  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1p6  40009  aks4d1p1p7  40010  aks4d1p1p5  40011  aks4d1p1  40012  aks4d1p2  40013  aks4d1p3  40014  aks4d1p5  40016  aks4d1p6  40017  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8d2  40021  aks4d1p8d3  40022  aks4d1p8  40023  aks4d1p9  40024  2np3bcnp1  40028  2ap1caineq  40029  sticksstones6  40035  sticksstones7  40036  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  sticksstones22  40052  metakunt1  40053  metakunt2  40054  metakunt7  40059  metakunt15  40067  metakunt16  40068  metakunt24  40076  metakunt28  40080  metakunt29  40081  2xp3dxp2ge1d  40090  factwoffsmonot  40091  sn-1ne2  40216  rtprmirr  40268  sn-00idlem2  40303  sn-0ne2  40310  sn-0tie0  40342  mulgt0b2d  40351  flt4lem7  40412  fltnlta  40416  3cubeslem1  40422  3cubeslem3r  40425  3cubeslem4  40427  lzenom  40508  irrapxlem1  40560  irrapxlem2  40561  irrapxlem4  40563  irrapxlem5  40564  pellexlem2  40568  pell1qrge1  40608  pell1qr1  40609  elpell1qr2  40610  pell14qrgapw  40614  pellfundgt1  40621  pellfundglb  40623  pellfundex  40624  pellfundrp  40626  pellfundne1  40627  rmspecsqrtnq  40644  rmspecnonsq  40645  rmspecfund  40647  rmspecpos  40654  monotoddzzfi  40680  rmygeid  40702  areaquad  40963  imo72b2lem0  41665  imo72b2lem1  41669  imo72b2  41672  cvgdvgrat  41820  radcnvrat  41821  hashnzfzclim  41829  lhe4.4ex1a  41836  binomcxplemnn0  41856  binomcxplemdvbinom  41860  binomcxplemnotnn0  41863  oddfl  42705  abscosbd  42706  zltlesub  42713  abssinbd  42724  monoords  42726  fzisoeu  42729  fzdifsuc2  42739  suplesup  42768  xralrple2  42783  infxr  42796  infleinflem2  42800  reclt0d  42816  xrralrecnnge  42820  sqrlearg  42981  iooiinioc  42984  fmul01  43011  fmul01lt1lem1  43015  fmul01lt1lem2  43016  climsuselem1  43038  sumnnodd  43061  0ellimcdiv  43080  dvmptidg  43348  dvcosax  43357  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvxpaek  43371  dvnmul  43374  iblspltprt  43404  itgspltprt  43410  stoweidlem5  43436  stoweidlem7  43438  stoweidlem10  43441  stoweidlem11  43442  stoweidlem12  43443  stoweidlem13  43444  stoweidlem14  43445  stoweidlem16  43447  stoweidlem18  43449  stoweidlem20  43451  stoweidlem24  43455  stoweidlem25  43456  stoweidlem34  43465  stoweidlem36  43467  stoweidlem38  43469  stoweidlem40  43471  stoweidlem41  43472  stoweidlem42  43473  stoweidlem45  43476  stoweidlem51  43482  stoweidlem60  43491  wallispilem3  43498  wallispilem4  43499  wallispilem5  43500  wallispi  43501  wallispi2lem1  43502  wallispi2lem2  43503  wallispi2  43504  stirlinglem1  43505  stirlinglem3  43507  stirlinglem5  43509  stirlinglem6  43510  stirlinglem7  43511  stirlinglem8  43512  stirlinglem10  43514  stirlinglem11  43515  stirlinglem12  43516  stirlinglem13  43517  stirlinglem15  43519  dirker2re  43523  dirkerval2  43525  dirkerre  43526  dirkertrigeqlem1  43529  dirkertrigeqlem3  43531  dirkeritg  43533  dirkercncflem1  43534  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem5  43543  fourierdlem6  43544  fourierdlem11  43549  fourierdlem15  43553  fourierdlem19  43557  fourierdlem20  43558  fourierdlem24  43562  fourierdlem26  43564  fourierdlem28  43566  fourierdlem30  43568  fourierdlem39  43577  fourierdlem41  43579  fourierdlem43  43581  fourierdlem47  43584  fourierdlem48  43585  fourierdlem56  43593  fourierdlem60  43597  fourierdlem61  43598  fourierdlem62  43599  fourierdlem64  43601  fourierdlem65  43602  fourierdlem66  43603  fourierdlem68  43605  fourierdlem73  43610  fourierdlem78  43615  fourierdlem79  43616  fourierdlem87  43624  fourierdlem103  43640  fourierdlem104  43641  sqwvfoura  43659  fouriersw  43662  etransclem4  43669  etransclem23  43688  etransclem24  43689  etransclem31  43696  etransclem32  43697  etransclem35  43700  etransclem41  43706  etransclem46  43711  etransclem48  43713  etransc  43714  ioorrnopnxrlem  43737  nnfoctbdjlem  43883  iundjiun  43888  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  ovnhoilem1  44029  vonioolem2  44109  vonicclem2  44112  pimrecltneg  44147  smfrec  44210  smfmullem1  44212  smfmullem2  44213  smfdiv  44218  sigaradd  44269  p1lep2  44680  zm1nn  44682  m1mod0mod1  44709  iccpartiltu  44762  iccpartlt  44764  iccpartgt  44767  fmtnoge3  44870  fmtnodvds  44884  fmtnoprmfac2lem1  44906  2pwp1prm  44929  flsqrt  44933  sfprmdvdsmersenne  44943  lighneallem2  44946  lighneallem4a  44948  proththdlem  44953  proththd  44954  nnoALTV  45035  bgoldbtbndlem4  45148  cznnring  45402  divge1b  45741  divgt1b  45742  m1modmmod  45755  difmodm1lt  45756  nn0eo  45762  regt1loggt0  45770  rege1logbrege0  45792  logblt1b  45798  fllog2  45802  nnolog2flm1  45824  dignn0flhalflem1  45849  rrxlinesc  45969  rrxlinec  45970  eenglngeehlnmlem1  45971  eenglngeehlnmlem2  45972  line2ylem  45985  line2  45986  line2xlem  45987  reseccl  46341  recsccl  46342  amgmwlem  46392  amgmlemALT  46393