Theorem 1red 11145

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

Syntax hints:   → wi 4   ∈ wcel 2114  ℝcr 11037  1c1 11039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371

This theorem is referenced by:  recgt0  11999  mulgt1  12015  ltrec  12036  nnne0  12191  nn0p1gt0  12442  nn0ge2m1nn  12483  nn0le2is012  12568  suprzcl  12584  ledivge1le  12990  ge2halflem1  13034  qbtwnre  13126  lincmb01cmp  13423  iccf1o  13424  xov1plusxeqvd  13426  zltaddlt1le  13433  fznatpl1  13506  elfz1b  13521  elfzo0subge1  13633  fzonn0p1p1  13672  elfznelfzo  13701  elfznelfzob  13702  fladdz  13757  2tnp1ge0ge0  13761  flhalf  13762  ltdifltdiv  13766  fldiv4lem1div2uz2  13768  mulp1mod1  13846  m1modge3gt1  13853  modltm1p1mod  13858  addmodlteq  13881  ltexp2a  14101  expcan  14104  ltexp2  14105  leexp2  14106  leexp2a  14107  leexp2r  14109  nnlesq  14140  bernneq3  14166  expnbnd  14167  expnlbnd2  14169  expnngt1  14176  fzsdom2  14363  wrdlenge2n0  14487  swrd2lsw  14887  2swrd2eqwrdeq  14888  01sqrexlem7  15183  rddif  15276  reccn2  15532  rlimo1  15552  o1fsum  15748  abscvgcvg  15754  climcndslem1  15784  flo1  15789  harmonic  15794  geomulcvg  15811  fprodrecl  15888  fprodreclf  15894  fprodle  15931  bpoly4  15994  efcllem  16012  efgt1  16053  tanhlt1  16097  sinltx  16126  eirrlem  16141  p1modz1  16198  mod2eq1n2dvds  16286  oddge22np1  16288  ltoddhalfle  16300  nn0o1gt2  16320  nno  16321  nn0oddm1d2  16324  nnoddm1d2  16325  bitsfzolem  16373  bitsfzo  16374  bitsmod  16375  bitscmp  16377  bitsinv1lem  16380  smuval2  16421  coprmgcdb  16588  prmind2  16624  dvdsnprmd  16629  2mulprm  16632  isprm5  16646  isprm7  16647  divdenle  16688  zsqrtelqelz  16697  fermltl  16723  odzdvds  16735  modprm0  16745  iserodd  16775  difsqpwdvds  16827  pcfaclem  16838  prmreclem1  16856  4sqlem11  16895  4sqlem12  16896  ramub1lem1  16966  prmgaplem8  16998  2expltfac  17032  chnccat  18561  pgpfaclem2  20025  znidomb  21528  psdmvr  22124  chfacfisf  22810  chfacfisfcpmat  22811  chfacfscmulgsum  22816  chfacfpmmulgsum  22820  nrginvrcnlem  24647  nmoid  24698  xrsmopn  24769  metnrmlem1a  24815  iihalf2cn  24897  iccpnfhmeo  24911  lebnumii  24933  htpycc  24947  pcohtpylem  24987  pcoass  24992  pcorevlem  24994  nmhmcn  25088  cncmet  25290  ovoliunlem1  25471  dyadmaxlem  25566  vitalilem2  25578  mbfi1fseqlem6  25689  itg2mulc  25716  itg2monolem1  25719  itg2monolem3  25721  dveflem  25951  mvth  25965  dvlipcn  25967  lhop1lem  25986  dvfsumlem1  26000  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsumlem3  26003  dvfsumlem4  26004  dvfsum2  26009  fta1glem2  26142  plyeq0lem  26183  fta1lem  26283  vieta1lem2  26287  aalioulem3  26310  aalioulem4  26311  radcnvlem1  26390  radcnvlem2  26391  dvradcnv  26398  abelthlem2  26410  abelthlem5  26413  abelthlem7  26416  abelth2  26420  cos02pilt1  26503  cosne0  26506  rplogcl  26581  logdivlti  26597  logno1  26613  dvlog2lem  26629  advlog  26631  logtayllem  26636  cxplt  26671  cxple  26672  cxpaddlelem  26729  cxpaddle  26730  rtprmirr  26738  relogbf  26769  logbgt0b  26771  isosctrlem1  26796  isosctrlem2  26797  chordthmlem4  26813  heron  26816  atanlogaddlem  26891  bndatandm  26907  leibpi  26920  log2tlbnd  26923  birthdaylem3  26931  rlimcnp  26943  rlimcnp2  26944  efrlim  26947  efrlimOLD  26948  cxp2limlem  26954  cxp2lim  26955  divsqrtsumo1  26962  jensenlem2  26966  logdiflbnd  26973  fsumharmonic  26990  lgamgulmlem2  27008  lgamgulmlem3  27009  lgamgulmlem4  27010  lgamgulmlem5  27011  lgamgulmlem6  27012  lgamcvg2  27033  regamcl  27039  wilthlem2  27047  ftalem2  27052  basellem9  27067  vma1  27144  ppieq0  27154  mumullem2  27158  fsumfldivdiaglem  27167  chpeq0  27187  chtub  27191  chpval2  27197  chpchtsum  27198  chpub  27199  logfacrlim  27203  logexprlim  27204  mersenne  27206  perfectlem2  27209  dchrelbas4  27222  bcmono  27256  bposlem1  27263  bposlem2  27264  zabsle1  27275  lgslem3  27278  lgsmod  27302  lgsdir2lem4  27307  lgsdirprm  27310  gausslemma2dlem1a  27344  gausslemma2d  27353  lgsquadlem2  27360  2sqlem8  27405  chebbnd1lem1  27448  chebbnd1lem2  27449  chtppilimlem1  27452  chebbnd2  27456  chto1lb  27457  chpchtlim  27458  chpo1ubb  27460  vmadivsum  27461  rplogsumlem1  27463  rpvmasumlem  27466  dchrisumlem3  27470  dchrmusumlema  27472  dchrmusum2  27473  dchrvmasumlem2  27477  dchrvmasumlem3  27478  dchrvmasumiflem1  27480  dchrvmasumiflem2  27481  dchrisum0flblem1  27487  dchrisum0flblem2  27488  dchrisum0fno1  27490  dchrisum0re  27492  dchrisum0lema  27493  dchrisum0lem1b  27494  dchrisum0lem2a  27496  dchrisum0lem2  27497  dchrisum0lem3  27498  rplogsum  27506  dirith2  27507  mudivsum  27509  mulogsumlem  27510  mulogsum  27511  mulog2sumlem1  27513  mulog2sumlem2  27514  vmalogdivsum2  27517  vmalogdivsum  27518  2vmadivsumlem  27519  log2sumbnd  27523  selberglem2  27525  selberg2lem  27529  chpdifbnd  27534  selberg3lem1  27536  selberg3  27538  selberg4lem1  27539  selberg4  27540  pntrmax  27543  pntrsumo1  27544  pntrsumbnd  27545  selberg3r  27548  selberg4r  27549  selberg34r  27550  pntrlog2bndlem1  27556  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem4  27559  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntrlog2bnd  27563  pntpbnd1a  27564  pntpbnd1  27565  pntibndlem2a  27569  pntibndlem2  27570  pntibnd  27572  pntlemc  27574  pntlemg  27577  pntlemr  27581  pntlemk  27585  pnt  27593  qabvle  27604  ostth2lem3  27614  ostth2  27616  trgcgrg  28599  tgcgr4  28615  ttgcontlem1  28969  axpaschlem  29025  axlowdimlem16  29042  axcontlem2  29050  axcontlem7  29055  nbusgrvtxm1  29464  upgrewlkle2  29692  pthdlem1  29851  crctcshwlkn0lem3  29897  crctcshwlkn0lem5  29899  wwlksm1edg  29966  wwlksnextproplem2  29995  clwlkclwwlklem2fv1  30082  clwlkclwwlklem2fv2  30083  clwlkclwwlklem2  30087  clwlkclwwlk2  30090  clwwisshclwwslem  30101  clwwlkf1  30136  clwwlkext2edg  30143  clwlknf1oclwwlknlem1  30168  clwwlknonex2lem2  30195  numclwwlk7  30478  frgrreggt1  30480  frgrogt3nreg  30484  smcnlem  30784  nmoub3i  30860  blocnilem  30891  ubthlem2  30958  minvecolem4  30967  htthlem  31004  nmcexi  32113  nmopcoi  32182  stadd3i  32335  cdj1i  32520  nnmulge  32828  receqid  32834  nndiffz1  32876  fzsplit3  32883  nexple  32935  indf1o  32956  wrdt2ind  33045  pmtrto1cl  33192  fzto1st1  33195  fzto1st  33196  psgnfzto1st  33198  cycpmco2lem6  33224  cycpmco2lem7  33225  cycpmrn  33236  qsidomlem1  33544  krull  33571  ply1degltel  33686  ply1degltlss  33688  constrnegcl  33940  constrdircl  33942  iconstr  33943  constrrecl  33946  constrmulcl  33948  constrreinvcl  33949  constrresqrtcl  33954  cos9thpiminplylem1  33959  cos9thpiminply  33965  cos9thpinconstrlem1  33966  1smat1  33981  submateqlem1  33984  madjusmdetlem2  34005  unitdivcld  34078  sqsscirc1  34085  esumdivc  34260  dya2ub  34447  dya2iocress  34451  dya2iocbrsiga  34452  dya2icobrsiga  34453  dya2icoseg  34454  dya2iocucvr  34461  sxbrsigalem2  34463  fibp1  34578  probmeasb  34607  dstrvprob  34649  dstfrvunirn  34652  ballotlemfc0  34670  ballotlemfcc  34671  ballotlemsgt1  34688  ballotlemsel1i  34690  ballotlemfrcn0  34707  signsply0  34728  itgexpif  34783  reprlt  34796  chtvalz  34806  breprexplemc  34809  breprexp  34810  circlemeth  34817  tgoldbachgnn  34836  acycgr1v  35362  subfaclim  35401  cvmliftlem2  35499  cvmliftlem13  35509  snmlff  35542  bccolsum  35952  faclim  35959  nn0prpwlem  36535  dnibndlem10  36706  dnibndlem12  36708  knoppcnlem4  36715  unblimceq0  36726  knoppndvlem1  36731  knoppndvlem2  36732  knoppndvlem3  36733  knoppndvlem7  36737  knoppndvlem11  36741  knoppndvlem12  36742  knoppndvlem14  36744  knoppndvlem15  36745  knoppndvlem17  36747  knoppndvlem18  36748  knoppndvlem20  36750  irrdiff  37575  poimirlem6  37871  poimirlem7  37872  poimirlem15  37880  poimirlem19  37884  poimirlem29  37894  poimirlem30  37895  poimirlem31  37896  poimirlem32  37897  broucube  37899  itg2addnclem2  37917  itg2addnclem3  37918  areacirclem1  37953  areacirclem4  37956  incsequz  37993  totbndbnd  38034  bfplem2  38068  resdvopclptsd  42392  lcmineqlem2  42394  lcmineqlem3  42395  lcmineqlem10  42402  lcmineqlem12  42404  lcmineqlem15  42407  lcmineqlem18  42410  lcmineqlem19  42411  lcmineqlem20  42412  lcmineqlem22  42414  lcmineqlem23  42415  3lexlogpow5ineq2  42419  3lexlogpow5ineq4  42420  3lexlogpow5ineq3  42421  3lexlogpow2ineq1  42422  3lexlogpow2ineq2  42423  3lexlogpow5ineq5  42424  aks4d1lem1  42426  dvrelog2  42428  dvrelog3  42429  dvrelog2b  42430  dvrelogpow2b  42432  aks4d1p1p3  42433  aks4d1p1p2  42434  aks4d1p1p4  42435  aks4d1p1p6  42437  aks4d1p1p7  42438  aks4d1p1p5  42439  aks4d1p1  42440  aks4d1p2  42441  aks4d1p3  42442  aks4d1p5  42444  aks4d1p6  42445  aks4d1p7d1  42446  aks4d1p7  42447  aks4d1p8d2  42449  aks4d1p8d3  42450  aks4d1p8  42451  aks4d1p9  42452  posbezout  42464  primrootlekpowne0  42469  primrootspoweq0  42470  aks6d1c1  42480  aks6d1c2p2  42483  hashscontpow1  42485  aks6d1c3  42487  aks6d1c2lem4  42491  aks6d1c2  42494  2np3bcnp1  42508  2ap1caineq  42509  sticksstones6  42515  sticksstones7  42516  sticksstones10  42519  sticksstones12a  42521  sticksstones12  42522  sticksstones22  42532  aks6d1c6lem3  42536  aks6d1c6lem4  42537  bcled  42542  bcle2d  42543  aks6d1c7lem1  42544  aks6d1c7lem2  42545  unitscyglem2  42560  unitscyglem4  42562  unitscyglem5  42563  aks5lem8  42565  sn-1ne2  42629  redvmptabs  42724  sn-00idlem2  42763  sn-0ne2  42770  rei4  42788  sn-rereccld  42812  rerecid  42813  sn-0tie0  42815  sn-nnne0  42824  mulgt0b1d  42836  sn-ltmulgt11d  42838  sn-0lt1  42839  sn-mulgt1d  42843  fimgmcyc  42898  flt4lem7  43011  fltnlta  43015  3cubeslem1  43035  3cubeslem3r  43038  3cubeslem4  43040  lzenom  43121  irrapxlem1  43173  irrapxlem2  43174  irrapxlem4  43176  irrapxlem5  43177  pellexlem2  43181  pell1qrge1  43221  pell1qr1  43222  elpell1qr2  43223  pell14qrgapw  43227  pellfundgt1  43234  pellfundglb  43236  pellfundex  43237  pellfundrp  43239  pellfundne1  43240  rmspecsqrtnq  43257  rmspecnonsq  43258  rmspecfund  43260  rmspecpos  43267  monotoddzzfi  43293  rmygeid  43315  areaquad  43567  imo72b2lem0  44515  imo72b2lem1  44519  imo72b2  44522  cvgdvgrat  44663  radcnvrat  44664  hashnzfzclim  44672  lhe4.4ex1a  44679  binomcxplemnn0  44699  binomcxplemdvbinom  44703  binomcxplemnotnn0  44706  oddfl  45634  abscosbd  45635  zltlesub  45641  abssinbd  45651  monoords  45653  fzisoeu  45656  fzdifsuc2  45666  suplesup  45692  xralrple2  45707  infxr  45719  infleinflem2  45723  reclt0d  45739  xrralrecnnge  45742  sqrlearg  45907  iooiinioc  45910  fmul01  45934  fmul01lt1lem1  45938  fmul01lt1lem2  45939  climsuselem1  45961  sumnnodd  45984  0ellimcdiv  46001  dvmptidg  46269  dvcosax  46278  ioodvbdlimc1lem1  46283  ioodvbdlimc1lem2  46284  ioodvbdlimc2lem  46286  dvxpaek  46292  dvnmul  46295  iblspltprt  46325  itgspltprt  46331  stoweidlem5  46357  stoweidlem7  46359  stoweidlem10  46362  stoweidlem11  46363  stoweidlem12  46364  stoweidlem13  46365  stoweidlem14  46366  stoweidlem16  46368  stoweidlem18  46370  stoweidlem20  46372  stoweidlem24  46376  stoweidlem25  46377  stoweidlem34  46386  stoweidlem36  46388  stoweidlem38  46390  stoweidlem40  46392  stoweidlem41  46393  stoweidlem42  46394  stoweidlem45  46397  stoweidlem51  46403  stoweidlem60  46412  wallispilem3  46419  wallispilem4  46420  wallispilem5  46421  wallispi  46422  wallispi2lem1  46423  wallispi2lem2  46424  wallispi2  46425  stirlinglem1  46426  stirlinglem3  46428  stirlinglem5  46430  stirlinglem6  46431  stirlinglem7  46432  stirlinglem8  46433  stirlinglem10  46435  stirlinglem11  46436  stirlinglem12  46437  stirlinglem13  46438  stirlinglem15  46440  dirker2re  46444  dirkerval2  46446  dirkerre  46447  dirkertrigeqlem1  46450  dirkertrigeqlem3  46452  dirkeritg  46454  dirkercncflem1  46455  dirkercncflem2  46456  dirkercncflem4  46458  fourierdlem5  46464  fourierdlem6  46465  fourierdlem11  46470  fourierdlem15  46474  fourierdlem19  46478  fourierdlem20  46479  fourierdlem24  46483  fourierdlem26  46485  fourierdlem28  46487  fourierdlem30  46489  fourierdlem39  46498  fourierdlem41  46500  fourierdlem43  46502  fourierdlem47  46505  fourierdlem48  46506  fourierdlem56  46514  fourierdlem60  46518  fourierdlem61  46519  fourierdlem62  46520  fourierdlem64  46522  fourierdlem65  46523  fourierdlem66  46524  fourierdlem68  46526  fourierdlem73  46531  fourierdlem78  46536  fourierdlem79  46537  fourierdlem87  46545  fourierdlem103  46561  fourierdlem104  46562  sqwvfoura  46580  fouriersw  46583  etransclem4  46590  etransclem23  46609  etransclem24  46610  etransclem31  46617  etransclem32  46618  etransclem35  46621  etransclem41  46627  etransclem46  46632  etransclem48  46634  etransc  46635  ioorrnopnxrlem  46658  nnfoctbdjlem  46807  iundjiun  46812  hoidmvlelem1  46947  hoidmvlelem2  46948  hoidmvlelem3  46949  hoidmvlelem4  46950  ovnhoilem1  46953  vonioolem2  47033  vonicclem2  47036  pimrecltneg  47076  smfrec  47141  smfmullem1  47143  smfmullem2  47144  smfdiv  47149  sigaradd  47218  ormkglobd  47227  cjnpoly  47243  p1lep2  47654  zm1nn  47656  ceilhalfgt1  47683  2tceilhalfelfzo1  47686  ceilbi  47687  rehalfge1  47689  ceilhalfnn  47690  addmodne  47698  m1mod0mod1  47708  m1modmmod  47712  difmodm1lt  47713  modmknepk  47716  modp2nep1  47721  modm1nem2  47723  iccpartiltu  47776  iccpartlt  47778  iccpartgt  47781  fmtnoge3  47884  fmtnodvds  47898  fmtnoprmfac2lem1  47920  2pwp1prm  47943  flsqrt  47947  sfprmdvdsmersenne  47957  lighneallem2  47960  lighneallem4a  47962  proththdlem  47967  proththd  47968  nnoALTV  48049  bgoldbtbndlem4  48162  gpgprismgrusgra  48412  gpgedgvtx0  48415  gpgvtxedg0  48417  gpg5nbgrvtx03starlem2  48423  gpg3kgrtriexlem4  48440  gpg3kgrtriexlem6  48442  cznnring  48616  divge1b  48866  divgt1b  48867  nn0eo  48882  regt1loggt0  48890  rege1logbrege0  48912  logblt1b  48918  fllog2  48922  nnolog2flm1  48944  dignn0flhalflem1  48969  rrxlinesc  49089  rrxlinec  49090  eenglngeehlnmlem1  49091  eenglngeehlnmlem2  49092  line2ylem  49105  line2  49106  line2xlem  49107  reseccl  50106  recsccl  50107  amgmwlem  50155  amgmlemALT  50156