Theorem 1re 7991

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

Syntax hints:   e. wcel 2160   RRcr 7845   1c1 7847

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

This theorem is referenced by:  0re  7992  1red  8007  1xr  8051  0lt1  8119  peano2re  8128  peano2rem  8259  0reALT  8289  0le1  8473  1le1  8564  inelr  8576  1ap0  8582  eqneg  8724  ltp1  8836  ltm1  8838  recgt0  8842  mulgt1  8855  ltmulgt11  8856  lemulge11  8858  reclt1  8888  recgt1  8889  recgt1i  8890  recp1lt1  8891  recreclt  8892  sup3exmid  8949  cju  8953  peano5nni  8957  nnssre  8958  1nn  8965  nnge1  8977  nnle1eq1  8978  nngt0  8979  nnnlt1  8980  nn1gt1  8988  nngt1ne1  8989  nnrecre  8991  nnrecgt0  8992  nnsub  8993  2re  9024  3re  9028  4re  9031  5re  9033  6re  9035  7re  9037  8re  9039  9re  9041  0le2  9044  2pos  9045  3pos  9048  4pos  9051  5pos  9054  6pos  9055  7pos  9056  8pos  9057  9pos  9058  neg1rr  9060  neg1lt0  9062  1lt2  9123  1lt3  9125  1lt4  9128  1lt5  9132  1lt6  9137  1lt7  9143  1lt8  9150  1lt9  9158  1ne2  9160  1ap2  9161  1le2  9162  1le3  9165  halflt1  9171  iap0  9177  addltmul  9190  elnnnn0c  9256  nn0ge2m1nn  9271  elnnz1  9311  zltp1le  9342  zleltp1  9343  recnz  9381  gtndiv  9383  3halfnz  9385  1lt10  9557  eluzp1m1  9587  eluzp1p1  9589  eluz2b2  9639  1rp  9693  divlt1lt  9760  divle1le  9761  nnledivrp  9802  0elunit  10022  1elunit  10023  divelunit  10038  lincmb01cmp  10039  iccf1o  10040  unitssre  10041  fzpreddisj  10107  fznatpl1  10112  fztpval  10119  qbtwnxr  10294  flqbi2  10328  fldiv4p1lem1div2  10342  flqdiv  10358  reexpcl  10577  reexpclzap  10580  expge0  10596  expge1  10597  expgt1  10598  bernneq  10681  bernneq2  10682  expnbnd  10684  expnlbnd  10685  expnlbnd2  10686  nn0ltexp2  10730  facwordi  10761  faclbnd3  10764  faclbnd6  10765  facavg  10767  cjexp  10943  re1  10947  im1  10948  rei  10949  imi  10950  caucvgre  11031  sqrt1  11096  sqrt2gt1lt2  11099  abs1  11122  caubnd2  11167  mulcn2  11361  reccn2ap  11362  expcnvap0  11551  geo2sum  11563  cvgratnnlemrate  11579  fprodge0  11686  fprodge1  11688  fprodle  11689  ere  11719  ege2le3  11720  efgt1  11746  resin4p  11767  recos4p  11768  sinbnd  11801  cosbnd  11802  sinbnd2  11803  cosbnd2  11804  ef01bndlem  11805  sin01bnd  11806  cos01bnd  11807  cos1bnd  11808  cos2bnd  11809  sin01gt0  11810  cos01gt0  11811  sin02gt0  11812  sincos1sgn  11813  cos12dec  11816  ene1  11833  eap1  11834  halfleoddlt  11940  flodddiv4  11980  isprm3  12161  sqnprm  12179  coprm  12187  phibndlem  12259  pythagtriplem3  12310  fldivp1  12391  pockthi  12401  exmidunben  12488  basendxnmulrndx  12656  starvndxnbasendx  12664  scandxnbasendx  12676  vscandxnbasendx  12681  ipndxnbasendx  12694  setsmsbasg  14464  tgioo  14531  dveflem  14672  reeff1olem  14677  reeff1o  14679  cosz12  14686  sinhalfpilem  14697  tangtx  14744  sincos4thpi  14746  pigt3  14750  coskpi  14754  cos0pilt1  14758  ioocosf1o  14760  loge  14773  logrpap0b  14782  logdivlti  14787  2logb9irrALT  14877  sqrt2cxp2logb9e3  14878  lgsdir  14922  lgsne0  14925  lgsabs1  14926  lgsdinn0  14935  ex-fl  14963  cvgcmp2nlemabs  15268  iooref1o  15270  trilpolemclim  15272  trilpolemcl  15273  trilpolemisumle  15274  trilpolemeq1  15276  trilpolemlt1  15277  apdiff  15284  nconstwlpolemgt0  15300