Theorem 1re 7923

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 7872	1 |- 1 e. RR

Syntax hints:   e. wcel 2142   RRcr 7777   1c1 7779

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

This theorem is referenced by:  0re  7924  1red  7939  1xr  7982  0lt1  8050  peano2re  8059  peano2rem  8190  0reALT  8220  0le1  8404  1le1  8495  inelr  8507  1ap0  8513  eqneg  8653  ltp1  8764  ltm1  8766  recgt0  8770  mulgt1  8783  ltmulgt11  8784  lemulge11  8786  reclt1  8816  recgt1  8817  recgt1i  8818  recp1lt1  8819  recreclt  8820  sup3exmid  8877  cju  8881  peano5nni  8885  nnssre  8886  1nn  8893  nnge1  8905  nnle1eq1  8906  nngt0  8907  nnnlt1  8908  nn1gt1  8916  nngt1ne1  8917  nnrecre  8919  nnrecgt0  8920  nnsub  8921  2re  8952  3re  8956  4re  8959  5re  8961  6re  8963  7re  8965  8re  8967  9re  8969  0le2  8972  2pos  8973  3pos  8976  4pos  8979  5pos  8982  6pos  8983  7pos  8984  8pos  8985  9pos  8986  neg1rr  8988  neg1lt0  8990  1lt2  9051  1lt3  9053  1lt4  9056  1lt5  9060  1lt6  9065  1lt7  9071  1lt8  9078  1lt9  9086  1ne2  9088  1ap2  9089  1le2  9090  1le3  9093  halflt1  9099  iap0  9105  addltmul  9118  elnnnn0c  9184  nn0ge2m1nn  9199  elnnz1  9239  zltp1le  9270  zleltp1  9271  recnz  9309  gtndiv  9311  3halfnz  9313  1lt10  9485  eluzp1m1  9514  eluzp1p1  9516  eluz2b2  9566  1rp  9618  divlt1lt  9685  divle1le  9686  nnledivrp  9727  0elunit  9947  1elunit  9948  divelunit  9963  lincmb01cmp  9964  iccf1o  9965  unitssre  9966  fzpreddisj  10031  fznatpl1  10036  fztpval  10043  qbtwnxr  10218  flqbi2  10251  fldiv4p1lem1div2  10265  flqdiv  10281  reexpcl  10497  reexpclzap  10500  expge0  10516  expge1  10517  expgt1  10518  bernneq  10600  bernneq2  10601  expnbnd  10603  expnlbnd  10604  expnlbnd2  10605  nn0ltexp2  10648  facwordi  10678  faclbnd3  10681  faclbnd6  10682  facavg  10684  cjexp  10861  re1  10865  im1  10866  rei  10867  imi  10868  caucvgre  10949  sqrt1  11014  sqrt2gt1lt2  11017  abs1  11040  caubnd2  11085  mulcn2  11279  reccn2ap  11280  expcnvap0  11469  geo2sum  11481  cvgratnnlemrate  11497  fprodge0  11604  fprodge1  11606  fprodle  11607  ere  11637  ege2le3  11638  efgt1  11664  resin4p  11685  recos4p  11686  sinbnd  11719  cosbnd  11720  sinbnd2  11721  cosbnd2  11722  ef01bndlem  11723  sin01bnd  11724  cos01bnd  11725  cos1bnd  11726  cos2bnd  11727  sin01gt0  11728  cos01gt0  11729  sin02gt0  11730  sincos1sgn  11731  cos12dec  11734  ene1  11751  eap1  11752  halfleoddlt  11857  flodddiv4  11897  isprm3  12076  sqnprm  12094  coprm  12102  phibndlem  12174  pythagtriplem3  12225  fldivp1  12304  pockthi  12314  exmidunben  12385  basendxnmulrndx  12536  setsmsbasg  13358  tgioo  13425  dveflem  13566  reeff1olem  13571  reeff1o  13573  cosz12  13580  sinhalfpilem  13591  tangtx  13638  sincos4thpi  13640  pigt3  13644  coskpi  13648  cos0pilt1  13652  ioocosf1o  13654  loge  13667  logrpap0b  13676  logdivlti  13681  2logb9irrALT  13771  sqrt2cxp2logb9e3  13772  lgsdir  13815  lgsne0  13818  lgsabs1  13819  lgsdinn0  13828  ex-fl  13845  cvgcmp2nlemabs  14149  iooref1o  14151  trilpolemclim  14153  trilpolemcl  14154  trilpolemisumle  14155  trilpolemeq1  14157  trilpolemlt1  14158  apdiff  14165  nconstwlpolemgt0  14180