Theorem 1re 7956

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

Syntax hints:   e. wcel 2148   RRcr 7810   1c1 7812

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

This theorem is referenced by:  0re  7957  1red  7972  1xr  8016  0lt1  8084  peano2re  8093  peano2rem  8224  0reALT  8254  0le1  8438  1le1  8529  inelr  8541  1ap0  8547  eqneg  8689  ltp1  8801  ltm1  8803  recgt0  8807  mulgt1  8820  ltmulgt11  8821  lemulge11  8823  reclt1  8853  recgt1  8854  recgt1i  8855  recp1lt1  8856  recreclt  8857  sup3exmid  8914  cju  8918  peano5nni  8922  nnssre  8923  1nn  8930  nnge1  8942  nnle1eq1  8943  nngt0  8944  nnnlt1  8945  nn1gt1  8953  nngt1ne1  8954  nnrecre  8956  nnrecgt0  8957  nnsub  8958  2re  8989  3re  8993  4re  8996  5re  8998  6re  9000  7re  9002  8re  9004  9re  9006  0le2  9009  2pos  9010  3pos  9013  4pos  9016  5pos  9019  6pos  9020  7pos  9021  8pos  9022  9pos  9023  neg1rr  9025  neg1lt0  9027  1lt2  9088  1lt3  9090  1lt4  9093  1lt5  9097  1lt6  9102  1lt7  9108  1lt8  9115  1lt9  9123  1ne2  9125  1ap2  9126  1le2  9127  1le3  9130  halflt1  9136  iap0  9142  addltmul  9155  elnnnn0c  9221  nn0ge2m1nn  9236  elnnz1  9276  zltp1le  9307  zleltp1  9308  recnz  9346  gtndiv  9348  3halfnz  9350  1lt10  9522  eluzp1m1  9551  eluzp1p1  9553  eluz2b2  9603  1rp  9657  divlt1lt  9724  divle1le  9725  nnledivrp  9766  0elunit  9986  1elunit  9987  divelunit  10002  lincmb01cmp  10003  iccf1o  10004  unitssre  10005  fzpreddisj  10071  fznatpl1  10076  fztpval  10083  qbtwnxr  10258  flqbi2  10291  fldiv4p1lem1div2  10305  flqdiv  10321  reexpcl  10537  reexpclzap  10540  expge0  10556  expge1  10557  expgt1  10558  bernneq  10641  bernneq2  10642  expnbnd  10644  expnlbnd  10645  expnlbnd2  10646  nn0ltexp2  10689  facwordi  10720  faclbnd3  10723  faclbnd6  10724  facavg  10726  cjexp  10902  re1  10906  im1  10907  rei  10908  imi  10909  caucvgre  10990  sqrt1  11055  sqrt2gt1lt2  11058  abs1  11081  caubnd2  11126  mulcn2  11320  reccn2ap  11321  expcnvap0  11510  geo2sum  11522  cvgratnnlemrate  11538  fprodge0  11645  fprodge1  11647  fprodle  11648  ere  11678  ege2le3  11679  efgt1  11705  resin4p  11726  recos4p  11727  sinbnd  11760  cosbnd  11761  sinbnd2  11762  cosbnd2  11763  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  cos1bnd  11767  cos2bnd  11768  sin01gt0  11769  cos01gt0  11770  sin02gt0  11771  sincos1sgn  11772  cos12dec  11775  ene1  11792  eap1  11793  halfleoddlt  11899  flodddiv4  11939  isprm3  12118  sqnprm  12136  coprm  12144  phibndlem  12216  pythagtriplem3  12267  fldivp1  12346  pockthi  12356  exmidunben  12427  basendxnmulrndx  12592  starvndxnbasendx  12600  scandxnbasendx  12612  vscandxnbasendx  12617  ipndxnbasendx  12630  setsmsbasg  13982  tgioo  14049  dveflem  14190  reeff1olem  14195  reeff1o  14197  cosz12  14204  sinhalfpilem  14215  tangtx  14262  sincos4thpi  14264  pigt3  14268  coskpi  14272  cos0pilt1  14276  ioocosf1o  14278  loge  14291  logrpap0b  14300  logdivlti  14305  2logb9irrALT  14395  sqrt2cxp2logb9e3  14396  lgsdir  14439  lgsne0  14442  lgsabs1  14443  lgsdinn0  14452  ex-fl  14480  cvgcmp2nlemabs  14783  iooref1o  14785  trilpolemclim  14787  trilpolemcl  14788  trilpolemisumle  14789  trilpolemeq1  14791  trilpolemlt1  14792  apdiff  14799  nconstwlpolemgt0  14814