Theorem 1re 7424

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

Assertion

Ref	Expression
1re	|- 1 e. RR

Proof of Theorem 1re

Step	Hyp	Ref	Expression
1		ax-1re 7376	1 |- 1 e. RR

Syntax hints:   e. wcel 1436   RRcr 7286   1c1 7288

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

This theorem is referenced by:  0re  7425  1red  7440  0lt1  7547  peano2re  7555  peano2rem  7686  0reALT  7716  0le1  7896  1le1  7983  inelr  7995  1ap0  8001  eqneg  8131  ltp1  8233  ltm1  8235  recgt0  8239  mulgt1  8252  ltmulgt11  8253  lemulge11  8255  reclt1  8285  recgt1  8286  recgt1i  8287  recp1lt1  8288  recreclt  8289  cju  8349  peano5nni  8353  nnssre  8354  1nn  8361  nnge1  8373  nnle1eq1  8374  nngt0  8375  nnnlt1  8376  nn1gt1  8383  nngt1ne1  8384  nnrecre  8386  nnrecgt0  8387  nnsub  8388  2re  8420  3re  8424  4re  8427  5re  8429  6re  8431  7re  8433  8re  8435  9re  8437  0le2  8440  2pos  8441  3pos  8444  4pos  8447  5pos  8450  6pos  8451  7pos  8452  8pos  8453  9pos  8454  neg1rr  8456  neg1lt0  8458  1lt2  8512  1lt3  8514  1lt4  8517  1lt5  8521  1lt6  8526  1lt7  8532  1lt8  8539  1lt9  8547  1ne2  8549  1le2  8550  1le3  8553  halflt1  8559  iap0  8565  addltmul  8578  elnnnn0c  8644  nn0ge2m1nn  8659  elnnz1  8699  zltp1le  8730  zleltp1  8731  recnz  8765  gtndiv  8767  3halfnz  8769  1lt10  8940  eluzp1m1  8967  eluzp1p1  8969  eluz2b2  9015  1rp  9063  divlt1lt  9126  divle1le  9127  nnledivrp  9162  0elunit  9328  1elunit  9329  divelunit  9344  lincmb01cmp  9345  iccf1o  9346  unitssre  9347  fzpreddisj  9408  fznatpl1  9413  fztpval  9420  qbtwnxr  9590  flqbi2  9619  fldiv4p1lem1div2  9633  flqdiv  9649  reexpcl  9863  reexpclzap  9866  expge0  9882  expge1  9883  expgt1  9884  bernneq  9963  bernneq2  9964  expnbnd  9966  expnlbnd  9967  expnlbnd2  9968  facwordi  10037  faclbnd3  10040  faclbnd6  10041  facavg  10043  cjexp  10215  re1  10219  im1  10220  rei  10221  imi  10222  caucvgre  10302  sqrt1  10367  sqrt2gt1lt2  10370  abs1  10393  caubnd2  10438  mulcn2  10586  halfleoddlt  10761  flodddiv4  10801  isprm3  10967  sqnprm  10984  coprm  10990  phibndlem  11059  ex-fl  11083