Theorem 1red 11175

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℝcr 11067  1c1 11069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  recgt0  12028  mulgt1  12044  ltrec  12065  nnne0  12220  nn0p1gt0  12471  nn0ge2m1nn  12512  nn0le2is012  12598  suprzcl  12614  ledivge1le  13024  ge2halflem1  13068  qbtwnre  13159  lincmb01cmp  13456  iccf1o  13457  xov1plusxeqvd  13459  zltaddlt1le  13466  fznatpl1  13539  elfz1b  13554  elfzo0subge1  13666  fzonn0p1p1  13705  elfznelfzo  13733  elfznelfzob  13734  fladdz  13787  2tnp1ge0ge0  13791  flhalf  13792  ltdifltdiv  13796  fldiv4lem1div2uz2  13798  mulp1mod1  13876  m1modge3gt1  13883  modltm1p1mod  13888  addmodlteq  13911  ltexp2a  14131  expcan  14134  ltexp2  14135  leexp2  14136  leexp2a  14137  leexp2r  14139  nnlesq  14170  bernneq3  14196  expnbnd  14197  expnlbnd2  14199  expnngt1  14206  fzsdom2  14393  wrdlenge2n0  14517  swrd2lsw  14918  2swrd2eqwrdeq  14919  01sqrexlem7  15214  rddif  15307  reccn2  15563  rlimo1  15583  o1fsum  15779  abscvgcvg  15785  climcndslem1  15815  flo1  15820  harmonic  15825  geomulcvg  15842  fprodrecl  15919  fprodreclf  15925  fprodle  15962  bpoly4  16025  efcllem  16043  efgt1  16084  tanhlt1  16128  sinltx  16157  eirrlem  16172  p1modz1  16229  mod2eq1n2dvds  16317  oddge22np1  16319  ltoddhalfle  16331  nn0o1gt2  16351  nno  16352  nn0oddm1d2  16355  nnoddm1d2  16356  bitsfzolem  16404  bitsfzo  16405  bitsmod  16406  bitscmp  16408  bitsinv1lem  16411  smuval2  16452  coprmgcdb  16619  prmind2  16655  dvdsnprmd  16660  2mulprm  16663  isprm5  16677  isprm7  16678  divdenle  16719  zsqrtelqelz  16728  fermltl  16754  odzdvds  16766  modprm0  16776  iserodd  16806  difsqpwdvds  16858  pcfaclem  16869  prmreclem1  16887  4sqlem11  16926  4sqlem12  16927  ramub1lem1  16997  prmgaplem8  17029  2expltfac  17063  pgpfaclem2  20014  znidomb  21471  psdmvr  22056  chfacfisf  22741  chfacfisfcpmat  22742  chfacfscmulgsum  22747  chfacfpmmulgsum  22751  nrginvrcnlem  24579  nmoid  24630  xrsmopn  24701  metnrmlem1a  24747  iihalf2cn  24829  iccpnfhmeo  24843  lebnumii  24865  htpycc  24879  pcohtpylem  24919  pcoass  24924  pcorevlem  24926  nmhmcn  25020  cncmet  25222  ovoliunlem1  25403  dyadmaxlem  25498  vitalilem2  25510  mbfi1fseqlem6  25621  itg2mulc  25648  itg2monolem1  25651  itg2monolem3  25653  dveflem  25883  mvth  25897  dvlipcn  25899  lhop1lem  25918  dvfsumlem1  25932  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem3  25935  dvfsumlem4  25936  dvfsum2  25941  fta1glem2  26074  plyeq0lem  26115  fta1lem  26215  vieta1lem2  26219  aalioulem3  26242  aalioulem4  26243  radcnvlem1  26322  radcnvlem2  26323  dvradcnv  26330  abelthlem2  26342  abelthlem5  26345  abelthlem7  26348  abelth2  26352  cos02pilt1  26435  cosne0  26438  rplogcl  26513  logdivlti  26529  logno1  26545  dvlog2lem  26561  advlog  26563  logtayllem  26568  cxplt  26603  cxple  26604  cxpaddlelem  26661  cxpaddle  26662  rtprmirr  26670  relogbf  26701  logbgt0b  26703  isosctrlem1  26728  isosctrlem2  26729  chordthmlem4  26745  heron  26748  atanlogaddlem  26823  bndatandm  26839  leibpi  26852  log2tlbnd  26855  birthdaylem3  26863  rlimcnp  26875  rlimcnp2  26876  efrlim  26879  efrlimOLD  26880  cxp2limlem  26886  cxp2lim  26887  divsqrtsumo1  26894  jensenlem2  26898  logdiflbnd  26905  fsumharmonic  26922  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamgulmlem4  26942  lgamgulmlem5  26943  lgamgulmlem6  26944  lgamcvg2  26965  regamcl  26971  wilthlem2  26979  ftalem2  26984  basellem9  26999  vma1  27076  ppieq0  27086  mumullem2  27090  fsumfldivdiaglem  27099  chpeq0  27119  chtub  27123  chpval2  27129  chpchtsum  27130  chpub  27131  logfacrlim  27135  logexprlim  27136  mersenne  27138  perfectlem2  27141  dchrelbas4  27154  bcmono  27188  bposlem1  27195  bposlem2  27196  zabsle1  27207  lgslem3  27210  lgsmod  27234  lgsdir2lem4  27239  lgsdirprm  27242  gausslemma2dlem1a  27276  gausslemma2d  27285  lgsquadlem2  27292  2sqlem8  27337  chebbnd1lem1  27380  chebbnd1lem2  27381  chtppilimlem1  27384  chebbnd2  27388  chto1lb  27389  chpchtlim  27390  chpo1ubb  27392  vmadivsum  27393  rplogsumlem1  27395  rpvmasumlem  27398  dchrisumlem3  27402  dchrmusumlema  27404  dchrmusum2  27405  dchrvmasumlem2  27409  dchrvmasumlem3  27410  dchrvmasumiflem1  27412  dchrvmasumiflem2  27413  dchrisum0flblem1  27419  dchrisum0flblem2  27420  dchrisum0fno1  27422  dchrisum0re  27424  dchrisum0lema  27425  dchrisum0lem1b  27426  dchrisum0lem2a  27428  dchrisum0lem2  27429  dchrisum0lem3  27430  rplogsum  27438  dirith2  27439  mudivsum  27441  mulogsumlem  27442  mulogsum  27443  mulog2sumlem1  27445  mulog2sumlem2  27446  vmalogdivsum2  27449  vmalogdivsum  27450  2vmadivsumlem  27451  log2sumbnd  27455  selberglem2  27457  selberg2lem  27461  chpdifbnd  27466  selberg3lem1  27468  selberg3  27470  selberg4lem1  27471  selberg4  27472  pntrmax  27475  pntrsumo1  27476  pntrsumbnd  27477  selberg3r  27480  selberg4r  27481  selberg34r  27482  pntrlog2bndlem1  27488  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem4  27491  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntrlog2bnd  27495  pntpbnd1a  27496  pntpbnd1  27497  pntibndlem2a  27501  pntibndlem2  27502  pntibnd  27504  pntlemc  27506  pntlemg  27509  pntlemr  27513  pntlemk  27517  pnt  27525  qabvle  27536  ostth2lem3  27546  ostth2  27548  trgcgrg  28442  tgcgr4  28458  ttgcontlem1  28812  axpaschlem  28867  axlowdimlem16  28884  axcontlem2  28892  axcontlem7  28897  nbusgrvtxm1  29306  upgrewlkle2  29534  pthdlem1  29696  crctcshwlkn0lem3  29742  crctcshwlkn0lem5  29744  wwlksm1edg  29811  wwlksnextproplem2  29840  clwlkclwwlklem2fv1  29924  clwlkclwwlklem2fv2  29925  clwlkclwwlklem2  29929  clwlkclwwlk2  29932  clwwisshclwwslem  29943  clwwlkf1  29978  clwwlkext2edg  29985  clwlknf1oclwwlknlem1  30010  clwwlknonex2lem2  30037  numclwwlk7  30320  frgrreggt1  30322  frgrogt3nreg  30326  smcnlem  30626  nmoub3i  30702  blocnilem  30733  ubthlem2  30800  minvecolem4  30809  htthlem  30846  nmcexi  31955  nmopcoi  32024  stadd3i  32177  cdj1i  32362  nnmulge  32662  receqid  32668  nndiffz1  32709  fzsplit3  32716  nexple  32769  indf1o  32787  wrdt2ind  32875  pmtrto1cl  33056  fzto1st1  33059  fzto1st  33060  psgnfzto1st  33062  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmrn  33100  qsidomlem1  33423  krull  33450  ply1degltel  33560  ply1degltlss  33562  constrnegcl  33753  constrdircl  33755  iconstr  33756  constrrecl  33759  constrmulcl  33761  constrreinvcl  33762  constrresqrtcl  33767  cos9thpiminplylem1  33772  cos9thpiminply  33778  cos9thpinconstrlem1  33779  1smat1  33794  submateqlem1  33797  madjusmdetlem2  33818  unitdivcld  33891  sqsscirc1  33898  esumdivc  34073  dya2ub  34261  dya2iocress  34265  dya2iocbrsiga  34266  dya2icobrsiga  34267  dya2icoseg  34268  dya2iocucvr  34275  sxbrsigalem2  34277  fibp1  34392  probmeasb  34421  dstrvprob  34463  dstfrvunirn  34466  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemsgt1  34502  ballotlemsel1i  34504  ballotlemfrcn0  34521  signsply0  34542  itgexpif  34597  reprlt  34610  chtvalz  34620  breprexplemc  34623  breprexp  34624  circlemeth  34631  tgoldbachgnn  34650  acycgr1v  35136  subfaclim  35175  cvmliftlem2  35273  cvmliftlem13  35283  snmlff  35316  bccolsum  35726  faclim  35733  nn0prpwlem  36310  dnibndlem10  36475  dnibndlem12  36477  knoppcnlem4  36484  unblimceq0  36495  knoppndvlem1  36500  knoppndvlem2  36501  knoppndvlem3  36502  knoppndvlem7  36506  knoppndvlem11  36510  knoppndvlem12  36511  knoppndvlem14  36513  knoppndvlem15  36514  knoppndvlem17  36516  knoppndvlem18  36517  knoppndvlem20  36519  irrdiff  37314  poimirlem6  37620  poimirlem7  37621  poimirlem15  37629  poimirlem19  37633  poimirlem29  37643  poimirlem30  37644  poimirlem31  37645  poimirlem32  37646  broucube  37648  itg2addnclem2  37666  itg2addnclem3  37667  areacirclem1  37702  areacirclem4  37705  incsequz  37742  totbndbnd  37783  bfplem2  37817  resdvopclptsd  42016  lcmineqlem2  42018  lcmineqlem3  42019  lcmineqlem10  42026  lcmineqlem12  42028  lcmineqlem15  42031  lcmineqlem18  42034  lcmineqlem19  42035  lcmineqlem20  42036  lcmineqlem22  42038  lcmineqlem23  42039  3lexlogpow5ineq2  42043  3lexlogpow5ineq4  42044  3lexlogpow5ineq3  42045  3lexlogpow2ineq1  42046  3lexlogpow2ineq2  42047  3lexlogpow5ineq5  42048  aks4d1lem1  42050  dvrelog2  42052  dvrelog3  42053  dvrelog2b  42054  dvrelogpow2b  42056  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p2  42065  aks4d1p3  42066  aks4d1p5  42068  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8d2  42073  aks4d1p8d3  42074  aks4d1p8  42075  aks4d1p9  42076  posbezout  42088  primrootlekpowne0  42093  primrootspoweq0  42094  aks6d1c1  42104  aks6d1c2p2  42107  hashscontpow1  42109  aks6d1c3  42111  aks6d1c2lem4  42115  aks6d1c2  42118  2np3bcnp1  42132  2ap1caineq  42133  sticksstones6  42139  sticksstones7  42140  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  sticksstones22  42156  aks6d1c6lem3  42160  aks6d1c6lem4  42161  bcled  42166  bcle2d  42167  aks6d1c7lem1  42168  aks6d1c7lem2  42169  unitscyglem2  42184  unitscyglem4  42186  unitscyglem5  42187  aks5lem8  42189  sn-1ne2  42253  redvmptabs  42348  sn-00idlem2  42387  sn-0ne2  42394  rei4  42412  sn-rereccld  42436  rerecid  42437  sn-0tie0  42439  sn-nnne0  42448  mulgt0b1d  42460  sn-ltmulgt11d  42462  sn-0lt1  42463  sn-mulgt1d  42467  fimgmcyc  42522  flt4lem7  42647  fltnlta  42651  3cubeslem1  42672  3cubeslem3r  42675  3cubeslem4  42677  lzenom  42758  irrapxlem1  42810  irrapxlem2  42811  irrapxlem4  42813  irrapxlem5  42814  pellexlem2  42818  pell1qrge1  42858  pell1qr1  42859  elpell1qr2  42860  pell14qrgapw  42864  pellfundgt1  42871  pellfundglb  42873  pellfundex  42874  pellfundrp  42876  pellfundne1  42877  rmspecsqrtnq  42894  rmspecnonsq  42895  rmspecfund  42897  rmspecpos  42905  monotoddzzfi  42931  rmygeid  42953  areaquad  43205  imo72b2lem0  44154  imo72b2lem1  44158  imo72b2  44161  cvgdvgrat  44302  radcnvrat  44303  hashnzfzclim  44311  lhe4.4ex1a  44318  binomcxplemnn0  44338  binomcxplemdvbinom  44342  binomcxplemnotnn0  44345  oddfl  45276  abscosbd  45277  zltlesub  45283  abssinbd  45293  monoords  45295  fzisoeu  45298  fzdifsuc2  45308  suplesup  45335  xralrple2  45350  infxr  45363  infleinflem2  45367  reclt0d  45383  xrralrecnnge  45386  sqrlearg  45551  iooiinioc  45554  fmul01  45578  fmul01lt1lem1  45582  fmul01lt1lem2  45583  climsuselem1  45605  sumnnodd  45628  0ellimcdiv  45647  dvmptidg  45915  dvcosax  45924  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvxpaek  45938  dvnmul  45941  iblspltprt  45971  itgspltprt  45977  stoweidlem5  46003  stoweidlem7  46005  stoweidlem10  46008  stoweidlem11  46009  stoweidlem12  46010  stoweidlem13  46011  stoweidlem14  46012  stoweidlem16  46014  stoweidlem18  46016  stoweidlem20  46018  stoweidlem24  46022  stoweidlem25  46023  stoweidlem34  46032  stoweidlem36  46034  stoweidlem38  46036  stoweidlem40  46038  stoweidlem41  46039  stoweidlem42  46040  stoweidlem45  46043  stoweidlem51  46049  stoweidlem60  46058  wallispilem3  46065  wallispilem4  46066  wallispilem5  46067  wallispi  46068  wallispi2lem1  46069  wallispi2lem2  46070  wallispi2  46071  stirlinglem1  46072  stirlinglem3  46074  stirlinglem5  46076  stirlinglem6  46077  stirlinglem7  46078  stirlinglem8  46079  stirlinglem10  46081  stirlinglem11  46082  stirlinglem12  46083  stirlinglem13  46084  stirlinglem15  46086  dirker2re  46090  dirkerval2  46092  dirkerre  46093  dirkertrigeqlem1  46096  dirkertrigeqlem3  46098  dirkeritg  46100  dirkercncflem1  46101  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem5  46110  fourierdlem6  46111  fourierdlem11  46116  fourierdlem15  46120  fourierdlem19  46124  fourierdlem20  46125  fourierdlem24  46129  fourierdlem26  46131  fourierdlem28  46133  fourierdlem30  46135  fourierdlem39  46144  fourierdlem41  46146  fourierdlem43  46148  fourierdlem47  46151  fourierdlem48  46152  fourierdlem56  46160  fourierdlem60  46164  fourierdlem61  46165  fourierdlem62  46166  fourierdlem64  46168  fourierdlem65  46169  fourierdlem66  46170  fourierdlem68  46172  fourierdlem73  46177  fourierdlem78  46182  fourierdlem79  46183  fourierdlem87  46191  fourierdlem103  46207  fourierdlem104  46208  sqwvfoura  46226  fouriersw  46229  etransclem4  46236  etransclem23  46255  etransclem24  46256  etransclem31  46263  etransclem32  46264  etransclem35  46267  etransclem41  46273  etransclem46  46278  etransclem48  46280  etransc  46281  ioorrnopnxrlem  46304  nnfoctbdjlem  46453  iundjiun  46458  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  ovnhoilem1  46599  vonioolem2  46679  vonicclem2  46682  pimrecltneg  46722  smfrec  46787  smfmullem1  46789  smfmullem2  46790  smfdiv  46795  sigaradd  46864  ormkglobd  46873  cjnpoly  46890  p1lep2  47301  zm1nn  47303  ceilhalfgt1  47330  2tceilhalfelfzo1  47333  ceilbi  47334  rehalfge1  47336  ceilhalfnn  47337  addmodne  47345  m1mod0mod1  47355  m1modmmod  47359  difmodm1lt  47360  modmknepk  47363  modp2nep1  47368  modm1nem2  47370  iccpartiltu  47423  iccpartlt  47425  iccpartgt  47428  fmtnoge3  47531  fmtnodvds  47545  fmtnoprmfac2lem1  47567  2pwp1prm  47590  flsqrt  47594  sfprmdvdsmersenne  47604  lighneallem2  47607  lighneallem4a  47609  proththdlem  47614  proththd  47615  nnoALTV  47696  bgoldbtbndlem4  47809  gpgprismgrusgra  48049  gpgedgvtx0  48052  gpgvtxedg0  48054  gpg5nbgrvtx03starlem2  48060  gpg3kgrtriexlem4  48077  gpg3kgrtriexlem6  48079  cznnring  48250  divge1b  48501  divgt1b  48502  nn0eo  48517  regt1loggt0  48525  rege1logbrege0  48547  logblt1b  48553  fllog2  48557  nnolog2flm1  48579  dignn0flhalflem1  48604  rrxlinesc  48724  rrxlinec  48725  eenglngeehlnmlem1  48726  eenglngeehlnmlem2  48727  line2ylem  48740  line2  48741  line2xlem  48742  reseccl  49742  recsccl  49743  amgmwlem  49791  amgmlemALT  49792