Theorem 1re 8020

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

Syntax hints:   ∈ wcel 2164  ℝcr 7873  1c1 7875

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

This theorem is referenced by:  0re  8021  1red  8036  1xr  8080  0lt1  8148  peano2re  8157  peano2rem  8288  0reALT  8318  0le1  8502  1le1  8593  inelr  8605  1ap0  8611  eqneg  8753  ltp1  8865  ltm1  8867  recgt0  8871  mulgt1  8884  ltmulgt11  8885  lemulge11  8887  reclt1  8917  recgt1  8918  recgt1i  8919  recp1lt1  8920  recreclt  8921  sup3exmid  8978  cju  8982  peano5nni  8987  nnssre  8988  1nn  8995  nnge1  9007  nnle1eq1  9008  nngt0  9009  nnnlt1  9010  nn1gt1  9018  nngt1ne1  9019  nnrecre  9021  nnrecgt0  9022  nnsub  9023  2re  9054  3re  9058  4re  9061  5re  9063  6re  9065  7re  9067  8re  9069  9re  9071  0le2  9074  2pos  9075  3pos  9078  4pos  9081  5pos  9084  6pos  9085  7pos  9086  8pos  9087  9pos  9088  neg1rr  9090  neg1lt0  9092  1lt2  9154  1lt3  9156  1lt4  9159  1lt5  9163  1lt6  9168  1lt7  9174  1lt8  9181  1lt9  9189  1ne2  9191  1ap2  9192  1le2  9193  1le3  9196  halflt1  9202  iap0  9208  addltmul  9222  elnnnn0c  9288  nn0ge2m1nn  9303  elnnz1  9343  zltp1le  9374  zleltp1  9375  recnz  9413  gtndiv  9415  3halfnz  9417  1lt10  9589  eluzp1m1  9619  eluzp1p1  9621  eluz2b2  9671  1rp  9726  divlt1lt  9793  divle1le  9794  nnledivrp  9835  0elunit  10055  1elunit  10056  divelunit  10071  lincmb01cmp  10072  iccf1o  10073  unitssre  10074  fzpreddisj  10140  fznatpl1  10145  fztpval  10152  qbtwnxr  10329  flqbi2  10363  fldiv4p1lem1div2  10377  flqdiv  10395  seqf1oglem1  10593  reexpcl  10630  reexpclzap  10633  expge0  10649  expge1  10650  expgt1  10651  bernneq  10734  bernneq2  10735  expnbnd  10737  expnlbnd  10738  expnlbnd2  10739  nn0ltexp2  10783  facwordi  10814  faclbnd3  10817  faclbnd6  10818  facavg  10820  cjexp  11040  re1  11044  im1  11045  rei  11046  imi  11047  caucvgre  11128  sqrt1  11193  sqrt2gt1lt2  11196  abs1  11219  caubnd2  11264  mulcn2  11458  reccn2ap  11459  expcnvap0  11648  geo2sum  11660  cvgratnnlemrate  11676  fprodge0  11783  fprodge1  11785  fprodle  11786  ere  11816  ege2le3  11817  efgt1  11843  resin4p  11864  recos4p  11865  sinbnd  11898  cosbnd  11899  sinbnd2  11900  cosbnd2  11901  ef01bndlem  11902  sin01bnd  11903  cos01bnd  11904  cos1bnd  11905  cos2bnd  11906  sinltxirr  11907  sin01gt0  11908  cos01gt0  11909  sin02gt0  11910  sincos1sgn  11911  cos12dec  11914  ene1  11931  eap1  11932  halfleoddlt  12038  flodddiv4  12078  isprm3  12259  sqnprm  12277  coprm  12285  phibndlem  12357  pythagtriplem3  12408  fldivp1  12489  pockthi  12499  exmidunben  12586  basendxnmulrndx  12754  starvndxnbasendx  12762  scandxnbasendx  12774  vscandxnbasendx  12779  ipndxnbasendx  12792  setsmsbasg  14658  tgioo  14733  dveflem  14905  reeff1olem  14947  reeff1o  14949  cosz12  14956  sinhalfpilem  14967  tangtx  15014  sincos4thpi  15016  pigt3  15020  coskpi  15024  cos0pilt1  15028  ioocosf1o  15030  loge  15043  logrpap0b  15052  logdivlti  15057  2logb9irrALT  15147  sqrt2cxp2logb9e3  15148  lgsdir  15192  lgsne0  15195  lgsabs1  15196  lgsdinn0  15205  gausslemma2dlem0i  15214  lgseisen  15231  2lgslem3  15258  ex-fl  15287  cvgcmp2nlemabs  15592  iooref1o  15594  trilpolemclim  15596  trilpolemcl  15597  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  apdiff  15608  nconstwlpolemgt0  15624