Theorem 1re 8238

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

Syntax hints:   e. wcel 2202   RRcr 8091   1c1 8093

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

This theorem is referenced by:  0re  8239  1red  8254  1xr  8297  0lt1  8365  peano2re  8374  peano2rem  8505  0reALT  8535  0le1  8720  1le1  8811  inelr  8823  1ap0  8829  eqneg  8971  ltp1  9083  ltm1  9085  recgt0  9089  mulgt1  9102  ltmulgt11  9103  lemulge11  9105  reclt1  9135  recgt1  9136  recgt1i  9137  recp1lt1  9138  recreclt  9139  sup3exmid  9196  cju  9200  peano5nni  9205  nnssre  9206  1nn  9213  nnge1  9225  nnle1eq1  9226  nngt0  9227  nnnlt1  9228  nn1gt1  9236  nngt1ne1  9237  nnrecre  9239  nnrecgt0  9240  nnsub  9241  2re  9272  3re  9276  4re  9279  5re  9281  6re  9283  7re  9285  8re  9287  9re  9289  0le2  9292  2pos  9293  3pos  9296  4pos  9299  5pos  9302  6pos  9303  7pos  9304  8pos  9305  9pos  9306  neg1rr  9308  neg1lt0  9310  1lt2  9372  1lt3  9374  1lt4  9377  1lt5  9381  1lt6  9386  1lt7  9392  1lt8  9399  1lt9  9407  1ne2  9409  1ap2  9410  1le2  9411  1le3  9414  halflt1  9420  iap0  9426  addltmul  9440  elnnnn0c  9506  nn0ge2m1nn  9523  elnnz1  9563  zltp1le  9595  zleltp1  9596  recnz  9634  gtndiv  9636  3halfnz  9638  1lt10  9810  eluzp1m1  9841  eluzp1p1  9843  eluz2b2  9898  1rp  9953  divlt1lt  10020  divle1le  10021  nnledivrp  10062  0elunit  10282  1elunit  10283  divelunit  10298  lincmb01cmp  10299  lincmble  10300  iccf1o  10301  unitssre  10302  fzpreddisj  10368  fznatpl1  10373  fztpval  10380  qbtwnxr  10580  flqbi2  10614  fldiv4p1lem1div2  10628  flqdiv  10646  seqf1oglem1  10844  reexpcl  10881  reexpclzap  10884  expge0  10900  expge1  10901  expgt1  10902  bernneq  10985  bernneq2  10986  expnbnd  10988  expnlbnd  10989  expnlbnd2  10990  nn0ltexp2  11034  facwordi  11065  faclbnd3  11068  faclbnd6  11069  facavg  11071  hashtpglem  11173  lsw0  11227  cjexp  11533  re1  11537  im1  11538  rei  11539  imi  11540  caucvgre  11621  sqrt1  11686  sqrt2gt1lt2  11689  abs1  11712  caubnd2  11757  mulcn2  11952  reccn2ap  11953  expcnvap0  12143  geo2sum  12155  cvgratnnlemrate  12171  fprodge0  12278  fprodge1  12280  fprodle  12281  ere  12311  ege2le3  12312  efgt1  12338  resin4p  12359  recos4p  12360  sinbnd  12393  cosbnd  12394  sinbnd2  12395  cosbnd2  12396  ef01bndlem  12397  sin01bnd  12398  cos01bnd  12399  cos1bnd  12400  cos2bnd  12401  sinltxirr  12402  sin01gt0  12403  cos01gt0  12404  sin02gt0  12405  sincos1sgn  12406  cos12dec  12409  ene1  12426  eap1  12427  3dvds  12505  halfleoddlt  12535  flodddiv4  12577  isprm3  12770  sqnprm  12788  coprm  12796  phibndlem  12868  pythagtriplem3  12920  fldivp1  13001  pockthi  13011  exmidunben  13127  basendxnmulrndx  13297  starvndxnbasendx  13305  scandxnbasendx  13317  vscandxnbasendx  13322  ipndxnbasendx  13335  basendxnocndx  13376  setsmsbasg  15290  tgioo  15365  dveflem  15537  reeff1olem  15582  reeff1o  15584  cosz12  15591  sinhalfpilem  15602  tangtx  15649  sincos4thpi  15651  pigt3  15655  coskpi  15659  cos0pilt1  15663  ioocosf1o  15665  loge  15678  logrpap0b  15687  logdivlti  15692  2logb9irrALT  15785  sqrt2cxp2logb9e3  15786  perfectlem2  15814  lgsdir  15854  lgsne0  15857  lgsabs1  15858  lgsdinn0  15867  gausslemma2dlem0i  15876  lgseisen  15893  2lgslem3  15920  usgrexmpldifpr  16190  konigsberglem2  16430  konigsberglem3  16431  konigsberglem5  16433  ex-fl  16439  cvgcmp2nlemabs  16764  iooref1o  16766  trilpolemclim  16768  trilpolemcl  16769  trilpolemisumle  16770  trilpolemeq1  16772  trilpolemlt1  16773  apdiff  16780  nconstwlpolemgt0  16797