Theorem 1re 8106

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

Syntax hints:   e. wcel 2178   RRcr 7959   1c1 7961

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

This theorem is referenced by:  0re  8107  1red  8122  1xr  8166  0lt1  8234  peano2re  8243  peano2rem  8374  0reALT  8404  0le1  8589  1le1  8680  inelr  8692  1ap0  8698  eqneg  8840  ltp1  8952  ltm1  8954  recgt0  8958  mulgt1  8971  ltmulgt11  8972  lemulge11  8974  reclt1  9004  recgt1  9005  recgt1i  9006  recp1lt1  9007  recreclt  9008  sup3exmid  9065  cju  9069  peano5nni  9074  nnssre  9075  1nn  9082  nnge1  9094  nnle1eq1  9095  nngt0  9096  nnnlt1  9097  nn1gt1  9105  nngt1ne1  9106  nnrecre  9108  nnrecgt0  9109  nnsub  9110  2re  9141  3re  9145  4re  9148  5re  9150  6re  9152  7re  9154  8re  9156  9re  9158  0le2  9161  2pos  9162  3pos  9165  4pos  9168  5pos  9171  6pos  9172  7pos  9173  8pos  9174  9pos  9175  neg1rr  9177  neg1lt0  9179  1lt2  9241  1lt3  9243  1lt4  9246  1lt5  9250  1lt6  9255  1lt7  9261  1lt8  9268  1lt9  9276  1ne2  9278  1ap2  9279  1le2  9280  1le3  9283  halflt1  9289  iap0  9295  addltmul  9309  elnnnn0c  9375  nn0ge2m1nn  9390  elnnz1  9430  zltp1le  9462  zleltp1  9463  recnz  9501  gtndiv  9503  3halfnz  9505  1lt10  9677  eluzp1m1  9707  eluzp1p1  9709  eluz2b2  9759  1rp  9814  divlt1lt  9881  divle1le  9882  nnledivrp  9923  0elunit  10143  1elunit  10144  divelunit  10159  lincmb01cmp  10160  iccf1o  10161  unitssre  10162  fzpreddisj  10228  fznatpl1  10233  fztpval  10240  qbtwnxr  10437  flqbi2  10471  fldiv4p1lem1div2  10485  flqdiv  10503  seqf1oglem1  10701  reexpcl  10738  reexpclzap  10741  expge0  10757  expge1  10758  expgt1  10759  bernneq  10842  bernneq2  10843  expnbnd  10845  expnlbnd  10846  expnlbnd2  10847  nn0ltexp2  10891  facwordi  10922  faclbnd3  10925  faclbnd6  10926  facavg  10928  lsw0  11078  cjexp  11319  re1  11323  im1  11324  rei  11325  imi  11326  caucvgre  11407  sqrt1  11472  sqrt2gt1lt2  11475  abs1  11498  caubnd2  11543  mulcn2  11738  reccn2ap  11739  expcnvap0  11928  geo2sum  11940  cvgratnnlemrate  11956  fprodge0  12063  fprodge1  12065  fprodle  12066  ere  12096  ege2le3  12097  efgt1  12123  resin4p  12144  recos4p  12145  sinbnd  12178  cosbnd  12179  sinbnd2  12180  cosbnd2  12181  ef01bndlem  12182  sin01bnd  12183  cos01bnd  12184  cos1bnd  12185  cos2bnd  12186  sinltxirr  12187  sin01gt0  12188  cos01gt0  12189  sin02gt0  12190  sincos1sgn  12191  cos12dec  12194  ene1  12211  eap1  12212  3dvds  12290  halfleoddlt  12320  flodddiv4  12362  isprm3  12555  sqnprm  12573  coprm  12581  phibndlem  12653  pythagtriplem3  12705  fldivp1  12786  pockthi  12796  exmidunben  12912  basendxnmulrndx  13081  starvndxnbasendx  13089  scandxnbasendx  13101  vscandxnbasendx  13106  ipndxnbasendx  13119  basendxnocndx  13160  setsmsbasg  15066  tgioo  15141  dveflem  15313  reeff1olem  15358  reeff1o  15360  cosz12  15367  sinhalfpilem  15378  tangtx  15425  sincos4thpi  15427  pigt3  15431  coskpi  15435  cos0pilt1  15439  ioocosf1o  15441  loge  15454  logrpap0b  15463  logdivlti  15468  2logb9irrALT  15561  sqrt2cxp2logb9e3  15562  perfectlem2  15587  lgsdir  15627  lgsne0  15630  lgsabs1  15631  lgsdinn0  15640  gausslemma2dlem0i  15649  lgseisen  15666  2lgslem3  15693  ex-fl  15861  cvgcmp2nlemabs  16173  iooref1o  16175  trilpolemclim  16177  trilpolemcl  16178  trilpolemisumle  16179  trilpolemeq1  16181  trilpolemlt1  16182  apdiff  16189  nconstwlpolemgt0  16205