Theorem 1re 8178

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

Syntax hints:   e. wcel 2202   RRcr 8031   1c1 8033

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

This theorem is referenced by:  0re  8179  1red  8194  1xr  8238  0lt1  8306  peano2re  8315  peano2rem  8446  0reALT  8476  0le1  8661  1le1  8752  inelr  8764  1ap0  8770  eqneg  8912  ltp1  9024  ltm1  9026  recgt0  9030  mulgt1  9043  ltmulgt11  9044  lemulge11  9046  reclt1  9076  recgt1  9077  recgt1i  9078  recp1lt1  9079  recreclt  9080  sup3exmid  9137  cju  9141  peano5nni  9146  nnssre  9147  1nn  9154  nnge1  9166  nnle1eq1  9167  nngt0  9168  nnnlt1  9169  nn1gt1  9177  nngt1ne1  9178  nnrecre  9180  nnrecgt0  9181  nnsub  9182  2re  9213  3re  9217  4re  9220  5re  9222  6re  9224  7re  9226  8re  9228  9re  9230  0le2  9233  2pos  9234  3pos  9237  4pos  9240  5pos  9243  6pos  9244  7pos  9245  8pos  9246  9pos  9247  neg1rr  9249  neg1lt0  9251  1lt2  9313  1lt3  9315  1lt4  9318  1lt5  9322  1lt6  9327  1lt7  9333  1lt8  9340  1lt9  9348  1ne2  9350  1ap2  9351  1le2  9352  1le3  9355  halflt1  9361  iap0  9367  addltmul  9381  elnnnn0c  9447  nn0ge2m1nn  9462  elnnz1  9502  zltp1le  9534  zleltp1  9535  recnz  9573  gtndiv  9575  3halfnz  9577  1lt10  9749  eluzp1m1  9780  eluzp1p1  9782  eluz2b2  9837  1rp  9892  divlt1lt  9959  divle1le  9960  nnledivrp  10001  0elunit  10221  1elunit  10222  divelunit  10237  lincmb01cmp  10238  iccf1o  10239  unitssre  10240  fzpreddisj  10306  fznatpl1  10311  fztpval  10318  qbtwnxr  10518  flqbi2  10552  fldiv4p1lem1div2  10566  flqdiv  10584  seqf1oglem1  10782  reexpcl  10819  reexpclzap  10822  expge0  10838  expge1  10839  expgt1  10840  bernneq  10923  bernneq2  10924  expnbnd  10926  expnlbnd  10927  expnlbnd2  10928  nn0ltexp2  10972  facwordi  11003  faclbnd3  11006  faclbnd6  11007  facavg  11009  hashtpglem  11111  lsw0  11165  cjexp  11471  re1  11475  im1  11476  rei  11477  imi  11478  caucvgre  11559  sqrt1  11624  sqrt2gt1lt2  11627  abs1  11650  caubnd2  11695  mulcn2  11890  reccn2ap  11891  expcnvap0  12081  geo2sum  12093  cvgratnnlemrate  12109  fprodge0  12216  fprodge1  12218  fprodle  12219  ere  12249  ege2le3  12250  efgt1  12276  resin4p  12297  recos4p  12298  sinbnd  12331  cosbnd  12332  sinbnd2  12333  cosbnd2  12334  ef01bndlem  12335  sin01bnd  12336  cos01bnd  12337  cos1bnd  12338  cos2bnd  12339  sinltxirr  12340  sin01gt0  12341  cos01gt0  12342  sin02gt0  12343  sincos1sgn  12344  cos12dec  12347  ene1  12364  eap1  12365  3dvds  12443  halfleoddlt  12473  flodddiv4  12515  isprm3  12708  sqnprm  12726  coprm  12734  phibndlem  12806  pythagtriplem3  12858  fldivp1  12939  pockthi  12949  exmidunben  13065  basendxnmulrndx  13235  starvndxnbasendx  13243  scandxnbasendx  13255  vscandxnbasendx  13260  ipndxnbasendx  13273  basendxnocndx  13314  setsmsbasg  15222  tgioo  15297  dveflem  15469  reeff1olem  15514  reeff1o  15516  cosz12  15523  sinhalfpilem  15534  tangtx  15581  sincos4thpi  15583  pigt3  15587  coskpi  15591  cos0pilt1  15595  ioocosf1o  15597  loge  15610  logrpap0b  15619  logdivlti  15624  2logb9irrALT  15717  sqrt2cxp2logb9e3  15718  perfectlem2  15743  lgsdir  15783  lgsne0  15786  lgsabs1  15787  lgsdinn0  15796  gausslemma2dlem0i  15805  lgseisen  15822  2lgslem3  15849  usgrexmpldifpr  16119  konigsberglem2  16359  konigsberglem3  16360  konigsberglem5  16362  ex-fl  16368  cvgcmp2nlemabs  16687  iooref1o  16689  trilpolemclim  16691  trilpolemcl  16692  trilpolemisumle  16693  trilpolemeq1  16695  trilpolemlt1  16696  apdiff  16703  nconstwlpolemgt0  16720