Theorem 1re 7931

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

Syntax hints:   e. wcel 2146   RRcr 7785   1c1 7787

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

This theorem is referenced by:  0re  7932  1red  7947  1xr  7990  0lt1  8058  peano2re  8067  peano2rem  8198  0reALT  8228  0le1  8412  1le1  8503  inelr  8515  1ap0  8521  eqneg  8661  ltp1  8772  ltm1  8774  recgt0  8778  mulgt1  8791  ltmulgt11  8792  lemulge11  8794  reclt1  8824  recgt1  8825  recgt1i  8826  recp1lt1  8827  recreclt  8828  sup3exmid  8885  cju  8889  peano5nni  8893  nnssre  8894  1nn  8901  nnge1  8913  nnle1eq1  8914  nngt0  8915  nnnlt1  8916  nn1gt1  8924  nngt1ne1  8925  nnrecre  8927  nnrecgt0  8928  nnsub  8929  2re  8960  3re  8964  4re  8967  5re  8969  6re  8971  7re  8973  8re  8975  9re  8977  0le2  8980  2pos  8981  3pos  8984  4pos  8987  5pos  8990  6pos  8991  7pos  8992  8pos  8993  9pos  8994  neg1rr  8996  neg1lt0  8998  1lt2  9059  1lt3  9061  1lt4  9064  1lt5  9068  1lt6  9073  1lt7  9079  1lt8  9086  1lt9  9094  1ne2  9096  1ap2  9097  1le2  9098  1le3  9101  halflt1  9107  iap0  9113  addltmul  9126  elnnnn0c  9192  nn0ge2m1nn  9207  elnnz1  9247  zltp1le  9278  zleltp1  9279  recnz  9317  gtndiv  9319  3halfnz  9321  1lt10  9493  eluzp1m1  9522  eluzp1p1  9524  eluz2b2  9574  1rp  9626  divlt1lt  9693  divle1le  9694  nnledivrp  9735  0elunit  9955  1elunit  9956  divelunit  9971  lincmb01cmp  9972  iccf1o  9973  unitssre  9974  fzpreddisj  10039  fznatpl1  10044  fztpval  10051  qbtwnxr  10226  flqbi2  10259  fldiv4p1lem1div2  10273  flqdiv  10289  reexpcl  10505  reexpclzap  10508  expge0  10524  expge1  10525  expgt1  10526  bernneq  10608  bernneq2  10609  expnbnd  10611  expnlbnd  10612  expnlbnd2  10613  nn0ltexp2  10656  facwordi  10686  faclbnd3  10689  faclbnd6  10690  facavg  10692  cjexp  10868  re1  10872  im1  10873  rei  10874  imi  10875  caucvgre  10956  sqrt1  11021  sqrt2gt1lt2  11024  abs1  11047  caubnd2  11092  mulcn2  11286  reccn2ap  11287  expcnvap0  11476  geo2sum  11488  cvgratnnlemrate  11504  fprodge0  11611  fprodge1  11613  fprodle  11614  ere  11644  ege2le3  11645  efgt1  11671  resin4p  11692  recos4p  11693  sinbnd  11726  cosbnd  11727  sinbnd2  11728  cosbnd2  11729  ef01bndlem  11730  sin01bnd  11731  cos01bnd  11732  cos1bnd  11733  cos2bnd  11734  sin01gt0  11735  cos01gt0  11736  sin02gt0  11737  sincos1sgn  11738  cos12dec  11741  ene1  11758  eap1  11759  halfleoddlt  11864  flodddiv4  11904  isprm3  12083  sqnprm  12101  coprm  12109  phibndlem  12181  pythagtriplem3  12232  fldivp1  12311  pockthi  12321  exmidunben  12392  basendxnmulrndx  12543  scandxnbasendx  12559  setsmsbasg  13530  tgioo  13597  dveflem  13738  reeff1olem  13743  reeff1o  13745  cosz12  13752  sinhalfpilem  13763  tangtx  13810  sincos4thpi  13812  pigt3  13816  coskpi  13820  cos0pilt1  13824  ioocosf1o  13826  loge  13839  logrpap0b  13848  logdivlti  13853  2logb9irrALT  13943  sqrt2cxp2logb9e3  13944  lgsdir  13987  lgsne0  13990  lgsabs1  13991  lgsdinn0  14000  ex-fl  14017  cvgcmp2nlemabs  14321  iooref1o  14323  trilpolemclim  14325  trilpolemcl  14326  trilpolemisumle  14327  trilpolemeq1  14329  trilpolemlt1  14330  apdiff  14337  nconstwlpolemgt0  14352