Theorem 1re 8073

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

Syntax hints:   e. wcel 2176   RRcr 7926   1c1 7928

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

This theorem is referenced by:  0re  8074  1red  8089  1xr  8133  0lt1  8201  peano2re  8210  peano2rem  8341  0reALT  8371  0le1  8556  1le1  8647  inelr  8659  1ap0  8665  eqneg  8807  ltp1  8919  ltm1  8921  recgt0  8925  mulgt1  8938  ltmulgt11  8939  lemulge11  8941  reclt1  8971  recgt1  8972  recgt1i  8973  recp1lt1  8974  recreclt  8975  sup3exmid  9032  cju  9036  peano5nni  9041  nnssre  9042  1nn  9049  nnge1  9061  nnle1eq1  9062  nngt0  9063  nnnlt1  9064  nn1gt1  9072  nngt1ne1  9073  nnrecre  9075  nnrecgt0  9076  nnsub  9077  2re  9108  3re  9112  4re  9115  5re  9117  6re  9119  7re  9121  8re  9123  9re  9125  0le2  9128  2pos  9129  3pos  9132  4pos  9135  5pos  9138  6pos  9139  7pos  9140  8pos  9141  9pos  9142  neg1rr  9144  neg1lt0  9146  1lt2  9208  1lt3  9210  1lt4  9213  1lt5  9217  1lt6  9222  1lt7  9228  1lt8  9235  1lt9  9243  1ne2  9245  1ap2  9246  1le2  9247  1le3  9250  halflt1  9256  iap0  9262  addltmul  9276  elnnnn0c  9342  nn0ge2m1nn  9357  elnnz1  9397  zltp1le  9429  zleltp1  9430  recnz  9468  gtndiv  9470  3halfnz  9472  1lt10  9644  eluzp1m1  9674  eluzp1p1  9676  eluz2b2  9726  1rp  9781  divlt1lt  9848  divle1le  9849  nnledivrp  9890  0elunit  10110  1elunit  10111  divelunit  10126  lincmb01cmp  10127  iccf1o  10128  unitssre  10129  fzpreddisj  10195  fznatpl1  10200  fztpval  10207  qbtwnxr  10402  flqbi2  10436  fldiv4p1lem1div2  10450  flqdiv  10468  seqf1oglem1  10666  reexpcl  10703  reexpclzap  10706  expge0  10722  expge1  10723  expgt1  10724  bernneq  10807  bernneq2  10808  expnbnd  10810  expnlbnd  10811  expnlbnd2  10812  nn0ltexp2  10856  facwordi  10887  faclbnd3  10890  faclbnd6  10891  facavg  10893  lsw0  11043  cjexp  11237  re1  11241  im1  11242  rei  11243  imi  11244  caucvgre  11325  sqrt1  11390  sqrt2gt1lt2  11393  abs1  11416  caubnd2  11461  mulcn2  11656  reccn2ap  11657  expcnvap0  11846  geo2sum  11858  cvgratnnlemrate  11874  fprodge0  11981  fprodge1  11983  fprodle  11984  ere  12014  ege2le3  12015  efgt1  12041  resin4p  12062  recos4p  12063  sinbnd  12096  cosbnd  12097  sinbnd2  12098  cosbnd2  12099  ef01bndlem  12100  sin01bnd  12101  cos01bnd  12102  cos1bnd  12103  cos2bnd  12104  sinltxirr  12105  sin01gt0  12106  cos01gt0  12107  sin02gt0  12108  sincos1sgn  12109  cos12dec  12112  ene1  12129  eap1  12130  3dvds  12208  halfleoddlt  12238  flodddiv4  12280  isprm3  12473  sqnprm  12491  coprm  12499  phibndlem  12571  pythagtriplem3  12623  fldivp1  12704  pockthi  12714  exmidunben  12830  basendxnmulrndx  12999  starvndxnbasendx  13007  scandxnbasendx  13019  vscandxnbasendx  13024  ipndxnbasendx  13037  basendxnocndx  13078  setsmsbasg  14984  tgioo  15059  dveflem  15231  reeff1olem  15276  reeff1o  15278  cosz12  15285  sinhalfpilem  15296  tangtx  15343  sincos4thpi  15345  pigt3  15349  coskpi  15353  cos0pilt1  15357  ioocosf1o  15359  loge  15372  logrpap0b  15381  logdivlti  15386  2logb9irrALT  15479  sqrt2cxp2logb9e3  15480  perfectlem2  15505  lgsdir  15545  lgsne0  15548  lgsabs1  15549  lgsdinn0  15558  gausslemma2dlem0i  15567  lgseisen  15584  2lgslem3  15611  ex-fl  15698  cvgcmp2nlemabs  16008  iooref1o  16010  trilpolemclim  16012  trilpolemcl  16013  trilpolemisumle  16014  trilpolemeq1  16016  trilpolemlt1  16017  apdiff  16024  nconstwlpolemgt0  16040