Theorem 1re 8275

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

Syntax hints:   e. wcel 2205   RRcr 8128   1c1 8130

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

This theorem is referenced by:  0re  8276  1red  8291  1xr  8334  0lt1  8402  peano2re  8411  peano2rem  8542  0reALT  8572  0le1  8757  1le1  8848  inelr  8860  1ap0  8866  eqneg  9008  ltp1  9120  ltm1  9122  recgt0  9126  mulgt1  9139  ltmulgt11  9140  lemulge11  9142  reclt1  9172  recgt1  9173  recgt1i  9174  recp1lt1  9175  recreclt  9176  sup3exmid  9233  cju  9237  peano5nni  9242  nnssre  9243  1nn  9250  nnge1  9262  nnle1eq1  9263  nngt0  9264  nnnlt1  9265  nn1gt1  9273  nngt1ne1  9274  nnrecre  9276  nnrecgt0  9277  nnsub  9278  2re  9309  3re  9313  4re  9316  5re  9318  6re  9320  7re  9322  8re  9324  9re  9326  0le2  9329  2pos  9330  3pos  9333  4pos  9336  5pos  9339  6pos  9340  7pos  9341  8pos  9342  9pos  9343  neg1rr  9345  neg1lt0  9347  1lt2  9409  1lt3  9411  1lt4  9414  1lt5  9418  1lt6  9423  1lt7  9429  1lt8  9436  1lt9  9444  1ne2  9446  1ap2  9447  1le2  9448  1le3  9451  halflt1  9457  iap0  9463  addltmul  9477  elnnnn0c  9543  nn0ge2m1nn  9562  elnnz1  9602  zltp1le  9634  zleltp1  9635  recnz  9674  gtndiv  9676  3halfnz  9678  1lt10  9850  eluzp1m1  9881  eluzp1p1  9883  eluz2b2  9938  1rp  9993  divlt1lt  10060  divle1le  10061  nnledivrp  10102  0elunit  10322  1elunit  10323  divelunit  10338  lincmb01cmp  10339  lincmble  10340  iccf1o  10341  unitssre  10342  fzpreddisj  10409  fznatpl1  10414  fztpval  10421  qbtwnxr  10621  flqbi2  10655  fldiv4p1lem1div2  10669  flqdiv  10687  seqf1oglem1  10885  reexpcl  10922  reexpclzap  10925  expge0  10941  expge1  10942  expgt1  10943  bernneq  11026  bernneq2  11027  expnbnd  11029  expnlbnd  11030  expnlbnd2  11031  nn0ltexp2  11075  facwordi  11106  faclbnd3  11109  faclbnd6  11110  facavg  11112  hashtpglem  11222  lsw0  11276  cjexp  11582  re1  11586  im1  11587  rei  11588  imi  11589  caucvgre  11670  sqrt1  11735  sqrt2gt1lt2  11738  abs1  11761  caubnd2  11806  mulcn2  12001  reccn2ap  12002  expcnvap0  12192  geo2sum  12204  cvgratnnlemrate  12220  fprodge0  12327  fprodge1  12329  fprodle  12330  ere  12360  ege2le3  12361  efgt1  12387  resin4p  12408  recos4p  12409  sinbnd  12442  cosbnd  12443  sinbnd2  12444  cosbnd2  12445  ef01bndlem  12446  sin01bnd  12447  cos01bnd  12448  cos1bnd  12449  cos2bnd  12450  sinltxirr  12451  sin01gt0  12452  cos01gt0  12453  sin02gt0  12454  sincos1sgn  12455  cos12dec  12458  ene1  12475  eap1  12476  3dvds  12554  halfleoddlt  12584  flodddiv4  12626  isprm3  12819  sqnprm  12837  coprm  12845  phibndlem  12917  pythagtriplem3  12969  fldivp1  13050  pockthi  13060  ballotfilem2  13149  ballotfilem4  13159  exmidunben  13194  basendxnmulrndx  13364  starvndxnbasendx  13372  scandxnbasendx  13384  vscandxnbasendx  13389  ipndxnbasendx  13402  basendxnocndx  13443  setsmsbasg  15361  tgioo  15436  dveflem  15608  reeff1olem  15653  reeff1o  15655  cosz12  15662  sinhalfpilem  15673  tangtx  15720  sincos4thpi  15722  pigt3  15726  coskpi  15730  cos0pilt1  15734  ioocosf1o  15736  loge  15749  logrpap0b  15758  logdivlti  15763  2logb9irrALT  15856  sqrt2cxp2logb9e3  15857  perfectlem2  15885  lgsdir  15925  lgsne0  15928  lgsabs1  15929  lgsdinn0  15938  gausslemma2dlem0i  15947  lgseisen  15964  2lgslem3  15991  usgrexmpldifpr  16261  konigsberglem2  16501  konigsberglem3  16502  konigsberglem5  16504  ex-fl  16510  cvgcmp2nlemabs  16833  iooref1o  16835  trilpolemclim  16837  trilpolemcl  16838  trilpolemisumle  16839  trilpolemeq1  16841  trilpolemlt1  16842  apdiff  16849  nconstwlpolemgt0  16867