Theorem 1re 7765

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

Syntax hints:   ∈ wcel 1480  ℝcr 7619  1c1 7621

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

This theorem is referenced by:  0re  7766  1red  7781  0lt1  7889  peano2re  7898  peano2rem  8029  0reALT  8059  0le1  8243  1le1  8334  inelr  8346  1ap0  8352  eqneg  8492  ltp1  8602  ltm1  8604  recgt0  8608  mulgt1  8621  ltmulgt11  8622  lemulge11  8624  reclt1  8654  recgt1  8655  recgt1i  8656  recp1lt1  8657  recreclt  8658  sup3exmid  8715  cju  8719  peano5nni  8723  nnssre  8724  1nn  8731  nnge1  8743  nnle1eq1  8744  nngt0  8745  nnnlt1  8746  nn1gt1  8754  nngt1ne1  8755  nnrecre  8757  nnrecgt0  8758  nnsub  8759  2re  8790  3re  8794  4re  8797  5re  8799  6re  8801  7re  8803  8re  8805  9re  8807  0le2  8810  2pos  8811  3pos  8814  4pos  8817  5pos  8820  6pos  8821  7pos  8822  8pos  8823  9pos  8824  neg1rr  8826  neg1lt0  8828  1lt2  8889  1lt3  8891  1lt4  8894  1lt5  8898  1lt6  8903  1lt7  8909  1lt8  8916  1lt9  8924  1ne2  8926  1ap2  8927  1le2  8928  1le3  8931  halflt1  8937  iap0  8943  addltmul  8956  elnnnn0c  9022  nn0ge2m1nn  9037  elnnz1  9077  zltp1le  9108  zleltp1  9109  recnz  9144  gtndiv  9146  3halfnz  9148  1lt10  9320  eluzp1m1  9349  eluzp1p1  9351  eluz2b2  9397  1rp  9445  divlt1lt  9511  divle1le  9512  nnledivrp  9553  0elunit  9769  1elunit  9770  divelunit  9785  lincmb01cmp  9786  iccf1o  9787  unitssre  9788  fzpreddisj  9851  fznatpl1  9856  fztpval  9863  qbtwnxr  10035  flqbi2  10064  fldiv4p1lem1div2  10078  flqdiv  10094  reexpcl  10310  reexpclzap  10313  expge0  10329  expge1  10330  expgt1  10331  bernneq  10412  bernneq2  10413  expnbnd  10415  expnlbnd  10416  expnlbnd2  10417  facwordi  10486  faclbnd3  10489  faclbnd6  10490  facavg  10492  cjexp  10665  re1  10669  im1  10670  rei  10671  imi  10672  caucvgre  10753  sqrt1  10818  sqrt2gt1lt2  10821  abs1  10844  caubnd2  10889  mulcn2  11081  reccn2ap  11082  expcnvap0  11271  geo2sum  11283  cvgratnnlemrate  11299  ere  11376  ege2le3  11377  efgt1  11403  resin4p  11425  recos4p  11426  sinbnd  11459  cosbnd  11460  sinbnd2  11461  cosbnd2  11462  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  cos1bnd  11466  cos2bnd  11467  sin01gt0  11468  cos01gt0  11469  sin02gt0  11470  sincos1sgn  11471  cos12dec  11474  ene1  11491  eap1  11492  halfleoddlt  11591  flodddiv4  11631  isprm3  11799  sqnprm  11816  coprm  11822  phibndlem  11892  exmidunben  11939  basendxnmulrndx  12073  setsmsbasg  12648  tgioo  12715  dveflem  12855  cosz12  12861  sinhalfpilem  12872  tangtx  12919  sincos4thpi  12921  pigt3  12925  coskpi  12929  ex-fl  12937  cvgcmp2nlemabs  13227  trilpolemclim  13229  trilpolemcl  13230  trilpolemisumle  13231  trilpolemeq1  13233  trilpolemlt1  13234