Theorem 1re 8042

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

Syntax hints:   e. wcel 2167   RRcr 7895   1c1 7897

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

This theorem is referenced by:  0re  8043  1red  8058  1xr  8102  0lt1  8170  peano2re  8179  peano2rem  8310  0reALT  8340  0le1  8525  1le1  8616  inelr  8628  1ap0  8634  eqneg  8776  ltp1  8888  ltm1  8890  recgt0  8894  mulgt1  8907  ltmulgt11  8908  lemulge11  8910  reclt1  8940  recgt1  8941  recgt1i  8942  recp1lt1  8943  recreclt  8944  sup3exmid  9001  cju  9005  peano5nni  9010  nnssre  9011  1nn  9018  nnge1  9030  nnle1eq1  9031  nngt0  9032  nnnlt1  9033  nn1gt1  9041  nngt1ne1  9042  nnrecre  9044  nnrecgt0  9045  nnsub  9046  2re  9077  3re  9081  4re  9084  5re  9086  6re  9088  7re  9090  8re  9092  9re  9094  0le2  9097  2pos  9098  3pos  9101  4pos  9104  5pos  9107  6pos  9108  7pos  9109  8pos  9110  9pos  9111  neg1rr  9113  neg1lt0  9115  1lt2  9177  1lt3  9179  1lt4  9182  1lt5  9186  1lt6  9191  1lt7  9197  1lt8  9204  1lt9  9212  1ne2  9214  1ap2  9215  1le2  9216  1le3  9219  halflt1  9225  iap0  9231  addltmul  9245  elnnnn0c  9311  nn0ge2m1nn  9326  elnnz1  9366  zltp1le  9397  zleltp1  9398  recnz  9436  gtndiv  9438  3halfnz  9440  1lt10  9612  eluzp1m1  9642  eluzp1p1  9644  eluz2b2  9694  1rp  9749  divlt1lt  9816  divle1le  9817  nnledivrp  9858  0elunit  10078  1elunit  10079  divelunit  10094  lincmb01cmp  10095  iccf1o  10096  unitssre  10097  fzpreddisj  10163  fznatpl1  10168  fztpval  10175  qbtwnxr  10364  flqbi2  10398  fldiv4p1lem1div2  10412  flqdiv  10430  seqf1oglem1  10628  reexpcl  10665  reexpclzap  10668  expge0  10684  expge1  10685  expgt1  10686  bernneq  10769  bernneq2  10770  expnbnd  10772  expnlbnd  10773  expnlbnd2  10774  nn0ltexp2  10818  facwordi  10849  faclbnd3  10852  faclbnd6  10853  facavg  10855  cjexp  11075  re1  11079  im1  11080  rei  11081  imi  11082  caucvgre  11163  sqrt1  11228  sqrt2gt1lt2  11231  abs1  11254  caubnd2  11299  mulcn2  11494  reccn2ap  11495  expcnvap0  11684  geo2sum  11696  cvgratnnlemrate  11712  fprodge0  11819  fprodge1  11821  fprodle  11822  ere  11852  ege2le3  11853  efgt1  11879  resin4p  11900  recos4p  11901  sinbnd  11934  cosbnd  11935  sinbnd2  11936  cosbnd2  11937  ef01bndlem  11938  sin01bnd  11939  cos01bnd  11940  cos1bnd  11941  cos2bnd  11942  sinltxirr  11943  sin01gt0  11944  cos01gt0  11945  sin02gt0  11946  sincos1sgn  11947  cos12dec  11950  ene1  11967  eap1  11968  3dvds  12046  halfleoddlt  12076  flodddiv4  12118  isprm3  12311  sqnprm  12329  coprm  12337  phibndlem  12409  pythagtriplem3  12461  fldivp1  12542  pockthi  12552  exmidunben  12668  basendxnmulrndx  12836  starvndxnbasendx  12844  scandxnbasendx  12856  vscandxnbasendx  12861  ipndxnbasendx  12874  basendxnocndx  12915  setsmsbasg  14799  tgioo  14874  dveflem  15046  reeff1olem  15091  reeff1o  15093  cosz12  15100  sinhalfpilem  15111  tangtx  15158  sincos4thpi  15160  pigt3  15164  coskpi  15168  cos0pilt1  15172  ioocosf1o  15174  loge  15187  logrpap0b  15196  logdivlti  15201  2logb9irrALT  15294  sqrt2cxp2logb9e3  15295  perfectlem2  15320  lgsdir  15360  lgsne0  15363  lgsabs1  15364  lgsdinn0  15373  gausslemma2dlem0i  15382  lgseisen  15399  2lgslem3  15426  ex-fl  15455  cvgcmp2nlemabs  15763  iooref1o  15765  trilpolemclim  15767  trilpolemcl  15768  trilpolemisumle  15769  trilpolemeq1  15771  trilpolemlt1  15772  apdiff  15779  nconstwlpolemgt0  15795