Theorem 1re 8315

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

Syntax hints:   e. wcel 2209   RRcr 8168   1c1 8170

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

This theorem is referenced by:  0re  8316  1red  8331  1xr  8374  0lt1  8443  peano2re  8452  peano2rem  8583  0reALT  8613  0le1  8799  1le1  8890  inelr  8902  1ap0  8908  eqneg  9052  ltp1  9164  ltm1  9166  recgt0  9170  mulgt1  9183  ltmulgt11  9184  lemulge11  9186  reclt1  9216  recgt1  9217  recgt1i  9218  recp1lt1  9219  recreclt  9220  sup3exmid  9277  cju  9281  peano5nni  9286  nnssre  9287  1nn  9294  nnge1  9306  nnle1eq1  9307  nngt0  9308  nnnlt1  9309  nn1gt1  9317  nngt1ne1  9318  nnrecre  9320  nnrecgt0  9321  nnsub  9322  2re  9353  3re  9357  4re  9360  5re  9362  6re  9364  7re  9366  8re  9368  9re  9370  0le2  9373  2pos  9374  3pos  9377  4pos  9380  5pos  9383  6pos  9384  7pos  9385  8pos  9386  9pos  9387  neg1rr  9389  neg1lt0  9391  1lt2  9453  1lt3  9455  1lt4  9458  1lt5  9462  1lt6  9467  1lt7  9473  1lt8  9480  1lt9  9488  1ne2  9490  1ap2  9491  1le2  9492  1le3  9495  halflt1  9501  iap0  9507  addltmul  9521  elnnnn0c  9587  nn0ge2m1nn  9606  elnnz1  9646  zltp1le  9678  zleltp1  9679  recnz  9718  gtndiv  9720  3halfnz  9722  1lt10  9894  eluzp1m1  9925  eluzp1p1  9927  eluz2b2  9982  1rp  10037  divlt1lt  10104  divle1le  10105  nnledivrp  10146  0elunit  10367  1elunit  10368  divelunit  10383  lincmb01cmp  10384  lincmble  10385  iccf1o  10386  unitssre  10387  fzpreddisj  10456  fznatpl1  10461  fztpval  10468  qbtwnxr  10670  flqbi2  10704  fldiv4p1lem1div2  10718  flqdiv  10736  seqf1oglem1  10934  reexpcl  10971  reexpclzap  10974  expge0  10990  expge1  10991  expgt1  10992  resq01  11073  bernneq  11076  bernneq2  11077  expnbnd  11079  expnlbnd  11080  expnlbnd2  11081  nn0ltexp2  11125  facwordi  11156  faclbnd3  11159  faclbnd6  11160  facavg  11162  hashtpglem  11276  lsw0  11330  cjexp  11636  re1  11641  im1  11642  rei  11643  imi  11644  caucvgre  11725  sqrt1  11790  sqrt2gt1lt2  11793  abs1  11816  caubnd2  11861  mulcn2  12056  reccn2ap  12057  expcnvap0  12247  geo2sum  12259  cvgratnnlemrate  12275  fprodge0  12382  fprodge1  12384  fprodle  12385  ere  12415  ege2le3  12416  efgt1  12442  resin4p  12463  recos4p  12464  sinbnd  12497  cosbnd  12498  sinbnd2  12499  cosbnd2  12500  ef01bndlem  12501  sin01bnd  12502  cos01bnd  12503  cos1bnd  12504  cos2bnd  12505  sinltxirr  12506  sin01gt0  12507  cos01gt0  12508  sin02gt0  12509  sincos1sgn  12510  cos12dec  12513  ene1  12530  eap1  12531  3dvds  12609  halfleoddlt  12639  flodddiv4  12681  isprm3  12874  sqnprm  12892  coprm  12900  phibndlem  12972  pythagtriplem3  13024  fldivp1  13105  pockthi  13115  ballotfilem2  13206  ballotfilem4  13219  ballotfilemi1  13223  ballotfilemic  13228  exmidunben  13295  basendxnmulrndx  13465  starvndxnbasendx  13473  scandxnbasendx  13485  vscandxnbasendx  13490  ipndxnbasendx  13503  basendxnocndx  13544  setsmsbasg  15503  tgioo  15578  dveflem  15750  reeff1olem  15795  reeff1o  15797  cosz12  15804  sinhalfpilem  15815  tangtx  15862  sincos4thpi  15864  pigt3  15868  coskpi  15872  cos0pilt1  15876  ioocosf1o  15878  loge  15891  logrpap0b  15900  logdivlti  15905  2logb9irrALT  15999  sqrt2cxp2logb9e3  16000  perfectlem2  16028  lgsdir  16068  lgsne0  16071  lgsabs1  16072  lgsdinn0  16081  gausslemma2dlem0i  16090  lgseisen  16107  2lgslem3  16134  usgrexmpldifpr  16404  konigsberglem2  16644  konigsberglem3  16645  konigsberglem5  16647  ex-fl  16653  cvgcmp2nlemabs  16986  iooref1o  16988  trilpolemclim  16990  trilpolemcl  16991  trilpolemisumle  16992  trilpolemeq1  16994  trilpolemlt1  16995  apdiff  17002  nconstwlpolemgt0  17019