Theorem 1re 8145

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

Syntax hints:   e. wcel 2200   RRcr 7998   1c1 8000

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

This theorem is referenced by:  0re  8146  1red  8161  1xr  8205  0lt1  8273  peano2re  8282  peano2rem  8413  0reALT  8443  0le1  8628  1le1  8719  inelr  8731  1ap0  8737  eqneg  8879  ltp1  8991  ltm1  8993  recgt0  8997  mulgt1  9010  ltmulgt11  9011  lemulge11  9013  reclt1  9043  recgt1  9044  recgt1i  9045  recp1lt1  9046  recreclt  9047  sup3exmid  9104  cju  9108  peano5nni  9113  nnssre  9114  1nn  9121  nnge1  9133  nnle1eq1  9134  nngt0  9135  nnnlt1  9136  nn1gt1  9144  nngt1ne1  9145  nnrecre  9147  nnrecgt0  9148  nnsub  9149  2re  9180  3re  9184  4re  9187  5re  9189  6re  9191  7re  9193  8re  9195  9re  9197  0le2  9200  2pos  9201  3pos  9204  4pos  9207  5pos  9210  6pos  9211  7pos  9212  8pos  9213  9pos  9214  neg1rr  9216  neg1lt0  9218  1lt2  9280  1lt3  9282  1lt4  9285  1lt5  9289  1lt6  9294  1lt7  9300  1lt8  9307  1lt9  9315  1ne2  9317  1ap2  9318  1le2  9319  1le3  9322  halflt1  9328  iap0  9334  addltmul  9348  elnnnn0c  9414  nn0ge2m1nn  9429  elnnz1  9469  zltp1le  9501  zleltp1  9502  recnz  9540  gtndiv  9542  3halfnz  9544  1lt10  9716  eluzp1m1  9746  eluzp1p1  9748  eluz2b2  9798  1rp  9853  divlt1lt  9920  divle1le  9921  nnledivrp  9962  0elunit  10182  1elunit  10183  divelunit  10198  lincmb01cmp  10199  iccf1o  10200  unitssre  10201  fzpreddisj  10267  fznatpl1  10272  fztpval  10279  qbtwnxr  10477  flqbi2  10511  fldiv4p1lem1div2  10525  flqdiv  10543  seqf1oglem1  10741  reexpcl  10778  reexpclzap  10781  expge0  10797  expge1  10798  expgt1  10799  bernneq  10882  bernneq2  10883  expnbnd  10885  expnlbnd  10886  expnlbnd2  10887  nn0ltexp2  10931  facwordi  10962  faclbnd3  10965  faclbnd6  10966  facavg  10968  lsw0  11119  cjexp  11404  re1  11408  im1  11409  rei  11410  imi  11411  caucvgre  11492  sqrt1  11557  sqrt2gt1lt2  11560  abs1  11583  caubnd2  11628  mulcn2  11823  reccn2ap  11824  expcnvap0  12013  geo2sum  12025  cvgratnnlemrate  12041  fprodge0  12148  fprodge1  12150  fprodle  12151  ere  12181  ege2le3  12182  efgt1  12208  resin4p  12229  recos4p  12230  sinbnd  12263  cosbnd  12264  sinbnd2  12265  cosbnd2  12266  ef01bndlem  12267  sin01bnd  12268  cos01bnd  12269  cos1bnd  12270  cos2bnd  12271  sinltxirr  12272  sin01gt0  12273  cos01gt0  12274  sin02gt0  12275  sincos1sgn  12276  cos12dec  12279  ene1  12296  eap1  12297  3dvds  12375  halfleoddlt  12405  flodddiv4  12447  isprm3  12640  sqnprm  12658  coprm  12666  phibndlem  12738  pythagtriplem3  12790  fldivp1  12871  pockthi  12881  exmidunben  12997  basendxnmulrndx  13167  starvndxnbasendx  13175  scandxnbasendx  13187  vscandxnbasendx  13192  ipndxnbasendx  13205  basendxnocndx  13246  setsmsbasg  15153  tgioo  15228  dveflem  15400  reeff1olem  15445  reeff1o  15447  cosz12  15454  sinhalfpilem  15465  tangtx  15512  sincos4thpi  15514  pigt3  15518  coskpi  15522  cos0pilt1  15526  ioocosf1o  15528  loge  15541  logrpap0b  15550  logdivlti  15555  2logb9irrALT  15648  sqrt2cxp2logb9e3  15649  perfectlem2  15674  lgsdir  15714  lgsne0  15717  lgsabs1  15718  lgsdinn0  15727  gausslemma2dlem0i  15736  lgseisen  15753  2lgslem3  15780  ex-fl  16089  cvgcmp2nlemabs  16400  iooref1o  16402  trilpolemclim  16404  trilpolemcl  16405  trilpolemisumle  16406  trilpolemeq1  16408  trilpolemlt1  16409  apdiff  16416  nconstwlpolemgt0  16432