Theorem 1red 11210

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

Syntax hints:   → wi 4   ∈ wcel 2143  ℝcr 11100  1c1 11102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11159  ax-icn 11160  ax-addcl 11161  ax-mulcl 11163  ax-mulrcl 11164  ax-i2m1 11169  ax-1ne0 11170  ax-rrecex 11173  ax-cnre 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fv 6546  df-ov 7415

This theorem is referenced by:  recgt0  12062  mulgt1  12077  ltrec  12098  nnne0  12271  nn0p1gt0  12534  nn0ge2m1nn  12575  nn0le2is012  12661  suprzcl  12677  ledivge1le  13090  ge2halflem1  13134  qbtwnre  13226  lincmb01cmp  13523  iccf1o  13524  xov1plusxeqvd  13526  zltaddlt1le  13533  nnge2recico01  13535  fznatpl1  13608  elfz1b  13623  elfzo0subge1  13736  fzonn0p1p1  13775  elfznelfzo  13804  elfznelfzob  13805  fladdz  13860  2tnp1ge0ge0  13864  flhalf  13865  ltdifltdiv  13869  fldiv4lem1div2uz2  13871  mulp1mod1  13949  m1modge3gt1  13956  modltm1p1mod  13961  addmodlteq  13984  ltexp2a  14204  expcan  14207  ltexp2  14208  leexp2  14209  leexp2a  14210  leexp2r  14212  nnlesq  14243  bernneq3  14269  expnbnd  14270  expnlbnd2  14272  expnngt1  14279  fzsdom2  14467  wrdlenge2n0  14591  swrd2lsw  14991  2swrd2eqwrdeq  14992  01sqrexlem7  15301  rddif  15394  reccn2  15650  rlimo1  15670  o1fsum  15867  abscvgcvg  15873  climcndslem1  15905  flo1  15910  harmonic  15915  geomulcvg  15932  fprodrecl  16009  fprodreclf  16015  fprodle  16052  bpoly4  16114  efcllem  16132  efgt1  16173  tanhlt1  16217  sinltx  16246  eirrlem  16261  p1modz1  16318  mod2eq1n2dvds  16406  oddge22np1  16408  ltoddhalfle  16420  nn0o1gt2  16440  nno  16441  nn0oddm1d2  16444  nnoddm1d2  16445  bitsfzolem  16493  bitsfzo  16494  bitsmod  16495  bitscmp  16497  bitsinv1lem  16500  smuval2  16541  coprmgcdb  16708  prmind2  16744  dvdsnprmd  16749  2mulprm  16752  isprm5  16767  isprm7  16768  divdenle  16809  zsqrtelqelz  16818  fermltl  16844  odzdvds  16856  modprm0  16866  iserodd  16896  difsqpwdvds  16948  pcfaclem  16959  prmreclem1  16977  4sqlem11  17016  4sqlem12  17017  ramub1lem1  17087  prmgaplem8  17119  2expltfac  17153  chnccat  18683  pgpfaclem2  20155  qsidomlem1  21461  znidomb  21692  psdmvr  22313  chfacfisf  22992  chfacfisfcpmat  22993  chfacfscmulgsum  22998  chfacfpmmulgsum  23002  nrginvrcnlem  24829  nmoid  24880  xrsmopn  24951  metnrmlem1a  24997  iihalf2cn  25074  iccpnfhmeo  25085  lebnumii  25106  htpycc  25120  pcohtpylem  25159  pcoass  25164  pcorevlem  25166  nmhmcn  25260  cncmet  25462  ovoliunlem1  25642  dyadmaxlem  25737  vitalilem2  25749  mbfi1fseqlem6  25860  itg2mulc  25887  itg2monolem1  25890  itg2monolem3  25892  dveflem  26119  mvth  26132  dvlipcn  26134  lhop1lem  26153  dvfsumlem1  26166  dvfsumlem2  26167  dvfsumlem3  26168  dvfsumlem4  26169  dvfsum2  26174  fta1glem2  26307  plyeq0lem  26348  fta1lem  26449  vieta1lem2  26453  aalioulem3  26476  aalioulem4  26477  radcnvlem1  26554  radcnvlem2  26555  dvradcnv  26562  abelthlem2  26573  abelthlem5  26576  abelthlem7  26579  abelth2  26583  cos02pilt1  26669  cosne0  26672  rplogcl  26747  logdivlti  26763  logno1  26779  dvlog2lem  26795  advlog  26797  logtayllem  26802  cxplt  26837  cxple  26838  cxpaddlelem  26894  cxpaddle  26895  rtprmirr  26903  relogbf  26934  logbgt0b  26936  isosctrlem1  26961  isosctrlem2  26962  chordthmlem4  26978  heron  26981  atanlogaddlem  27056  bndatandm  27072  leibpi  27085  log2tlbnd  27088  birthdaylem3  27096  rlimcnp  27108  rlimcnp2  27109  efrlim  27112  cxp2limlem  27118  cxp2lim  27119  divsqrtsumo1  27126  jensenlem2  27130  logdiflbnd  27137  fsumharmonic  27154  lgamgulmlem2  27172  lgamgulmlem3  27173  lgamgulmlem4  27174  lgamgulmlem5  27175  lgamgulmlem6  27176  lgamcvg2  27197  regamcl  27203  wilthlem2  27211  ftalem2  27216  basellem9  27231  vma1  27308  ppieq0  27318  mumullem2  27322  fsumfldivdiaglem  27331  chpeq0  27350  chtub  27354  chpval2  27360  chpchtsum  27361  chpub  27362  logfacrlim  27366  logexprlim  27367  mersenne  27369  perfectlem2  27372  dchrelbas4  27385  bcmono  27419  bposlem1  27426  bposlem2  27427  zabsle1  27438  lgslem3  27441  lgsmod  27465  lgsdir2lem4  27470  lgsdirprm  27473  gausslemma2dlem1a  27507  gausslemma2d  27516  lgsquadlem2  27523  2sqlem8  27568  chebbnd1lem1  27611  chebbnd1lem2  27612  chtppilimlem1  27615  chebbnd2  27619  chto1lb  27620  chpchtlim  27621  chpo1ubb  27623  vmadivsum  27624  rplogsumlem1  27626  rpvmasumlem  27629  dchrisumlem3  27633  dchrmusumlema  27635  dchrmusum2  27636  dchrvmasumlem2  27640  dchrvmasumlem3  27641  dchrvmasumiflem1  27643  dchrvmasumiflem2  27644  dchrisum0flblem1  27650  dchrisum0flblem2  27651  dchrisum0fno1  27653  dchrisum0re  27655  dchrisum0lema  27656  dchrisum0lem1b  27657  dchrisum0lem2a  27659  dchrisum0lem2  27660  dchrisum0lem3  27661  rplogsum  27669  dirith2  27670  mudivsum  27672  mulogsumlem  27673  mulogsum  27674  mulog2sumlem1  27676  mulog2sumlem2  27677  vmalogdivsum2  27680  vmalogdivsum  27681  2vmadivsumlem  27682  log2sumbnd  27686  selberglem2  27688  selberg2lem  27692  chpdifbnd  27697  selberg3lem1  27699  selberg3  27701  selberg4lem1  27702  selberg4  27703  pntrmax  27706  pntrsumo1  27707  pntrsumbnd  27708  selberg3r  27711  selberg4r  27712  selberg34r  27713  pntrlog2bndlem1  27719  pntrlog2bndlem2  27720  pntrlog2bndlem3  27721  pntrlog2bndlem4  27722  pntrlog2bndlem5  27723  pntrlog2bndlem6  27725  pntrlog2bnd  27726  pntpbnd1a  27727  pntpbnd1  27728  pntibndlem2a  27732  pntibndlem2  27733  pntibnd  27735  pntlemc  27737  pntlemg  27740  pntlemr  27744  pntlemk  27748  pnt  27756  qabvle  27767  ostth2lem3  27777  ostth2  27779  trgcgrg  28762  tgcgr4  28778  ttgcontlem1  29212  axpaschlem  29268  axlowdimlem16  29285  axcontlem2  29293  axcontlem7  29298  nbusgrvtxm1  29707  upgrewlkle2  29934  pthdlem1  30093  crctcshwlkn0lem3  30139  crctcshwlkn0lem5  30141  wwlksm1edg  30208  wwlksnextproplem2  30237  clwlkclwwlklem2fv1  30324  clwlkclwwlklem2fv2  30325  clwlkclwwlklem2  30329  clwlkclwwlk2  30332  clwwisshclwwslem  30343  clwwlkf1  30378  clwwlkext2edg  30385  clwlknf1oclwwlknlem1  30410  clwwlknonex2lem2  30437  numclwwlk7  30720  frgrreggt1  30722  frgrogt3nreg  30726  smcnlem  31027  nmoub3i  31103  blocnilem  31134  ubthlem2  31201  minvecolem4  31210  htthlem  31247  nmcexi  32356  nmopcoi  32425  stadd3i  32578  cdj1i  32763  nnmulge  33062  receqid  33067  nndiffz1  33109  fzsplit3  33116  nexple  33155  indf1o  33162  wrdt2ind  33251  pmtrto1cl  33397  fzto1st1  33400  fzto1st  33401  psgnfzto1st  33403  cycpmco2lem6  33429  cycpmco2lem7  33430  cycpmrn  33441  krull  33739  ply1degltel  33862  ply1degltlss  33864  constrnegcl  34131  constrdircl  34133  iconstr  34134  constrrecl  34137  constrmulcl  34139  constrreinvcl  34140  constrresqrtcl  34145  cos9thpiminplylem1  34150  cos9thpiminply  34156  cos9thpinconstrlem1  34157  1smat1  34172  submateqlem1  34175  madjusmdetlem2  34196  unitdivcld  34269  sqsscirc1  34276  esumdivc  34451  dya2ub  34638  dya2iocress  34642  dya2iocbrsiga  34643  dya2icobrsiga  34644  dya2icoseg  34645  dya2iocucvr  34652  sxbrsigalem2  34654  fibp1  34769  probmeasb  34798  dstrvprob  34840  dstfrvunirn  34843  ballotlemfc0  34861  ballotlemfcc  34862  ballotlemsgt1  34879  ballotlemsel1i  34881  ballotlemfrcn0  34898  signsply0  34916  itgexpif  34971  reprlt  34984  chtvalz  34994  breprexplemc  34997  breprexp  34998  circlemeth  35005  tgoldbachgnn  35024  acycgr1v  35619  subfaclim  35658  cvmliftlem2  35756  cvmliftlem13  35766  snmlff  35799  bccolsum  36209  faclim  36216  nn0prpwlem  36811  dnibndlem10  37054  dnibndlem12  37056  knoppcnlem4  37063  unblimceq0  37074  knoppndvlem1  37079  knoppndvlem2  37080  knoppndvlem3  37081  knoppndvlem7  37085  knoppndvlem11  37089  knoppndvlem12  37090  knoppndvlem14  37092  knoppndvlem15  37093  knoppndvlem17  37095  knoppndvlem18  37096  knoppndvlem20  37098  irrdiff  37948  poimirlem6  38255  poimirlem7  38256  poimirlem15  38264  poimirlem19  38268  poimirlem29  38278  poimirlem30  38279  poimirlem31  38280  poimirlem32  38281  broucube  38283  itg2addnclem2  38301  itg2addnclem3  38302  areacirclem1  38337  areacirclem4  38340  incsequz  38377  totbndbnd  38418  bfplem2  38452  resdvopclptsd  42773  lcmineqlem2  42775  lcmineqlem3  42776  lcmineqlem10  42783  lcmineqlem12  42785  lcmineqlem15  42788  lcmineqlem18  42791  lcmineqlem19  42792  lcmineqlem20  42793  lcmineqlem22  42795  lcmineqlem23  42796  3lexlogpow5ineq2  42800  3lexlogpow5ineq4  42801  3lexlogpow5ineq3  42802  3lexlogpow2ineq1  42803  3lexlogpow2ineq2  42804  3lexlogpow5ineq5  42805  aks4d1lem1  42807  dvrelog2  42809  dvrelog3  42810  dvrelog2b  42811  dvrelogpow2b  42813  aks4d1p1p3  42814  aks4d1p1p2  42815  aks4d1p1p4  42816  aks4d1p1p6  42818  aks4d1p1p7  42819  aks4d1p1p5  42820  aks4d1p1  42821  aks4d1p2  42822  aks4d1p3  42823  aks4d1p5  42825  aks4d1p6  42826  aks4d1p7d1  42827  aks4d1p7  42828  aks4d1p8d2  42830  aks4d1p8d3  42831  aks4d1p8  42832  aks4d1p9  42833  posbezout  42845  primrootlekpowne0  42850  primrootspoweq0  42851  aks6d1c1  42861  aks6d1c2p2  42864  hashscontpow1  42866  aks6d1c3  42868  aks6d1c2lem4  42872  aks6d1c2  42875  2np3bcnp1  42889  2ap1caineq  42890  sticksstones6  42896  sticksstones7  42897  sticksstones10  42900  sticksstones12a  42902  sticksstones12  42903  sticksstones22  42913  aks6d1c6lem3  42917  aks6d1c6lem4  42918  bcled  42923  bcle2d  42924  aks6d1c7lem1  42925  aks6d1c7lem2  42926  unitscyglem2  42941  unitscyglem4  42943  unitscyglem5  42944  aks5lem8  42946  sn-1ne2  43010  redvmptabs  43099  sn-00idlem2  43138  sn-0ne2  43145  rei4  43163  rediveq1d  43190  sn-rediv1d  43191  sn-rereccld  43194  rerecne0d  43195  rerecidd  43196  rerecrecd  43198  sn-0tie0  43203  sn-nnne0  43212  mulgt0b1d  43224  sn-ltmulgt11d  43226  sn-0lt1  43227  sn-mulgt1d  43231  fimgmcyc  43282  flt4lem7  43371  fltnlta  43375  3cubeslem1  43395  3cubeslem3r  43398  3cubeslem4  43400  lzenom  43481  irrapxlem1  43529  irrapxlem2  43530  irrapxlem4  43532  irrapxlem5  43533  pellexlem2  43537  pell1qrge1  43577  pell1qr1  43578  elpell1qr2  43579  pell14qrgapw  43583  pellfundgt1  43590  pellfundglb  43592  pellfundex  43593  pellfundrp  43595  pellfundne1  43596  rmspecsqrtnq  43613  rmspecnonsq  43614  rmspecfund  43616  rmspecpos  43623  monotoddzzfi  43649  rmygeid  43671  areaquad  43923  imo72b2lem0  44871  imo72b2lem1  44875  imo72b2  44878  cvgdvgrat  45003  radcnvrat  45004  hashnzfzclim  45012  lhe4.4ex1a  45019  binomcxplemnn0  45039  binomcxplemdvbinom  45043  binomcxplemnotnn0  45046  oddfl  45977  abscosbd  45978  zltlesub  45984  abssinbd  45994  monoords  45996  fzisoeu  45999  fzdifsuc2  46009  suplesup  46035  xralrple2  46050  infxr  46062  infleinflem2  46066  reclt0d  46082  xrralrecnnge  46085  sqrlearg  46249  iooiinioc  46252  fmul01  46276  fmul01lt1lem1  46280  fmul01lt1lem2  46281  climsuselem1  46303  sumnnodd  46326  0ellimcdiv  46343  dvmptidg  46611  dvcosax  46620  ioodvbdlimc1lem1  46625  ioodvbdlimc1lem2  46626  ioodvbdlimc2lem  46628  dvxpaek  46634  dvnmul  46637  iblspltprt  46667  itgspltprt  46673  stoweidlem5  46699  stoweidlem7  46701  stoweidlem10  46704  stoweidlem11  46705  stoweidlem12  46706  stoweidlem13  46707  stoweidlem14  46708  stoweidlem16  46710  stoweidlem18  46712  stoweidlem20  46714  stoweidlem24  46718  stoweidlem25  46719  stoweidlem34  46728  stoweidlem36  46730  stoweidlem38  46732  stoweidlem40  46734  stoweidlem41  46735  stoweidlem42  46736  stoweidlem45  46739  stoweidlem51  46745  stoweidlem60  46754  wallispilem3  46761  wallispilem4  46762  wallispilem5  46763  wallispi  46764  wallispi2lem1  46765  wallispi2lem2  46766  wallispi2  46767  stirlinglem1  46768  stirlinglem3  46770  stirlinglem5  46772  stirlinglem6  46773  stirlinglem7  46774  stirlinglem8  46775  stirlinglem10  46777  stirlinglem11  46778  stirlinglem12  46779  stirlinglem13  46780  stirlinglem15  46782  dirker2re  46786  dirkerval2  46788  dirkerre  46789  dirkertrigeqlem1  46792  dirkertrigeqlem3  46794  dirkeritg  46796  dirkercncflem1  46797  dirkercncflem2  46798  dirkercncflem4  46800  fourierdlem5  46806  fourierdlem6  46807  fourierdlem11  46812  fourierdlem15  46816  fourierdlem19  46820  fourierdlem20  46821  fourierdlem24  46825  fourierdlem26  46827  fourierdlem28  46829  fourierdlem30  46831  fourierdlem39  46840  fourierdlem41  46842  fourierdlem43  46844  fourierdlem47  46847  fourierdlem48  46848  fourierdlem56  46856  fourierdlem60  46860  fourierdlem61  46861  fourierdlem62  46862  fourierdlem64  46864  fourierdlem65  46865  fourierdlem66  46866  fourierdlem68  46868  fourierdlem73  46873  fourierdlem78  46878  fourierdlem79  46879  fourierdlem87  46887  fourierdlem103  46903  fourierdlem104  46904  sqwvfoura  46922  fouriersw  46925  etransclem4  46932  etransclem23  46951  etransclem24  46952  etransclem31  46959  etransclem32  46960  etransclem35  46963  etransclem41  46969  etransclem46  46974  etransclem48  46976  etransc  46977  ioorrnopnxrlem  47000  nnfoctbdjlem  47149  iundjiun  47154  hoidmvlelem1  47289  hoidmvlelem2  47290  hoidmvlelem3  47291  hoidmvlelem4  47292  ovnhoilem1  47295  vonioolem2  47375  vonicclem2  47378  pimrecltneg  47418  smfrec  47483  smfmullem1  47485  smfmullem2  47486  smfdiv  47491  sigaradd  47560  ormkglobd  47571  cjnpoly  47603  p1lep2  48014  zm1nn  48016  ceilhalfgt1  48047  2tceilhalfelfzo1  48050  ceilbi  48051  rehalfge1  48053  ceilhalfnn  48054  flmrecm1  48057  addmodne  48064  m1mod0mod1  48074  m1modmmod  48078  difmodm1lt  48079  modmknepk  48082  modp2nep1  48087  modm1nem2  48089  2timesltsqm1  48093  muldvdsfacm1  48101  iccpartiltu  48148  iccpartlt  48150  iccpartgt  48153  fmtnoge3  48259  fmtnodvds  48273  fmtnoprmfac2lem1  48295  2pwp1prm  48318  flsqrt  48322  sfprmdvdsmersenne  48332  lighneallem2  48335  lighneallem4a  48337  proththdlem  48342  proththd  48343  nprmdvdsfacm1lem4  48352  nnoALTV  48437  bgoldbtbndlem4  48550  gpgprismgrusgra  48800  gpgedgvtx0  48803  gpgvtxedg0  48805  gpg5nbgrvtx03starlem2  48811  gpg3kgrtriexlem4  48828  gpg3kgrtriexlem6  48830  cznnring  49004  divge1b  49269  divgt1b  49270  nn0eo  49285  regt1loggt0  49293  rege1logbrege0  49315  logblt1b  49321  fllog2  49325  nnolog2flm1  49347  dignn0flhalflem1  49372  rrxlinesc  49492  rrxlinec  49493  eenglngeehlnmlem1  49494  eenglngeehlnmlem2  49495  line2ylem  49508  line2  49509  line2xlem  49510  reseccl  50508  recsccl  50509  amgmwlem  50579  amgmlemALT  50580