Theorem 1re 8289

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

Syntax hints:   e. wcel 2205   RRcr 8142   1c1 8144

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

This theorem is referenced by:  0re  8290  1red  8305  1xr  8348  0lt1  8416  peano2re  8425  peano2rem  8556  0reALT  8586  0le1  8772  1le1  8863  inelr  8875  1ap0  8881  eqneg  9023  ltp1  9135  ltm1  9137  recgt0  9141  mulgt1  9154  ltmulgt11  9155  lemulge11  9157  reclt1  9187  recgt1  9188  recgt1i  9189  recp1lt1  9190  recreclt  9191  sup3exmid  9248  cju  9252  peano5nni  9257  nnssre  9258  1nn  9265  nnge1  9277  nnle1eq1  9278  nngt0  9279  nnnlt1  9280  nn1gt1  9288  nngt1ne1  9289  nnrecre  9291  nnrecgt0  9292  nnsub  9293  2re  9324  3re  9328  4re  9331  5re  9333  6re  9335  7re  9337  8re  9339  9re  9341  0le2  9344  2pos  9345  3pos  9348  4pos  9351  5pos  9354  6pos  9355  7pos  9356  8pos  9357  9pos  9358  neg1rr  9360  neg1lt0  9362  1lt2  9424  1lt3  9426  1lt4  9429  1lt5  9433  1lt6  9438  1lt7  9444  1lt8  9451  1lt9  9459  1ne2  9461  1ap2  9462  1le2  9463  1le3  9466  halflt1  9472  iap0  9478  addltmul  9492  elnnnn0c  9558  nn0ge2m1nn  9577  elnnz1  9617  zltp1le  9649  zleltp1  9650  recnz  9689  gtndiv  9691  3halfnz  9693  1lt10  9865  eluzp1m1  9896  eluzp1p1  9898  eluz2b2  9953  1rp  10008  divlt1lt  10075  divle1le  10076  nnledivrp  10117  0elunit  10338  1elunit  10339  divelunit  10354  lincmb01cmp  10355  lincmble  10356  iccf1o  10357  unitssre  10358  fzpreddisj  10427  fznatpl1  10432  fztpval  10439  qbtwnxr  10641  flqbi2  10675  fldiv4p1lem1div2  10689  flqdiv  10707  seqf1oglem1  10905  reexpcl  10942  reexpclzap  10945  expge0  10961  expge1  10962  expgt1  10963  resq01  11044  bernneq  11047  bernneq2  11048  expnbnd  11050  expnlbnd  11051  expnlbnd2  11052  nn0ltexp2  11096  facwordi  11127  faclbnd3  11130  faclbnd6  11131  facavg  11133  hashtpglem  11243  lsw0  11297  cjexp  11603  re1  11607  im1  11608  rei  11609  imi  11610  caucvgre  11691  sqrt1  11756  sqrt2gt1lt2  11759  abs1  11782  caubnd2  11827  mulcn2  12022  reccn2ap  12023  expcnvap0  12213  geo2sum  12225  cvgratnnlemrate  12241  fprodge0  12348  fprodge1  12350  fprodle  12351  ere  12381  ege2le3  12382  efgt1  12408  resin4p  12429  recos4p  12430  sinbnd  12463  cosbnd  12464  sinbnd2  12465  cosbnd2  12466  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  cos1bnd  12470  cos2bnd  12471  sinltxirr  12472  sin01gt0  12473  cos01gt0  12474  sin02gt0  12475  sincos1sgn  12476  cos12dec  12479  ene1  12496  eap1  12497  3dvds  12575  halfleoddlt  12605  flodddiv4  12647  isprm3  12840  sqnprm  12858  coprm  12866  phibndlem  12938  pythagtriplem3  12990  fldivp1  13071  pockthi  13081  ballotfilem2  13172  ballotfilem4  13185  ballotfilemi1  13189  ballotfilemic  13194  exmidunben  13261  basendxnmulrndx  13431  starvndxnbasendx  13439  scandxnbasendx  13451  vscandxnbasendx  13456  ipndxnbasendx  13469  basendxnocndx  13510  setsmsbasg  15470  tgioo  15545  dveflem  15717  reeff1olem  15762  reeff1o  15764  cosz12  15771  sinhalfpilem  15782  tangtx  15829  sincos4thpi  15831  pigt3  15835  coskpi  15839  cos0pilt1  15843  ioocosf1o  15845  loge  15858  logrpap0b  15867  logdivlti  15872  2logb9irrALT  15965  sqrt2cxp2logb9e3  15966  perfectlem2  15994  lgsdir  16034  lgsne0  16037  lgsabs1  16038  lgsdinn0  16047  gausslemma2dlem0i  16056  lgseisen  16073  2lgslem3  16100  usgrexmpldifpr  16370  konigsberglem2  16610  konigsberglem3  16611  konigsberglem5  16613  ex-fl  16619  cvgcmp2nlemabs  16942  iooref1o  16944  trilpolemclim  16946  trilpolemcl  16947  trilpolemisumle  16948  trilpolemeq1  16950  trilpolemlt1  16951  apdiff  16958  nconstwlpolemgt0  16976