Theorem 1re 7908

Description: 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)

Assertion

Ref	Expression
1re	⊢ 1 ∈ ℝ

Proof of Theorem 1re

Step	Hyp	Ref	Expression
1		ax-1re 7857	1 ⊢ 1 ∈ ℝ

Syntax hints:   ∈ wcel 2141  ℝcr 7762  1c1 7764

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

This theorem is referenced by:  0re  7909  1red  7924  1xr  7967  0lt1  8035  peano2re  8044  peano2rem  8175  0reALT  8205  0le1  8389  1le1  8480  inelr  8492  1ap0  8498  eqneg  8638  ltp1  8749  ltm1  8751  recgt0  8755  mulgt1  8768  ltmulgt11  8769  lemulge11  8771  reclt1  8801  recgt1  8802  recgt1i  8803  recp1lt1  8804  recreclt  8805  sup3exmid  8862  cju  8866  peano5nni  8870  nnssre  8871  1nn  8878  nnge1  8890  nnle1eq1  8891  nngt0  8892  nnnlt1  8893  nn1gt1  8901  nngt1ne1  8902  nnrecre  8904  nnrecgt0  8905  nnsub  8906  2re  8937  3re  8941  4re  8944  5re  8946  6re  8948  7re  8950  8re  8952  9re  8954  0le2  8957  2pos  8958  3pos  8961  4pos  8964  5pos  8967  6pos  8968  7pos  8969  8pos  8970  9pos  8971  neg1rr  8973  neg1lt0  8975  1lt2  9036  1lt3  9038  1lt4  9041  1lt5  9045  1lt6  9050  1lt7  9056  1lt8  9063  1lt9  9071  1ne2  9073  1ap2  9074  1le2  9075  1le3  9078  halflt1  9084  iap0  9090  addltmul  9103  elnnnn0c  9169  nn0ge2m1nn  9184  elnnz1  9224  zltp1le  9255  zleltp1  9256  recnz  9294  gtndiv  9296  3halfnz  9298  1lt10  9470  eluzp1m1  9499  eluzp1p1  9501  eluz2b2  9551  1rp  9603  divlt1lt  9670  divle1le  9671  nnledivrp  9712  0elunit  9932  1elunit  9933  divelunit  9948  lincmb01cmp  9949  iccf1o  9950  unitssre  9951  fzpreddisj  10016  fznatpl1  10021  fztpval  10028  qbtwnxr  10203  flqbi2  10236  fldiv4p1lem1div2  10250  flqdiv  10266  reexpcl  10482  reexpclzap  10485  expge0  10501  expge1  10502  expgt1  10503  bernneq  10585  bernneq2  10586  expnbnd  10588  expnlbnd  10589  expnlbnd2  10590  nn0ltexp2  10633  facwordi  10663  faclbnd3  10666  faclbnd6  10667  facavg  10669  cjexp  10846  re1  10850  im1  10851  rei  10852  imi  10853  caucvgre  10934  sqrt1  10999  sqrt2gt1lt2  11002  abs1  11025  caubnd2  11070  mulcn2  11264  reccn2ap  11265  expcnvap0  11454  geo2sum  11466  cvgratnnlemrate  11482  fprodge0  11589  fprodge1  11591  fprodle  11592  ere  11622  ege2le3  11623  efgt1  11649  resin4p  11670  recos4p  11671  sinbnd  11704  cosbnd  11705  sinbnd2  11706  cosbnd2  11707  ef01bndlem  11708  sin01bnd  11709  cos01bnd  11710  cos1bnd  11711  cos2bnd  11712  sin01gt0  11713  cos01gt0  11714  sin02gt0  11715  sincos1sgn  11716  cos12dec  11719  ene1  11736  eap1  11737  halfleoddlt  11842  flodddiv4  11882  isprm3  12061  sqnprm  12079  coprm  12087  phibndlem  12159  pythagtriplem3  12210  fldivp1  12289  pockthi  12299  exmidunben  12370  basendxnmulrndx  12521  setsmsbasg  13234  tgioo  13301  dveflem  13442  reeff1olem  13447  reeff1o  13449  cosz12  13456  sinhalfpilem  13467  tangtx  13514  sincos4thpi  13516  pigt3  13520  coskpi  13524  cos0pilt1  13528  ioocosf1o  13530  loge  13543  logrpap0b  13552  logdivlti  13557  2logb9irrALT  13647  sqrt2cxp2logb9e3  13648  lgsdir  13691  lgsne0  13694  lgsabs1  13695  lgsdinn0  13704  ex-fl  13721  cvgcmp2nlemabs  14026  iooref1o  14028  trilpolemclim  14030  trilpolemcl  14031  trilpolemisumle  14032  trilpolemeq1  14034  trilpolemlt1  14035  apdiff  14042  nconstwlpolemgt0  14057