Theorem 1re 8331

Description: 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)

Assertion

Ref	Expression
1re	⊢ 1 ∈ ℝ

Proof of Theorem 1re

Step	Hyp	Ref	Expression
1		ax-1re 8279	1 ⊢ 1 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2209  ℝcr 8184  1c1 8186

This proof depends on axioms:  ax-1re 8279

This theorem is used by:  0re  8332  1red  8347  1xr  8390  0lt1  8460  peano2re  8469  peano2rem  8600  0reALT  8630  0le1  8816  1le1  8908  inelr  8920  1ap0  8926  eqneg  9070  ltp1  9182  ltm1  9184  recgt0  9188  mulgt1  9201  ltmulgt11  9202  lemulge11  9204  reclt1  9234  recgt1  9235  recgt1i  9236  recp1lt1  9237  recreclt  9238  sup3exmid  9295  cju  9299  indfval  9308  indconst1  9312  peano5nni  9316  nnssre  9317  1nn  9324  nnge1  9336  nnle1eq1  9337  nngt0  9338  nnnlt1  9339  nn1gt1  9347  nngt1ne1  9348  nnrecre  9350  nnrecgt0  9351  nnsub  9352  2re  9383  3re  9387  4re  9390  5re  9392  6re  9394  7re  9396  8re  9398  9re  9400  0le2  9403  2pos  9404  3pos  9407  4pos  9410  5pos  9413  6pos  9414  7pos  9415  8pos  9416  9pos  9417  neg1rr  9419  neg1lt0  9421  1lt2  9485  1lt3  9487  1lt4  9490  1lt5  9494  1lt6  9499  1lt7  9505  1lt8  9512  1lt9  9520  1ne2  9522  1ap2  9523  1le2  9524  1le3  9527  halflt1  9533  iap0  9539  addltmul  9553  elnnnn0c  9619  nn0ge2m1nn  9636  elnnz1  9676  zltp1le  9708  zleltp1  9709  recnz  9749  gtndiv  9751  3halfnz  9753  1lt10  9930  eluzp1m1  9961  eluzp1p1  9963  eluz2b2  10018  1rp  10074  divlt1lt  10141  divle1le  10142  nnledivrp  10183  0elunit  10404  1elunit  10405  divelunit  10420  lincmb01cmp  10421  lincmble  10422  iccf1o  10423  unitssre  10424  fzpreddisj  10494  fznatpl1  10499  fztpval  10506  qbtwnxr  10708  flqbi2  10746  fldiv4p1lem1div2  10760  flqdiv  10778  seqf1oglem1  10976  reexpcl  11013  reexpclzap  11016  expge0  11032  expge1  11033  expgt1  11034  resq01  11115  bernneq  11118  bernneq2  11119  expnbnd  11121  expnlbnd  11122  expnlbnd2  11123  nn0ltexp2  11168  facwordi  11199  faclbnd3  11202  faclbnd6  11203  facavg  11205  hashtpglem  11319  lsw0  11373  cjexp  11679  re1  11684  im1  11685  rei  11686  imi  11687  caucvgre  11768  sqrt1  11833  sqrt2gt1lt2  11836  abs1  11859  caubnd2  11905  mulcn2  12102  reccn2ap  12103  expcnvap0  12293  geo2sum  12305  cvgratnnlemrate  12321  fprodge0  12428  fprodge1  12430  fprodle  12431  ere  12461  ege2le3  12462  efgt1  12488  resin4p  12509  recos4p  12510  sinbnd  12543  cosbnd  12544  sinbnd2  12545  cosbnd2  12546  ef01bndlem  12547  sin01bnd  12548  cos01bnd  12549  cos1bnd  12550  cos2bnd  12551  sinltxirr  12552  sin01gt0  12553  cos01gt0  12554  sin02gt0  12555  sincos1sgn  12556  cos12dec  12559  ene1  12576  eap1  12577  3dvds  12655  halfleoddlt  12685  flodddiv4  12727  isprm3  12920  sqnprm  12939  coprm  12947  phibndlem  13022  pythagtriplem3  13074  fldivp1  13155  pockthi  13165  ballotfilem2  13285  ballotfilem4  13298  ballotfilemi1  13302  ballotfilemic  13307  exmidunben  13374  basendxnmulrndx  13546  starvndxnbasendx  13554  scandxnbasendx  13566  vscandxnbasendx  13571  ipndxnbasendx  13584  basendxnocndx  13625  setsmsbasg  15722  tgioo  15797  dveflem  15969  reeff1olem  16014  reeff1o  16016  cosz12  16024  sinhalfpilem  16035  tangtx  16082  sincos4thpi  16084  pigt3  16088  coskpi  16092  cos0pilt1  16097  ioocosf1o  16099  loge  16113  logrpap0b  16123  logdivlti  16128  2logb9irrALT  16227  sqrt2cxp2logb9e3  16228  birthdaylem3  16244  ppiublem1  16308  ppiqub  16310  chtublem  16312  chtqub  16313  perfectlem2  16317  bposlem1  16328  bposlem2  16329  bposlem5  16332  bposlem8  16335  lgsdir  16376  lgsne0  16379  lgsabs1  16380  lgsdinn0  16389  gausslemma2dlem0i  16398  lgseisen  16415  2lgslem3  16442  usgrexmpldifpr  16712  konigsberglem2  16952  konigsberglem3  16953  konigsberglem5  16955  ex-fl  16961  cvgcmp2nlemabs  17304  iooref1o  17306  trilpolemclim  17309  trilpolemcl  17310  trilpolemisumle  17311  trilpolemeq1  17313  trilpolemlt1  17314  apdiff  17321  nconstwlpolemgt0  17338