Theorem 1re 8025

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

Syntax hints:   e. wcel 2167   RRcr 7878   1c1 7880

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

This theorem is referenced by:  0re  8026  1red  8041  1xr  8085  0lt1  8153  peano2re  8162  peano2rem  8293  0reALT  8323  0le1  8508  1le1  8599  inelr  8611  1ap0  8617  eqneg  8759  ltp1  8871  ltm1  8873  recgt0  8877  mulgt1  8890  ltmulgt11  8891  lemulge11  8893  reclt1  8923  recgt1  8924  recgt1i  8925  recp1lt1  8926  recreclt  8927  sup3exmid  8984  cju  8988  peano5nni  8993  nnssre  8994  1nn  9001  nnge1  9013  nnle1eq1  9014  nngt0  9015  nnnlt1  9016  nn1gt1  9024  nngt1ne1  9025  nnrecre  9027  nnrecgt0  9028  nnsub  9029  2re  9060  3re  9064  4re  9067  5re  9069  6re  9071  7re  9073  8re  9075  9re  9077  0le2  9080  2pos  9081  3pos  9084  4pos  9087  5pos  9090  6pos  9091  7pos  9092  8pos  9093  9pos  9094  neg1rr  9096  neg1lt0  9098  1lt2  9160  1lt3  9162  1lt4  9165  1lt5  9169  1lt6  9174  1lt7  9180  1lt8  9187  1lt9  9195  1ne2  9197  1ap2  9198  1le2  9199  1le3  9202  halflt1  9208  iap0  9214  addltmul  9228  elnnnn0c  9294  nn0ge2m1nn  9309  elnnz1  9349  zltp1le  9380  zleltp1  9381  recnz  9419  gtndiv  9421  3halfnz  9423  1lt10  9595  eluzp1m1  9625  eluzp1p1  9627  eluz2b2  9677  1rp  9732  divlt1lt  9799  divle1le  9800  nnledivrp  9841  0elunit  10061  1elunit  10062  divelunit  10077  lincmb01cmp  10078  iccf1o  10079  unitssre  10080  fzpreddisj  10146  fznatpl1  10151  fztpval  10158  qbtwnxr  10347  flqbi2  10381  fldiv4p1lem1div2  10395  flqdiv  10413  seqf1oglem1  10611  reexpcl  10648  reexpclzap  10651  expge0  10667  expge1  10668  expgt1  10669  bernneq  10752  bernneq2  10753  expnbnd  10755  expnlbnd  10756  expnlbnd2  10757  nn0ltexp2  10801  facwordi  10832  faclbnd3  10835  faclbnd6  10836  facavg  10838  cjexp  11058  re1  11062  im1  11063  rei  11064  imi  11065  caucvgre  11146  sqrt1  11211  sqrt2gt1lt2  11214  abs1  11237  caubnd2  11282  mulcn2  11477  reccn2ap  11478  expcnvap0  11667  geo2sum  11679  cvgratnnlemrate  11695  fprodge0  11802  fprodge1  11804  fprodle  11805  ere  11835  ege2le3  11836  efgt1  11862  resin4p  11883  recos4p  11884  sinbnd  11917  cosbnd  11918  sinbnd2  11919  cosbnd2  11920  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  cos1bnd  11924  cos2bnd  11925  sinltxirr  11926  sin01gt0  11927  cos01gt0  11928  sin02gt0  11929  sincos1sgn  11930  cos12dec  11933  ene1  11950  eap1  11951  3dvds  12029  halfleoddlt  12059  flodddiv4  12101  isprm3  12286  sqnprm  12304  coprm  12312  phibndlem  12384  pythagtriplem3  12436  fldivp1  12517  pockthi  12527  exmidunben  12643  basendxnmulrndx  12811  starvndxnbasendx  12819  scandxnbasendx  12831  vscandxnbasendx  12836  ipndxnbasendx  12849  setsmsbasg  14715  tgioo  14790  dveflem  14962  reeff1olem  15007  reeff1o  15009  cosz12  15016  sinhalfpilem  15027  tangtx  15074  sincos4thpi  15076  pigt3  15080  coskpi  15084  cos0pilt1  15088  ioocosf1o  15090  loge  15103  logrpap0b  15112  logdivlti  15117  2logb9irrALT  15210  sqrt2cxp2logb9e3  15211  perfectlem2  15236  lgsdir  15276  lgsne0  15279  lgsabs1  15280  lgsdinn0  15289  gausslemma2dlem0i  15298  lgseisen  15315  2lgslem3  15342  ex-fl  15371  cvgcmp2nlemabs  15676  iooref1o  15678  trilpolemclim  15680  trilpolemcl  15681  trilpolemisumle  15682  trilpolemeq1  15684  trilpolemlt1  15685  apdiff  15692  nconstwlpolemgt0  15708