Theorem 1re 7889

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

Syntax hints:   e. wcel 2135   RRcr 7743   1c1 7745

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

This theorem is referenced by:  0re  7890  1red  7905  1xr  7948  0lt1  8016  peano2re  8025  peano2rem  8156  0reALT  8186  0le1  8370  1le1  8461  inelr  8473  1ap0  8479  eqneg  8619  ltp1  8730  ltm1  8732  recgt0  8736  mulgt1  8749  ltmulgt11  8750  lemulge11  8752  reclt1  8782  recgt1  8783  recgt1i  8784  recp1lt1  8785  recreclt  8786  sup3exmid  8843  cju  8847  peano5nni  8851  nnssre  8852  1nn  8859  nnge1  8871  nnle1eq1  8872  nngt0  8873  nnnlt1  8874  nn1gt1  8882  nngt1ne1  8883  nnrecre  8885  nnrecgt0  8886  nnsub  8887  2re  8918  3re  8922  4re  8925  5re  8927  6re  8929  7re  8931  8re  8933  9re  8935  0le2  8938  2pos  8939  3pos  8942  4pos  8945  5pos  8948  6pos  8949  7pos  8950  8pos  8951  9pos  8952  neg1rr  8954  neg1lt0  8956  1lt2  9017  1lt3  9019  1lt4  9022  1lt5  9026  1lt6  9031  1lt7  9037  1lt8  9044  1lt9  9052  1ne2  9054  1ap2  9055  1le2  9056  1le3  9059  halflt1  9065  iap0  9071  addltmul  9084  elnnnn0c  9150  nn0ge2m1nn  9165  elnnz1  9205  zltp1le  9236  zleltp1  9237  recnz  9275  gtndiv  9277  3halfnz  9279  1lt10  9451  eluzp1m1  9480  eluzp1p1  9482  eluz2b2  9532  1rp  9584  divlt1lt  9651  divle1le  9652  nnledivrp  9693  0elunit  9913  1elunit  9914  divelunit  9929  lincmb01cmp  9930  iccf1o  9931  unitssre  9932  fzpreddisj  9996  fznatpl1  10001  fztpval  10008  qbtwnxr  10183  flqbi2  10216  fldiv4p1lem1div2  10230  flqdiv  10246  reexpcl  10462  reexpclzap  10465  expge0  10481  expge1  10482  expgt1  10483  bernneq  10564  bernneq2  10565  expnbnd  10567  expnlbnd  10568  expnlbnd2  10569  nn0ltexp2  10612  facwordi  10642  faclbnd3  10645  faclbnd6  10646  facavg  10648  cjexp  10821  re1  10825  im1  10826  rei  10827  imi  10828  caucvgre  10909  sqrt1  10974  sqrt2gt1lt2  10977  abs1  11000  caubnd2  11045  mulcn2  11239  reccn2ap  11240  expcnvap0  11429  geo2sum  11441  cvgratnnlemrate  11457  fprodge0  11564  fprodge1  11566  fprodle  11567  ere  11597  ege2le3  11598  efgt1  11624  resin4p  11645  recos4p  11646  sinbnd  11679  cosbnd  11680  sinbnd2  11681  cosbnd2  11682  ef01bndlem  11683  sin01bnd  11684  cos01bnd  11685  cos1bnd  11686  cos2bnd  11687  sin01gt0  11688  cos01gt0  11689  sin02gt0  11690  sincos1sgn  11691  cos12dec  11694  ene1  11711  eap1  11712  halfleoddlt  11816  flodddiv4  11856  isprm3  12029  sqnprm  12047  coprm  12053  phibndlem  12125  pythagtriplem3  12176  fldivp1  12255  exmidunben  12296  basendxnmulrndx  12445  setsmsbasg  13020  tgioo  13087  dveflem  13228  reeff1olem  13233  reeff1o  13235  cosz12  13242  sinhalfpilem  13253  tangtx  13300  sincos4thpi  13302  pigt3  13306  coskpi  13310  cos0pilt1  13314  ioocosf1o  13316  loge  13329  logrpap0b  13338  logdivlti  13343  2logb9irrALT  13433  sqrt2cxp2logb9e3  13434  ex-fl  13443  cvgcmp2nlemabs  13745  iooref1o  13747  trilpolemclim  13749  trilpolemcl  13750  trilpolemisumle  13751  trilpolemeq1  13753  trilpolemlt1  13754  apdiff  13761  nconstwlpolemgt0  13776