Theorem 1re 8319

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

This proof depends on syntax axioms:   e. wcel 2209   RRcr 8172   1c1 8174

This proof depends on axioms:  ax-1re 8267

This theorem is used by:  0re  8320  1red  8335  1xr  8378  0lt1  8447  peano2re  8456  peano2rem  8587  0reALT  8617  0le1  8803  1le1  8894  inelr  8906  1ap0  8912  eqneg  9056  ltp1  9168  ltm1  9170  recgt0  9174  mulgt1  9187  ltmulgt11  9188  lemulge11  9190  reclt1  9220  recgt1  9221  recgt1i  9222  recp1lt1  9223  recreclt  9224  sup3exmid  9281  cju  9285  peano5nni  9290  nnssre  9291  1nn  9298  nnge1  9310  nnle1eq1  9311  nngt0  9312  nnnlt1  9313  nn1gt1  9321  nngt1ne1  9322  nnrecre  9324  nnrecgt0  9325  nnsub  9326  2re  9357  3re  9361  4re  9364  5re  9366  6re  9368  7re  9370  8re  9372  9re  9374  0le2  9377  2pos  9378  3pos  9381  4pos  9384  5pos  9387  6pos  9388  7pos  9389  8pos  9390  9pos  9391  neg1rr  9393  neg1lt0  9395  1lt2  9457  1lt3  9459  1lt4  9462  1lt5  9466  1lt6  9471  1lt7  9477  1lt8  9484  1lt9  9492  1ne2  9494  1ap2  9495  1le2  9496  1le3  9499  halflt1  9505  iap0  9511  addltmul  9525  elnnnn0c  9591  nn0ge2m1nn  9610  elnnz1  9650  zltp1le  9682  zleltp1  9683  recnz  9722  gtndiv  9724  3halfnz  9726  1lt10  9898  eluzp1m1  9929  eluzp1p1  9931  eluz2b2  9986  1rp  10041  divlt1lt  10108  divle1le  10109  nnledivrp  10150  0elunit  10371  1elunit  10372  divelunit  10387  lincmb01cmp  10388  lincmble  10389  iccf1o  10390  unitssre  10391  fzpreddisj  10461  fznatpl1  10466  fztpval  10473  qbtwnxr  10675  flqbi2  10709  fldiv4p1lem1div2  10723  flqdiv  10741  seqf1oglem1  10939  reexpcl  10976  reexpclzap  10979  expge0  10995  expge1  10996  expgt1  10997  resq01  11078  bernneq  11081  bernneq2  11082  expnbnd  11084  expnlbnd  11085  expnlbnd2  11086  nn0ltexp2  11130  facwordi  11161  faclbnd3  11164  faclbnd6  11165  facavg  11167  hashtpglem  11281  lsw0  11335  cjexp  11641  re1  11646  im1  11647  rei  11648  imi  11649  caucvgre  11730  sqrt1  11795  sqrt2gt1lt2  11798  abs1  11821  caubnd2  11866  mulcn2  12061  reccn2ap  12062  expcnvap0  12252  geo2sum  12264  cvgratnnlemrate  12280  fprodge0  12387  fprodge1  12389  fprodle  12390  ere  12420  ege2le3  12421  efgt1  12447  resin4p  12468  recos4p  12469  sinbnd  12502  cosbnd  12503  sinbnd2  12504  cosbnd2  12505  ef01bndlem  12506  sin01bnd  12507  cos01bnd  12508  cos1bnd  12509  cos2bnd  12510  sinltxirr  12511  sin01gt0  12512  cos01gt0  12513  sin02gt0  12514  sincos1sgn  12515  cos12dec  12518  ene1  12535  eap1  12536  3dvds  12614  halfleoddlt  12644  flodddiv4  12686  isprm3  12879  sqnprm  12897  coprm  12905  phibndlem  12977  pythagtriplem3  13029  fldivp1  13110  pockthi  13120  ballotfilem2  13211  ballotfilem4  13224  ballotfilemi1  13228  ballotfilemic  13233  exmidunben  13300  basendxnmulrndx  13471  starvndxnbasendx  13479  scandxnbasendx  13491  vscandxnbasendx  13496  ipndxnbasendx  13509  basendxnocndx  13550  setsmsbasg  15563  tgioo  15638  dveflem  15810  reeff1olem  15855  reeff1o  15857  cosz12  15864  sinhalfpilem  15875  tangtx  15922  sincos4thpi  15924  pigt3  15928  coskpi  15932  cos0pilt1  15936  ioocosf1o  15938  loge  15951  logrpap0b  15960  logdivlti  15965  2logb9irrALT  16059  sqrt2cxp2logb9e3  16060  birthdaylem3  16072  perfectlem2  16097  lgsdir  16137  lgsne0  16140  lgsabs1  16141  lgsdinn0  16150  gausslemma2dlem0i  16159  lgseisen  16176  2lgslem3  16203  usgrexmpldifpr  16473  konigsberglem2  16713  konigsberglem3  16714  konigsberglem5  16716  ex-fl  16722  cvgcmp2nlemabs  17056  iooref1o  17058  trilpolemclim  17060  trilpolemcl  17061  trilpolemisumle  17062  trilpolemeq1  17064  trilpolemlt1  17065  apdiff  17072  nconstwlpolemgt0  17089