Theorem 1red 11197

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

Syntax hints:   → wi 4   ∈ wcel 2145  ℝcr 11087  1c1 11089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-1cn 11146  ax-icn 11147  ax-addcl 11148  ax-mulcl 11150  ax-mulrcl 11151  ax-i2m1 11156  ax-1ne0 11157  ax-rrecex 11160  ax-cnre 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403

This theorem is referenced by:  recgt0  12052  mulgt1  12067  ltrec  12088  nnne0  12261  nn0p1gt0  12524  nn0ge2m1nn  12565  nn0le2is012  12651  suprzcl  12667  ledivge1le  13080  ge2halflem1  13124  qbtwnre  13216  lincmb01cmp  13513  iccf1o  13514  xov1plusxeqvd  13516  zltaddlt1le  13523  nnge2recico01  13525  fznatpl1  13597  elfz1b  13612  elfzo0subge1  13725  fzonn0p1p1  13764  elfznelfzo  13793  elfznelfzob  13794  fladdz  13849  2tnp1ge0ge0  13853  flhalf  13854  ltdifltdiv  13858  fldiv4lem1div2uz2  13860  mulp1mod1  13938  m1modge3gt1  13945  modltm1p1mod  13950  addmodlteq  13973  ltexp2a  14193  expcan  14196  ltexp2  14197  leexp2  14198  leexp2a  14199  leexp2r  14201  nnlesq  14232  bernneq3  14258  expnbnd  14259  expnlbnd2  14261  expnngt1  14268  fzsdom2  14455  wrdlenge2n0  14579  swrd2lsw  14979  2swrd2eqwrdeq  14980  01sqrexlem7  15289  rddif  15382  reccn2  15638  rlimo1  15658  o1fsum  15855  abscvgcvg  15861  climcndslem1  15893  flo1  15898  harmonic  15903  geomulcvg  15920  fprodrecl  15997  fprodreclf  16003  fprodle  16040  bpoly4  16103  efcllem  16121  efgt1  16162  tanhlt1  16206  sinltx  16235  eirrlem  16250  p1modz1  16307  mod2eq1n2dvds  16395  oddge22np1  16397  ltoddhalfle  16409  nn0o1gt2  16429  nno  16430  nn0oddm1d2  16433  nnoddm1d2  16434  bitsfzolem  16482  bitsfzo  16483  bitsmod  16484  bitscmp  16486  bitsinv1lem  16489  smuval2  16530  coprmgcdb  16697  prmind2  16733  dvdsnprmd  16738  2mulprm  16741  isprm5  16756  isprm7  16757  divdenle  16798  zsqrtelqelz  16807  fermltl  16833  odzdvds  16845  modprm0  16855  iserodd  16885  difsqpwdvds  16937  pcfaclem  16948  prmreclem1  16966  4sqlem11  17005  4sqlem12  17006  ramub1lem1  17076  prmgaplem8  17108  2expltfac  17142  chnccat  18672  pgpfaclem2  20145  qsidomlem1  21440  znidomb  21671  psdmvr  22292  chfacfisf  22972  chfacfisfcpmat  22973  chfacfscmulgsum  22978  chfacfpmmulgsum  22982  nrginvrcnlem  24809  nmoid  24860  xrsmopn  24931  metnrmlem1a  24977  iihalf2cn  25054  iccpnfhmeo  25065  lebnumii  25086  htpycc  25100  pcohtpylem  25139  pcoass  25144  pcorevlem  25146  nmhmcn  25240  cncmet  25442  ovoliunlem1  25622  dyadmaxlem  25717  vitalilem2  25729  mbfi1fseqlem6  25840  itg2mulc  25867  itg2monolem1  25870  itg2monolem3  25872  dveflem  26099  mvth  26112  dvlipcn  26114  lhop1lem  26133  dvfsumlem1  26146  dvfsumlem2  26147  dvfsumlem3  26148  dvfsumlem4  26149  dvfsum2  26154  fta1glem2  26287  plyeq0lem  26328  fta1lem  26429  vieta1lem2  26433  aalioulem3  26456  aalioulem4  26457  radcnvlem1  26534  radcnvlem2  26535  dvradcnv  26542  abelthlem2  26553  abelthlem5  26556  abelthlem7  26559  abelth2  26563  cos02pilt1  26649  cosne0  26652  rplogcl  26727  logdivlti  26743  logno1  26759  dvlog2lem  26775  advlog  26777  logtayllem  26782  cxplt  26817  cxple  26818  cxpaddlelem  26874  cxpaddle  26875  rtprmirr  26883  relogbf  26914  logbgt0b  26916  isosctrlem1  26941  isosctrlem2  26942  chordthmlem4  26958  heron  26961  atanlogaddlem  27036  bndatandm  27052  leibpi  27065  log2tlbnd  27068  birthdaylem3  27076  rlimcnp  27088  rlimcnp2  27089  efrlim  27092  cxp2limlem  27098  cxp2lim  27099  divsqrtsumo1  27106  jensenlem2  27110  logdiflbnd  27117  fsumharmonic  27134  lgamgulmlem2  27152  lgamgulmlem3  27153  lgamgulmlem4  27154  lgamgulmlem5  27155  lgamgulmlem6  27156  lgamcvg2  27177  regamcl  27183  wilthlem2  27191  ftalem2  27196  basellem9  27211  vma1  27288  ppieq0  27298  mumullem2  27302  fsumfldivdiaglem  27311  chpeq0  27330  chtub  27334  chpval2  27340  chpchtsum  27341  chpub  27342  logfacrlim  27346  logexprlim  27347  mersenne  27349  perfectlem2  27352  dchrelbas4  27365  bcmono  27399  bposlem1  27406  bposlem2  27407  zabsle1  27418  lgslem3  27421  lgsmod  27445  lgsdir2lem4  27450  lgsdirprm  27453  gausslemma2dlem1a  27487  gausslemma2d  27496  lgsquadlem2  27503  2sqlem8  27548  chebbnd1lem1  27591  chebbnd1lem2  27592  chtppilimlem1  27595  chebbnd2  27599  chto1lb  27600  chpchtlim  27601  chpo1ubb  27603  vmadivsum  27604  rplogsumlem1  27606  rpvmasumlem  27609  dchrisumlem3  27613  dchrmusumlema  27615  dchrmusum2  27616  dchrvmasumlem2  27620  dchrvmasumlem3  27621  dchrvmasumiflem1  27623  dchrvmasumiflem2  27624  dchrisum0flblem1  27630  dchrisum0flblem2  27631  dchrisum0fno1  27633  dchrisum0re  27635  dchrisum0lema  27636  dchrisum0lem1b  27637  dchrisum0lem2a  27639  dchrisum0lem2  27640  dchrisum0lem3  27641  rplogsum  27649  dirith2  27650  mudivsum  27652  mulogsumlem  27653  mulogsum  27654  mulog2sumlem1  27656  mulog2sumlem2  27657  vmalogdivsum2  27660  vmalogdivsum  27661  2vmadivsumlem  27662  log2sumbnd  27666  selberglem2  27668  selberg2lem  27672  chpdifbnd  27677  selberg3lem1  27679  selberg3  27681  selberg4lem1  27682  selberg4  27683  pntrmax  27686  pntrsumo1  27687  pntrsumbnd  27688  selberg3r  27691  selberg4r  27692  selberg34r  27693  pntrlog2bndlem1  27699  pntrlog2bndlem2  27700  pntrlog2bndlem3  27701  pntrlog2bndlem4  27702  pntrlog2bndlem5  27703  pntrlog2bndlem6  27705  pntrlog2bnd  27706  pntpbnd1a  27707  pntpbnd1  27708  pntibndlem2a  27712  pntibndlem2  27713  pntibnd  27715  pntlemc  27717  pntlemg  27720  pntlemr  27724  pntlemk  27728  pnt  27736  qabvle  27747  ostth2lem3  27757  ostth2  27759  trgcgrg  28742  tgcgr4  28758  ttgcontlem1  29143  axpaschlem  29199  axlowdimlem16  29216  axcontlem2  29224  axcontlem7  29229  nbusgrvtxm1  29638  upgrewlkle2  29865  pthdlem1  30024  crctcshwlkn0lem3  30070  crctcshwlkn0lem5  30072  wwlksm1edg  30139  wwlksnextproplem2  30168  clwlkclwwlklem2fv1  30255  clwlkclwwlklem2fv2  30256  clwlkclwwlklem2  30260  clwlkclwwlk2  30263  clwwisshclwwslem  30274  clwwlkf1  30309  clwwlkext2edg  30316  clwlknf1oclwwlknlem1  30341  clwwlknonex2lem2  30368  numclwwlk7  30651  frgrreggt1  30653  frgrogt3nreg  30657  smcnlem  30958  nmoub3i  31034  blocnilem  31065  ubthlem2  31132  minvecolem4  31141  htthlem  31178  nmcexi  32287  nmopcoi  32356  stadd3i  32509  cdj1i  32694  nnmulge  32996  receqid  33001  nndiffz1  33043  fzsplit3  33050  nexple  33090  indf1o  33097  wrdt2ind  33186  pmtrto1cl  33332  fzto1st1  33335  fzto1st  33336  psgnfzto1st  33338  cycpmco2lem6  33364  cycpmco2lem7  33365  cycpmrn  33376  krull  33678  ply1degltel  33801  ply1degltlss  33803  constrnegcl  34070  constrdircl  34072  iconstr  34073  constrrecl  34076  constrmulcl  34078  constrreinvcl  34079  constrresqrtcl  34084  cos9thpiminplylem1  34089  cos9thpiminply  34095  cos9thpinconstrlem1  34096  1smat1  34111  submateqlem1  34114  madjusmdetlem2  34135  unitdivcld  34208  sqsscirc1  34215  esumdivc  34390  dya2ub  34577  dya2iocress  34581  dya2iocbrsiga  34582  dya2icobrsiga  34583  dya2icoseg  34584  dya2iocucvr  34591  sxbrsigalem2  34593  fibp1  34708  probmeasb  34737  dstrvprob  34779  dstfrvunirn  34782  ballotlemfc0  34800  ballotlemfcc  34801  ballotlemsgt1  34818  ballotlemsel1i  34820  ballotlemfrcn0  34837  signsply0  34855  itgexpif  34910  reprlt  34923  chtvalz  34933  breprexplemc  34936  breprexp  34937  circlemeth  34944  tgoldbachgnn  34963  acycgr1v  35512  subfaclim  35551  cvmliftlem2  35649  cvmliftlem13  35659  snmlff  35692  bccolsum  36102  faclim  36109  nn0prpwlem  36695  dnibndlem10  36938  dnibndlem12  36940  knoppcnlem4  36947  unblimceq0  36958  knoppndvlem1  36963  knoppndvlem2  36964  knoppndvlem3  36965  knoppndvlem7  36969  knoppndvlem11  36973  knoppndvlem12  36974  knoppndvlem14  36976  knoppndvlem15  36977  knoppndvlem17  36979  knoppndvlem18  36980  knoppndvlem20  36982  irrdiff  37830  poimirlem6  38137  poimirlem7  38138  poimirlem15  38146  poimirlem19  38150  poimirlem29  38160  poimirlem30  38161  poimirlem31  38162  poimirlem32  38163  broucube  38165  itg2addnclem2  38183  itg2addnclem3  38184  areacirclem1  38219  areacirclem4  38222  incsequz  38259  totbndbnd  38300  bfplem2  38334  resdvopclptsd  42657  lcmineqlem2  42659  lcmineqlem3  42660  lcmineqlem10  42667  lcmineqlem12  42669  lcmineqlem15  42672  lcmineqlem18  42675  lcmineqlem19  42676  lcmineqlem20  42677  lcmineqlem22  42679  lcmineqlem23  42680  3lexlogpow5ineq2  42684  3lexlogpow5ineq4  42685  3lexlogpow5ineq3  42686  3lexlogpow2ineq1  42687  3lexlogpow2ineq2  42688  3lexlogpow5ineq5  42689  aks4d1lem1  42691  dvrelog2  42693  dvrelog3  42694  dvrelog2b  42695  dvrelogpow2b  42697  aks4d1p1p3  42698  aks4d1p1p2  42699  aks4d1p1p4  42700  aks4d1p1p6  42702  aks4d1p1p7  42703  aks4d1p1p5  42704  aks4d1p1  42705  aks4d1p2  42706  aks4d1p3  42707  aks4d1p5  42709  aks4d1p6  42710  aks4d1p7d1  42711  aks4d1p7  42712  aks4d1p8d2  42714  aks4d1p8d3  42715  aks4d1p8  42716  aks4d1p9  42717  posbezout  42729  primrootlekpowne0  42734  primrootspoweq0  42735  aks6d1c1  42745  aks6d1c2p2  42748  hashscontpow1  42750  aks6d1c3  42752  aks6d1c2lem4  42756  aks6d1c2  42759  2np3bcnp1  42773  2ap1caineq  42774  sticksstones6  42780  sticksstones7  42781  sticksstones10  42784  sticksstones12a  42786  sticksstones12  42787  sticksstones22  42797  aks6d1c6lem3  42801  aks6d1c6lem4  42802  bcled  42807  bcle2d  42808  aks6d1c7lem1  42809  aks6d1c7lem2  42810  unitscyglem2  42825  unitscyglem4  42827  unitscyglem5  42828  aks5lem8  42830  sn-1ne2  42892  redvmptabs  42981  sn-00idlem2  43020  sn-0ne2  43027  rei4  43045  rediveq1d  43072  sn-rediv1d  43073  sn-rereccld  43076  rerecne0d  43077  rerecidd  43078  rerecrecd  43080  sn-0tie0  43085  sn-nnne0  43094  mulgt0b1d  43106  sn-ltmulgt11d  43108  sn-0lt1  43109  sn-mulgt1d  43113  fimgmcyc  43164  flt4lem7  43253  fltnlta  43257  3cubeslem1  43277  3cubeslem3r  43280  3cubeslem4  43282  lzenom  43363  irrapxlem1  43411  irrapxlem2  43412  irrapxlem4  43414  irrapxlem5  43415  pellexlem2  43419  pell1qrge1  43459  pell1qr1  43460  elpell1qr2  43461  pell14qrgapw  43465  pellfundgt1  43472  pellfundglb  43474  pellfundex  43475  pellfundrp  43477  pellfundne1  43478  rmspecsqrtnq  43495  rmspecnonsq  43496  rmspecfund  43498  rmspecpos  43505  monotoddzzfi  43531  rmygeid  43553  areaquad  43805  imo72b2lem0  44753  imo72b2lem1  44757  imo72b2  44760  cvgdvgrat  44887  radcnvrat  44888  hashnzfzclim  44896  lhe4.4ex1a  44903  binomcxplemnn0  44923  binomcxplemdvbinom  44927  binomcxplemnotnn0  44930  oddfl  45855  abscosbd  45856  zltlesub  45862  abssinbd  45872  monoords  45874  fzisoeu  45877  fzdifsuc2  45887  suplesup  45913  xralrple2  45928  infxr  45940  infleinflem2  45944  reclt0d  45960  xrralrecnnge  45963  sqrlearg  46127  iooiinioc  46130  fmul01  46154  fmul01lt1lem1  46158  fmul01lt1lem2  46159  climsuselem1  46181  sumnnodd  46204  0ellimcdiv  46221  dvmptidg  46489  dvcosax  46498  ioodvbdlimc1lem1  46503  ioodvbdlimc1lem2  46504  ioodvbdlimc2lem  46506  dvxpaek  46512  dvnmul  46515  iblspltprt  46545  itgspltprt  46551  stoweidlem5  46577  stoweidlem7  46579  stoweidlem10  46582  stoweidlem11  46583  stoweidlem12  46584  stoweidlem13  46585  stoweidlem14  46586  stoweidlem16  46588  stoweidlem18  46590  stoweidlem20  46592  stoweidlem24  46596  stoweidlem25  46597  stoweidlem34  46606  stoweidlem36  46608  stoweidlem38  46610  stoweidlem40  46612  stoweidlem41  46613  stoweidlem42  46614  stoweidlem45  46617  stoweidlem51  46623  stoweidlem60  46632  wallispilem3  46639  wallispilem4  46640  wallispilem5  46641  wallispi  46642  wallispi2lem1  46643  wallispi2lem2  46644  wallispi2  46645  stirlinglem1  46646  stirlinglem3  46648  stirlinglem5  46650  stirlinglem6  46651  stirlinglem7  46652  stirlinglem8  46653  stirlinglem10  46655  stirlinglem11  46656  stirlinglem12  46657  stirlinglem13  46658  stirlinglem15  46660  dirker2re  46664  dirkerval2  46666  dirkerre  46667  dirkertrigeqlem1  46670  dirkertrigeqlem3  46672  dirkeritg  46674  dirkercncflem1  46675  dirkercncflem2  46676  dirkercncflem4  46678  fourierdlem5  46684  fourierdlem6  46685  fourierdlem11  46690  fourierdlem15  46694  fourierdlem19  46698  fourierdlem20  46699  fourierdlem24  46703  fourierdlem26  46705  fourierdlem28  46707  fourierdlem30  46709  fourierdlem39  46718  fourierdlem41  46720  fourierdlem43  46722  fourierdlem47  46725  fourierdlem48  46726  fourierdlem56  46734  fourierdlem60  46738  fourierdlem61  46739  fourierdlem62  46740  fourierdlem64  46742  fourierdlem65  46743  fourierdlem66  46744  fourierdlem68  46746  fourierdlem73  46751  fourierdlem78  46756  fourierdlem79  46757  fourierdlem87  46765  fourierdlem103  46781  fourierdlem104  46782  sqwvfoura  46800  fouriersw  46803  etransclem4  46810  etransclem23  46829  etransclem24  46830  etransclem31  46837  etransclem32  46838  etransclem35  46841  etransclem41  46847  etransclem46  46852  etransclem48  46854  etransc  46855  ioorrnopnxrlem  46878  nnfoctbdjlem  47027  iundjiun  47032  hoidmvlelem1  47167  hoidmvlelem2  47168  hoidmvlelem3  47169  hoidmvlelem4  47170  ovnhoilem1  47173  vonioolem2  47253  vonicclem2  47256  pimrecltneg  47296  smfrec  47361  smfmullem1  47363  smfmullem2  47364  smfdiv  47369  sigaradd  47438  ormkglobd  47449  cjnpoly  47481  p1lep2  47892  zm1nn  47894  ceilhalfgt1  47925  2tceilhalfelfzo1  47928  ceilbi  47929  rehalfge1  47931  ceilhalfnn  47932  flmrecm1  47935  addmodne  47942  m1mod0mod1  47952  m1modmmod  47956  difmodm1lt  47957  modmknepk  47960  modp2nep1  47965  modm1nem2  47967  2timesltsqm1  47971  muldvdsfacm1  47979  iccpartiltu  48026  iccpartlt  48028  iccpartgt  48031  fmtnoge3  48137  fmtnodvds  48151  fmtnoprmfac2lem1  48173  2pwp1prm  48196  flsqrt  48200  sfprmdvdsmersenne  48210  lighneallem2  48213  lighneallem4a  48215  proththdlem  48220  proththd  48221  nprmdvdsfacm1lem4  48230  nnoALTV  48315  bgoldbtbndlem4  48428  gpgprismgrusgra  48678  gpgedgvtx0  48681  gpgvtxedg0  48683  gpg5nbgrvtx03starlem2  48689  gpg3kgrtriexlem4  48706  gpg3kgrtriexlem6  48708  cznnring  48882  divge1b  49143  divgt1b  49144  nn0eo  49159  regt1loggt0  49167  rege1logbrege0  49189  logblt1b  49195  fllog2  49199  nnolog2flm1  49221  dignn0flhalflem1  49246  rrxlinesc  49366  rrxlinec  49367  eenglngeehlnmlem1  49368  eenglngeehlnmlem2  49369  line2ylem  49382  line2  49383  line2xlem  49384  reseccl  50382  recsccl  50383  amgmwlem  50431  amgmlemALT  50432