Theorem 1re 7431

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

Syntax hints:   ∈ wcel 1436  ℝcr 7293  1c1 7295

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

This theorem is referenced by:  0re  7432  1red  7447  0lt1  7554  peano2re  7562  peano2rem  7693  0reALT  7723  0le1  7903  1le1  7990  inelr  8002  1ap0  8008  eqneg  8138  ltp1  8240  ltm1  8242  recgt0  8246  mulgt1  8259  ltmulgt11  8260  lemulge11  8262  reclt1  8292  recgt1  8293  recgt1i  8294  recp1lt1  8295  recreclt  8296  cju  8356  peano5nni  8360  nnssre  8361  1nn  8368  nnge1  8380  nnle1eq1  8381  nngt0  8382  nnnlt1  8383  nn1gt1  8390  nngt1ne1  8391  nnrecre  8393  nnrecgt0  8394  nnsub  8395  2re  8427  3re  8431  4re  8434  5re  8436  6re  8438  7re  8440  8re  8442  9re  8444  0le2  8447  2pos  8448  3pos  8451  4pos  8454  5pos  8457  6pos  8458  7pos  8459  8pos  8460  9pos  8461  neg1rr  8463  neg1lt0  8465  1lt2  8519  1lt3  8521  1lt4  8524  1lt5  8528  1lt6  8533  1lt7  8539  1lt8  8546  1lt9  8554  1ne2  8556  1le2  8557  1le3  8560  halflt1  8566  iap0  8572  addltmul  8585  elnnnn0c  8651  nn0ge2m1nn  8666  elnnz1  8706  zltp1le  8737  zleltp1  8738  recnz  8772  gtndiv  8774  3halfnz  8776  1lt10  8947  eluzp1m1  8974  eluzp1p1  8976  eluz2b2  9022  1rp  9070  divlt1lt  9133  divle1le  9134  nnledivrp  9169  0elunit  9335  1elunit  9336  divelunit  9351  lincmb01cmp  9352  iccf1o  9353  unitssre  9354  fzpreddisj  9415  fznatpl1  9420  fztpval  9427  qbtwnxr  9597  flqbi2  9626  fldiv4p1lem1div2  9640  flqdiv  9656  reexpcl  9871  reexpclzap  9874  expge0  9890  expge1  9891  expgt1  9892  bernneq  9971  bernneq2  9972  expnbnd  9974  expnlbnd  9975  expnlbnd2  9976  facwordi  10045  faclbnd3  10048  faclbnd6  10049  facavg  10051  cjexp  10223  re1  10227  im1  10228  rei  10229  imi  10230  caucvgre  10310  sqrt1  10375  sqrt2gt1lt2  10378  abs1  10401  caubnd2  10446  mulcn2  10595  halfleoddlt  10776  flodddiv4  10816  isprm3  10982  sqnprm  10999  coprm  11005  phibndlem  11074  ex-fl  11098