Theorem 1re 7898

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

Assertion

Ref	Expression
1re	|- 1 e. RR

Proof of Theorem 1re

Step	Hyp	Ref	Expression
1		ax-1re 7847	1 |- 1 e. RR

Syntax hints:   e. wcel 2136   RRcr 7752   1c1 7754

This theorem was proved from axioms:  ax-1re 7847

This theorem is referenced by:  0re  7899  1red  7914  1xr  7957  0lt1  8025  peano2re  8034  peano2rem  8165  0reALT  8195  0le1  8379  1le1  8470  inelr  8482  1ap0  8488  eqneg  8628  ltp1  8739  ltm1  8741  recgt0  8745  mulgt1  8758  ltmulgt11  8759  lemulge11  8761  reclt1  8791  recgt1  8792  recgt1i  8793  recp1lt1  8794  recreclt  8795  sup3exmid  8852  cju  8856  peano5nni  8860  nnssre  8861  1nn  8868  nnge1  8880  nnle1eq1  8881  nngt0  8882  nnnlt1  8883  nn1gt1  8891  nngt1ne1  8892  nnrecre  8894  nnrecgt0  8895  nnsub  8896  2re  8927  3re  8931  4re  8934  5re  8936  6re  8938  7re  8940  8re  8942  9re  8944  0le2  8947  2pos  8948  3pos  8951  4pos  8954  5pos  8957  6pos  8958  7pos  8959  8pos  8960  9pos  8961  neg1rr  8963  neg1lt0  8965  1lt2  9026  1lt3  9028  1lt4  9031  1lt5  9035  1lt6  9040  1lt7  9046  1lt8  9053  1lt9  9061  1ne2  9063  1ap2  9064  1le2  9065  1le3  9068  halflt1  9074  iap0  9080  addltmul  9093  elnnnn0c  9159  nn0ge2m1nn  9174  elnnz1  9214  zltp1le  9245  zleltp1  9246  recnz  9284  gtndiv  9286  3halfnz  9288  1lt10  9460  eluzp1m1  9489  eluzp1p1  9491  eluz2b2  9541  1rp  9593  divlt1lt  9660  divle1le  9661  nnledivrp  9702  0elunit  9922  1elunit  9923  divelunit  9938  lincmb01cmp  9939  iccf1o  9940  unitssre  9941  fzpreddisj  10006  fznatpl1  10011  fztpval  10018  qbtwnxr  10193  flqbi2  10226  fldiv4p1lem1div2  10240  flqdiv  10256  reexpcl  10472  reexpclzap  10475  expge0  10491  expge1  10492  expgt1  10493  bernneq  10575  bernneq2  10576  expnbnd  10578  expnlbnd  10579  expnlbnd2  10580  nn0ltexp2  10623  facwordi  10653  faclbnd3  10656  faclbnd6  10657  facavg  10659  cjexp  10835  re1  10839  im1  10840  rei  10841  imi  10842  caucvgre  10923  sqrt1  10988  sqrt2gt1lt2  10991  abs1  11014  caubnd2  11059  mulcn2  11253  reccn2ap  11254  expcnvap0  11443  geo2sum  11455  cvgratnnlemrate  11471  fprodge0  11578  fprodge1  11580  fprodle  11581  ere  11611  ege2le3  11612  efgt1  11638  resin4p  11659  recos4p  11660  sinbnd  11693  cosbnd  11694  sinbnd2  11695  cosbnd2  11696  ef01bndlem  11697  sin01bnd  11698  cos01bnd  11699  cos1bnd  11700  cos2bnd  11701  sin01gt0  11702  cos01gt0  11703  sin02gt0  11704  sincos1sgn  11705  cos12dec  11708  ene1  11725  eap1  11726  halfleoddlt  11831  flodddiv4  11871  isprm3  12050  sqnprm  12068  coprm  12076  phibndlem  12148  pythagtriplem3  12199  fldivp1  12278  pockthi  12288  exmidunben  12359  basendxnmulrndx  12509  setsmsbasg  13119  tgioo  13186  dveflem  13327  reeff1olem  13332  reeff1o  13334  cosz12  13341  sinhalfpilem  13352  tangtx  13399  sincos4thpi  13401  pigt3  13405  coskpi  13409  cos0pilt1  13413  ioocosf1o  13415  loge  13428  logrpap0b  13437  logdivlti  13442  2logb9irrALT  13532  sqrt2cxp2logb9e3  13533  lgsdir  13576  lgsne0  13579  lgsabs1  13580  lgsdinn0  13589  ex-fl  13606  cvgcmp2nlemabs  13911  iooref1o  13913  trilpolemclim  13915  trilpolemcl  13916  trilpolemisumle  13917  trilpolemeq1  13919  trilpolemlt1  13920  apdiff  13927  nconstwlpolemgt0  13942