Theorem 1re 7985

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 7934	1 ⊢ 1 ∈ ℝ

Syntax hints:   ∈ wcel 2160  ℝcr 7839  1c1 7841

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

This theorem is referenced by:  0re  7986  1red  8001  1xr  8045  0lt1  8113  peano2re  8122  peano2rem  8253  0reALT  8283  0le1  8467  1le1  8558  inelr  8570  1ap0  8576  eqneg  8718  ltp1  8830  ltm1  8832  recgt0  8836  mulgt1  8849  ltmulgt11  8850  lemulge11  8852  reclt1  8882  recgt1  8883  recgt1i  8884  recp1lt1  8885  recreclt  8886  sup3exmid  8943  cju  8947  peano5nni  8951  nnssre  8952  1nn  8959  nnge1  8971  nnle1eq1  8972  nngt0  8973  nnnlt1  8974  nn1gt1  8982  nngt1ne1  8983  nnrecre  8985  nnrecgt0  8986  nnsub  8987  2re  9018  3re  9022  4re  9025  5re  9027  6re  9029  7re  9031  8re  9033  9re  9035  0le2  9038  2pos  9039  3pos  9042  4pos  9045  5pos  9048  6pos  9049  7pos  9050  8pos  9051  9pos  9052  neg1rr  9054  neg1lt0  9056  1lt2  9117  1lt3  9119  1lt4  9122  1lt5  9126  1lt6  9131  1lt7  9137  1lt8  9144  1lt9  9152  1ne2  9154  1ap2  9155  1le2  9156  1le3  9159  halflt1  9165  iap0  9171  addltmul  9184  elnnnn0c  9250  nn0ge2m1nn  9265  elnnz1  9305  zltp1le  9336  zleltp1  9337  recnz  9375  gtndiv  9377  3halfnz  9379  1lt10  9551  eluzp1m1  9580  eluzp1p1  9582  eluz2b2  9632  1rp  9686  divlt1lt  9753  divle1le  9754  nnledivrp  9795  0elunit  10015  1elunit  10016  divelunit  10031  lincmb01cmp  10032  iccf1o  10033  unitssre  10034  fzpreddisj  10100  fznatpl1  10105  fztpval  10112  qbtwnxr  10287  flqbi2  10321  fldiv4p1lem1div2  10335  flqdiv  10351  reexpcl  10567  reexpclzap  10570  expge0  10586  expge1  10587  expgt1  10588  bernneq  10671  bernneq2  10672  expnbnd  10674  expnlbnd  10675  expnlbnd2  10676  nn0ltexp2  10720  facwordi  10751  faclbnd3  10754  faclbnd6  10755  facavg  10757  cjexp  10933  re1  10937  im1  10938  rei  10939  imi  10940  caucvgre  11021  sqrt1  11086  sqrt2gt1lt2  11089  abs1  11112  caubnd2  11157  mulcn2  11351  reccn2ap  11352  expcnvap0  11541  geo2sum  11553  cvgratnnlemrate  11569  fprodge0  11676  fprodge1  11678  fprodle  11679  ere  11709  ege2le3  11710  efgt1  11736  resin4p  11757  recos4p  11758  sinbnd  11791  cosbnd  11792  sinbnd2  11793  cosbnd2  11794  ef01bndlem  11795  sin01bnd  11796  cos01bnd  11797  cos1bnd  11798  cos2bnd  11799  sin01gt0  11800  cos01gt0  11801  sin02gt0  11802  sincos1sgn  11803  cos12dec  11806  ene1  11823  eap1  11824  halfleoddlt  11930  flodddiv4  11970  isprm3  12149  sqnprm  12167  coprm  12175  phibndlem  12247  pythagtriplem3  12298  fldivp1  12379  pockthi  12389  exmidunben  12476  basendxnmulrndx  12642  starvndxnbasendx  12650  scandxnbasendx  12662  vscandxnbasendx  12667  ipndxnbasendx  12680  setsmsbasg  14431  tgioo  14498  dveflem  14639  reeff1olem  14644  reeff1o  14646  cosz12  14653  sinhalfpilem  14664  tangtx  14711  sincos4thpi  14713  pigt3  14717  coskpi  14721  cos0pilt1  14725  ioocosf1o  14727  loge  14740  logrpap0b  14749  logdivlti  14754  2logb9irrALT  14844  sqrt2cxp2logb9e3  14845  lgsdir  14889  lgsne0  14892  lgsabs1  14893  lgsdinn0  14902  ex-fl  14930  cvgcmp2nlemabs  15234  iooref1o  15236  trilpolemclim  15238  trilpolemcl  15239  trilpolemisumle  15240  trilpolemeq1  15242  trilpolemlt1  15243  apdiff  15250  nconstwlpolemgt0  15266