Theorem 1re 8071

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

Syntax hints:   e. wcel 2176   RRcr 7924   1c1 7926

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

This theorem is referenced by:  0re  8072  1red  8087  1xr  8131  0lt1  8199  peano2re  8208  peano2rem  8339  0reALT  8369  0le1  8554  1le1  8645  inelr  8657  1ap0  8663  eqneg  8805  ltp1  8917  ltm1  8919  recgt0  8923  mulgt1  8936  ltmulgt11  8937  lemulge11  8939  reclt1  8969  recgt1  8970  recgt1i  8971  recp1lt1  8972  recreclt  8973  sup3exmid  9030  cju  9034  peano5nni  9039  nnssre  9040  1nn  9047  nnge1  9059  nnle1eq1  9060  nngt0  9061  nnnlt1  9062  nn1gt1  9070  nngt1ne1  9071  nnrecre  9073  nnrecgt0  9074  nnsub  9075  2re  9106  3re  9110  4re  9113  5re  9115  6re  9117  7re  9119  8re  9121  9re  9123  0le2  9126  2pos  9127  3pos  9130  4pos  9133  5pos  9136  6pos  9137  7pos  9138  8pos  9139  9pos  9140  neg1rr  9142  neg1lt0  9144  1lt2  9206  1lt3  9208  1lt4  9211  1lt5  9215  1lt6  9220  1lt7  9226  1lt8  9233  1lt9  9241  1ne2  9243  1ap2  9244  1le2  9245  1le3  9248  halflt1  9254  iap0  9260  addltmul  9274  elnnnn0c  9340  nn0ge2m1nn  9355  elnnz1  9395  zltp1le  9427  zleltp1  9428  recnz  9466  gtndiv  9468  3halfnz  9470  1lt10  9642  eluzp1m1  9672  eluzp1p1  9674  eluz2b2  9724  1rp  9779  divlt1lt  9846  divle1le  9847  nnledivrp  9888  0elunit  10108  1elunit  10109  divelunit  10124  lincmb01cmp  10125  iccf1o  10126  unitssre  10127  fzpreddisj  10193  fznatpl1  10198  fztpval  10205  qbtwnxr  10400  flqbi2  10434  fldiv4p1lem1div2  10448  flqdiv  10466  seqf1oglem1  10664  reexpcl  10701  reexpclzap  10704  expge0  10720  expge1  10721  expgt1  10722  bernneq  10805  bernneq2  10806  expnbnd  10808  expnlbnd  10809  expnlbnd2  10810  nn0ltexp2  10854  facwordi  10885  faclbnd3  10888  faclbnd6  10889  facavg  10891  lsw0  11041  cjexp  11204  re1  11208  im1  11209  rei  11210  imi  11211  caucvgre  11292  sqrt1  11357  sqrt2gt1lt2  11360  abs1  11383  caubnd2  11428  mulcn2  11623  reccn2ap  11624  expcnvap0  11813  geo2sum  11825  cvgratnnlemrate  11841  fprodge0  11948  fprodge1  11950  fprodle  11951  ere  11981  ege2le3  11982  efgt1  12008  resin4p  12029  recos4p  12030  sinbnd  12063  cosbnd  12064  sinbnd2  12065  cosbnd2  12066  ef01bndlem  12067  sin01bnd  12068  cos01bnd  12069  cos1bnd  12070  cos2bnd  12071  sinltxirr  12072  sin01gt0  12073  cos01gt0  12074  sin02gt0  12075  sincos1sgn  12076  cos12dec  12079  ene1  12096  eap1  12097  3dvds  12175  halfleoddlt  12205  flodddiv4  12247  isprm3  12440  sqnprm  12458  coprm  12466  phibndlem  12538  pythagtriplem3  12590  fldivp1  12671  pockthi  12681  exmidunben  12797  basendxnmulrndx  12966  starvndxnbasendx  12974  scandxnbasendx  12986  vscandxnbasendx  12991  ipndxnbasendx  13004  basendxnocndx  13045  setsmsbasg  14951  tgioo  15026  dveflem  15198  reeff1olem  15243  reeff1o  15245  cosz12  15252  sinhalfpilem  15263  tangtx  15310  sincos4thpi  15312  pigt3  15316  coskpi  15320  cos0pilt1  15324  ioocosf1o  15326  loge  15339  logrpap0b  15348  logdivlti  15353  2logb9irrALT  15446  sqrt2cxp2logb9e3  15447  perfectlem2  15472  lgsdir  15512  lgsne0  15515  lgsabs1  15516  lgsdinn0  15525  gausslemma2dlem0i  15534  lgseisen  15551  2lgslem3  15578  ex-fl  15665  cvgcmp2nlemabs  15975  iooref1o  15977  trilpolemclim  15979  trilpolemcl  15980  trilpolemisumle  15981  trilpolemeq1  15983  trilpolemlt1  15984  apdiff  15991  nconstwlpolemgt0  16007