Theorem 1red 11312

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ℝcr 11202  1c1 11204

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11261  ax-icn 11262  ax-addcl 11263  ax-mulcl 11265  ax-mulrcl 11266  ax-i2m1 11271  ax-1ne0 11272  ax-rrecex 11275  ax-cnre 11276

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546  df-ov 7423

This theorem is used by:  recgt0  12166  mulgt1  12181  ltrec  12202  nnne0  12375  nn0p1gt0  12638  nn0ge2m1nn  12679  nn0le2is012  12766  suprzcl  12782  ledivge1le  13196  ge2halflem1  13240  qbtwnre  13332  lincmb01cmp  13629  iccf1o  13630  xov1plusxeqvd  13632  zltaddlt1le  13639  nnge2recico01  13641  fznatpl1  13715  elfz1b  13730  elfzo0subge1  13843  fzonn0p1p1  13882  elfznelfzo  13911  elfznelfzob  13912  fladdz  13968  2tnp1ge0ge0  13972  flhalf  13973  ltdifltdiv  13977  mulp1mod1  14057  m1modge3gt1  14064  modltm1p1mod  14069  addmodlteq  14092  ltexp2a  14312  expcan  14315  ltexp2  14316  leexp2  14317  leexp2a  14318  leexp2r  14320  nnlesq  14352  bernneq3  14378  expnbnd  14379  expnlbnd2  14381  expnngt1  14388  fzsdom2  14576  wrdlenge2n0  14700  swrd2lsw  15110  2swrd2eqwrdeq  15111  01sqrexlem7  15420  rddif  15513  reccn2  15769  rlimo1  15789  o1fsum  15985  abscvgcvg  15991  climcndslem1  16023  flo1  16028  harmonic  16033  geomulcvg  16050  fprodrecl  16125  fprodreclf  16131  fprodle  16168  bpoly4  16230  efcllem  16248  efgt1  16289  tanhlt1  16333  sinltx  16362  eirrlem  16377  p1modz1  16434  mod2eq1n2dvds  16522  oddge22np1  16524  ltoddhalfle  16536  nn0o1gt2  16556  nno  16557  nn0oddm1d2  16560  nnoddm1d2  16561  bitsfzolem  16609  bitsfzo  16610  bitsmod  16611  bitscmp  16613  bitsinv1lem  16616  smuval2  16657  coprmgcdb  16829  prmind2  16865  dvdsnprmd  16870  2mulprm  16873  isprm5  16888  isprm7  16889  divdenle  16930  zsqrtelqelz  16939  fermltl  16966  odzdvds  16978  modprm0  16988  iserodd  17018  difsqpwdvds  17070  pcfaclem  17081  prmreclem1  17099  4sqlem11  17138  4sqlem12  17139  ramub1lem1  17209  prmgaplem8  17241  2expltfac  17275  chnccat  18805  pgpfaclem2  20303  qsidomlem1  21641  znidomb  21872  psdmvr  22495  chfacfisf  23177  chfacfisfcpmat  23178  chfacfscmulgsum  23183  chfacfpmmulgsum  23187  nrginvrcnlem  25015  nmoid  25066  xrsmopn  25137  metnrmlem1a  25183  iihalf2cn  25260  iccpnfhmeo  25271  lebnumii  25292  htpycc  25306  pcohtpylem  25345  pcoass  25350  pcorevlem  25352  nmhmcn  25446  cncmet  25648  ovoliunlem1  25828  dyadmaxlem  25923  vitalilem2  25935  mbfi1fseqlem6  26046  itg2mulc  26073  itg2monolem1  26076  itg2monolem3  26078  dveflem  26304  mvth  26317  dvlipcn  26319  lhop1lem  26338  dvfsumlem1  26351  dvfsumlem2  26352  dvfsumlem3  26353  dvfsumlem4  26354  dvfsum2  26359  fta1glem2  26492  plyeq0lem  26534  fta1lem  26633  vieta1lem2  26639  aalioulem3  26666  aalioulem4  26667  radcnvlem1  26745  radcnvlem2  26746  dvradcnv  26753  abelthlem2  26764  abelthlem5  26767  abelthlem7  26770  abelth2  26774  cos02pilt1  26859  cosne0  26862  rplogcl  26937  logdivlti  26953  logno1  26969  dvlog2lem  26985  advlog  26987  logtayllem  26992  cxplt  27027  cxple  27028  cxpaddlelem  27084  cxpaddle  27085  rtprmirr  27093  relogbf  27124  logbgt0b  27126  isosctrlem1  27151  isosctrlem2  27152  chordthmlem4  27168  heron  27171  atanlogaddlem  27246  bndatandm  27262  leibpi  27275  log2tlbnd  27278  birthdaylem3  27286  rlimcnp  27298  rlimcnp2  27299  efrlim  27302  cxp2limlem  27308  cxp2lim  27309  divsqrtsumo1  27316  jensenlem2  27320  logdiflbnd  27327  fsumharmonic  27344  lgamgulmlem2  27362  lgamgulmlem3  27363  lgamgulmlem4  27364  lgamgulmlem5  27365  lgamgulmlem6  27366  lgamcvg2  27387  regamcl  27393  wilthlem2  27401  ftalem2  27406  basellem9  27421  vma1  27498  ppieq0  27508  mumullem2  27512  fsumfldivdiaglem  27521  ppiub  27536  chpeq0  27540  chtub  27544  chpval2  27550  chpchtsum  27551  chpub  27552  logfacrlim  27556  logexprlim  27557  mersenne  27559  perfectlem2  27562  dchrelbas4  27575  bcmono  27609  bposlem1  27616  bposlem2  27617  zabsle1  27628  lgslem3  27631  lgsmod  27655  lgsdir2lem4  27660  lgsdirprm  27663  gausslemma2dlem1a  27697  gausslemma2d  27706  lgsquadlem2  27713  2sqlem8  27758  chebbnd1lem1  27801  chebbnd1lem2  27802  chtppilimlem1  27805  chebbnd2  27809  chto1lb  27810  chpchtlim  27811  chpo1ubb  27813  vmadivsum  27814  rplogsumlem1  27816  rpvmasumlem  27819  dchrisumlem3  27823  dchrmusumlema  27825  dchrmusum2  27826  dchrvmasumlem2  27830  dchrvmasumlem3  27831  dchrvmasumiflem1  27833  dchrvmasumiflem2  27834  dchrisum0flblem1  27840  dchrisum0flblem2  27841  dchrisum0fno1  27843  dchrisum0re  27845  dchrisum0lema  27846  dchrisum0lem1b  27847  dchrisum0lem2a  27849  dchrisum0lem2  27850  dchrisum0lem3  27851  rplogsum  27859  dirith2  27860  mudivsum  27862  mulogsumlem  27863  mulogsum  27864  mulog2sumlem1  27866  mulog2sumlem2  27867  vmalogdivsum2  27870  vmalogdivsum  27871  2vmadivsumlem  27872  log2sumbnd  27876  selberglem2  27878  selberg2lem  27882  chpdifbnd  27887  selberg3lem1  27889  selberg3  27891  selberg4lem1  27892  selberg4  27893  pntrmax  27896  pntrsumo1  27897  pntrsumbnd  27898  selberg3r  27901  selberg4r  27902  selberg34r  27903  pntrlog2bndlem1  27909  pntrlog2bndlem2  27910  pntrlog2bndlem3  27911  pntrlog2bndlem4  27912  pntrlog2bndlem5  27913  pntrlog2bndlem6  27915  pntrlog2bnd  27916  pntpbnd1a  27917  pntpbnd1  27918  pntibndlem2a  27922  pntibndlem2  27923  pntibnd  27925  pntlemc  27927  pntlemg  27930  pntlemr  27934  pntlemk  27938  pnt  27946  qabvle  27957  ostth2lem3  27967  ostth2  27969  flt4lem7  27994  trgcgrg  28983  tgcgr4  28999  ttgcontlem1  29467  axpaschlem  29523  axlowdimlem16  29540  axcontlem2  29548  axcontlem7  29553  nbusgrvtxm1  29965  upgrewlkle2  30192  pthdlem1  30357  crctcshwlkn0lem3  30406  crctcshwlkn0lem5  30408  wwlksm1edg  30475  wwlksnextproplem2  30504  clwlkclwwlklem2fv1  30591  clwlkclwwlklem2fv2  30592  clwlkclwwlklem2  30596  clwlkclwwlk2  30599  clwwisshclwwslem  30610  clwwlkf1  30645  clwwlkext2edg  30652  clwlknf1oclwwlknlem1  30677  clwwlknonex2lem2  30704  numclwwlk7  30997  frgrreggt1  30999  frgrogt3nreg  31003  smcnlem  31304  nmoub3i  31380  blocnilem  31411  ubthlem2  31478  minvecolem4  31487  htthlem  31524  nmcexi  32633  nmopcoi  32702  stadd3i  32855  cdj1i  33040  nnmulge  33377  receqid  33382  nndiffz1  33424  fzsplit3  33431  nexple  33470  indf1o  33477  wrdt2ind  33562  pmtrto1cl  33706  fzto1st1  33709  fzto1st  33710  psgnfzto1st  33712  cycpmco2lem6  33738  cycpmco2lem7  33739  cycpmrn  33750  krull  34049  ply1degltel  34172  ply1degltlss  34174  constrnegcl  34441  constrdircl  34443  iconstr  34444  constrrecl  34447  constrmulcl  34449  constrreinvcl  34450  constrresqrtcl  34455  cos9thpiminplylem1  34460  cos9thpiminply  34466  cos9thpinconstrlem1  34467  1smat1  34482  submateqlem1  34485  madjusmdetlem2  34506  unitdivcld  34579  sqsscirc1  34586  esumdivc  34761  dya2ub  34948  dya2iocress  34952  dya2iocbrsiga  34953  dya2icobrsiga  34954  dya2icoseg  34955  dya2iocucvr  34962  sxbrsigalem2  34964  omssubadd  34978  fibp1  35079  probmeasb  35108  dstrvprob  35150  dstfrvunirn  35153  ballotlemfc0  35171  ballotlemfcc  35172  ballotlemsgt1  35189  ballotlemsel1i  35191  ballotlemfrcn0  35208  signsply0  35226  itgexpif  35281  reprlt  35294  chtvalz  35304  breprexplemc  35307  breprexp  35308  circlemeth  35315  tgoldbachgnn  35334  acycgr1v  35990  subfaclim  36039  cvmliftlem2  36137  cvmliftlem13  36147  snmlff  36180  bccolsum  36596  faclim  36603  nn0prpwlem  37202  dnibndlem10  37445  dnibndlem12  37447  knoppcnlem4  37454  unblimceq0  37465  knoppndvlem1  37470  knoppndvlem2  37471  knoppndvlem3  37472  knoppndvlem7  37476  knoppndvlem11  37480  knoppndvlem12  37481  knoppndvlem14  37483  knoppndvlem15  37484  knoppndvlem17  37486  knoppndvlem18  37487  knoppndvlem20  37489  irrdiff  38340  poimirlem6  38637  poimirlem7  38638  poimirlem15  38646  poimirlem19  38650  poimirlem29  38660  poimirlem30  38661  poimirlem31  38662  poimirlem32  38663  broucube  38665  itg2addnclem2  38683  itg2addnclem3  38684  areacirclem1  38719  areacirclem4  38722  incsequz  38775  totbndbnd  38816  bfplem2  38850  resdvopclptsd  43171  lcmineqlem2  43173  lcmineqlem3  43174  lcmineqlem10  43181  lcmineqlem12  43183  lcmineqlem15  43186  lcmineqlem18  43189  lcmineqlem19  43190  lcmineqlem20  43191  lcmineqlem22  43193  lcmineqlem23  43194  3lexlogpow5ineq2  43198  3lexlogpow5ineq4  43199  3lexlogpow5ineq3  43200  3lexlogpow2ineq1  43201  3lexlogpow2ineq2  43202  3lexlogpow5ineq5  43203  aks4d1lem1  43205  dvrelog2  43207  dvrelog3  43208  dvrelog2b  43209  dvrelogpow2b  43211  aks4d1p1p3  43212  aks4d1p1p2  43213  aks4d1p1p4  43214  aks4d1p1p6  43216  aks4d1p1p7  43217  aks4d1p1p5  43218  aks4d1p1  43219  aks4d1p2  43220  aks4d1p3  43221  aks4d1p5  43223  aks4d1p6  43224  aks4d1p7d1  43225  aks4d1p7  43226  aks4d1p8d2  43228  aks4d1p8d3  43229  aks4d1p8  43230  aks4d1p9  43231  posbezout  43243  primrootlekpowne0  43248  primrootspoweq0  43249  aks6d1c1  43259  aks6d1c2p2  43262  hashscontpow1  43264  aks6d1c3  43266  aks6d1c2lem4  43270  aks6d1c2  43273  2np3bcnp1  43287  2ap1caineq  43288  sticksstones6  43294  sticksstones7  43295  sticksstones10  43298  sticksstones12a  43300  sticksstones12  43301  sticksstones22  43311  aks6d1c6lem3  43315  aks6d1c6lem4  43316  bcled  43321  bcle2d  43322  aks6d1c7lem1  43323  aks6d1c7lem2  43324  unitscyglem2  43339  unitscyglem4  43341  unitscyglem5  43342  aks5lem8  43344  sn-1ne2  43423  redvmptabs  43504  sn-00idlem2  43543  sn-0ne2  43550  rei4  43568  rediveq1d  43595  sn-rediv1d  43596  sn-rereccld  43599  rerecne0d  43600  rerecidd  43601  rerecrecd  43603  sn-0tie0  43608  sn-nnne0  43617  mulgt0b1d  43629  sn-ltmulgt11d  43631  sn-0lt1  43632  sn-mulgt1d  43636  fimgmcyc  43691  fltnlta  43767  3cubeslem1  43787  3cubeslem3r  43790  3cubeslem4  43792  lzenom  43874  irrapxlem1  43922  irrapxlem2  43923  irrapxlem4  43925  irrapxlem5  43926  pellexlem2  43930  pell1qrge1  43970  pell1qr1  43971  elpell1qr2  43972  pell14qrgapw  43976  pellfundgt1  43983  pellfundglb  43985  pellfundex  43986  pellfundrp  43988  pellfundne1  43989  rmspecsqrtnq  44006  rmspecnonsq  44007  rmspecfund  44009  rmspecpos  44016  monotoddzzfi  44042  rmygeid  44064  areaquad  44311  imo72b2lem0  45258  imo72b2lem1  45262  imo72b2  45265  cvgdvgrat  45390  radcnvrat  45391  hashnzfzclim  45399  lhe4.4ex1a  45406  binomcxplemnn0  45426  binomcxplemdvbinom  45430  binomcxplemnotnn0  45433  oddfl  46387  abscosbd  46388  zltlesub  46394  abssinbd  46404  monoords  46406  fzisoeu  46409  fzdifsuc2  46419  suplesup  46444  xralrple2  46459  infxr  46471  infleinflem2  46475  reclt0d  46491  xrralrecnnge  46494  sqrlearg  46658  iooiinioc  46661  fmul01  46685  fmul01lt1lem1  46689  fmul01lt1lem2  46690  climsuselem1  46712  sumnnodd  46735  0ellimcdiv  46752  dvmptidg  47020  dvcosax  47029  ioodvbdlimc1lem1  47034  ioodvbdlimc1lem2  47035  ioodvbdlimc2lem  47037  dvxpaek  47043  dvnmul  47046  iblspltprt  47076  itgspltprt  47082  stoweidlem5  47108  stoweidlem7  47110  stoweidlem10  47113  stoweidlem11  47114  stoweidlem12  47115  stoweidlem13  47116  stoweidlem14  47117  stoweidlem16  47119  stoweidlem18  47121  stoweidlem20  47123  stoweidlem24  47127  stoweidlem25  47128  stoweidlem34  47137  stoweidlem36  47139  stoweidlem38  47141  stoweidlem40  47143  stoweidlem41  47144  stoweidlem42  47145  stoweidlem45  47148  stoweidlem51  47154  stoweidlem60  47163  wallispilem3  47170  wallispilem4  47171  wallispilem5  47172  wallispi  47173  wallispi2lem1  47174  wallispi2lem2  47175  wallispi2  47176  stirlinglem1  47177  stirlinglem3  47179  stirlinglem5  47181  stirlinglem6  47182  stirlinglem7  47183  stirlinglem8  47184  stirlinglem10  47186  stirlinglem11  47187  stirlinglem12  47188  stirlinglem13  47189  stirlinglem15  47191  dirker2re  47195  dirkerval2  47197  dirkerre  47198  dirkertrigeqlem1  47201  dirkertrigeqlem3  47203  dirkeritg  47205  dirkercncflem1  47206  dirkercncflem2  47207  dirkercncflem4  47209  fourierdlem5  47215  fourierdlem6  47216  fourierdlem11  47221  fourierdlem15  47225  fourierdlem19  47229  fourierdlem20  47230  fourierdlem24  47234  fourierdlem26  47236  fourierdlem28  47238  fourierdlem30  47240  fourierdlem39  47249  fourierdlem41  47251  fourierdlem43  47253  fourierdlem47  47256  fourierdlem48  47257  fourierdlem56  47265  fourierdlem60  47269  fourierdlem61  47270  fourierdlem62  47271  fourierdlem64  47273  fourierdlem65  47274  fourierdlem66  47275  fourierdlem68  47277  fourierdlem73  47282  fourierdlem78  47287  fourierdlem79  47288  fourierdlem87  47296  fourierdlem103  47312  fourierdlem104  47313  sqwvfoura  47331  fouriersw  47334  etransclem4  47341  etransclem23  47360  etransclem24  47361  etransclem31  47368  etransclem32  47369  etransclem35  47372  etransclem41  47378  etransclem46  47383  etransclem48  47385  etransc  47386  ioorrnopnxrlem  47409  nnfoctbdjlem  47558  iundjiun  47563  hoidmvlelem1  47698  hoidmvlelem2  47699  hoidmvlelem3  47700  hoidmvlelem4  47701  ovnhoilem1  47704  vonioolem2  47784  vonicclem2  47787  pimrecltneg  47827  smfrec  47892  smfmullem1  47894  smfmullem2  47895  smfdiv  47900  sigaradd  47969  ormkglobd  47980  cjnpoly  48032  p1lep2  48463  zm1nn  48465  ceilhalfgt1  48496  2tceilhalfelfzo1  48499  ceilbi  48500  rehalfge1  48502  ceilhalfnn  48503  flmrecm1  48506  addmodne  48513  m1mod0mod1  48523  m1modmmod  48527  difmodm1lt  48528  modmknepk  48531  modp2nep1  48536  modm1nem2  48538  2timesltsqm1  48542  muldvdsfacm1  48550  iccpartiltu  48597  iccpartlt  48599  iccpartgt  48602  fmtnoge3  48708  fmtnodvds  48722  fmtnoprmfac2lem1  48744  2pwp1prm  48767  flsqrt  48771  sfprmdvdsmersenne  48781  lighneallem2  48784  lighneallem4a  48786  proththdlem  48791  proththd  48792  nprmdvdsfacm1lem4  48801  nnoALTV  48886  bgoldbtbndlem4  48999  gpgprismgrusgra  49249  gpgedgvtx0  49252  gpgvtxedg0  49254  gpg5nbgrvtx03starlem2  49260  gpg3kgrtriexlem4  49277  gpg3kgrtriexlem6  49279  cznnring  49452  divge1b  49717  divgt1b  49718  nn0eo  49733  regt1loggt0  49741  rege1logbrege0  49763  logblt1b  49769  fllog2  49773  nnolog2flm1  49795  dignn0flhalflem1  49820  rrxlinesc  49941  rrxlinec  49942  eenglngeehlnmlem1  49943  eenglngeehlnmlem2  49944  line2ylem  49956  line2  49957  line2xlem  49958  reseccl  51014  recsccl  51015  amgmwlem  51155  amgmlemALT  51156