Theorem 1re 7118

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 7070	1 |- 1 e. RR

Syntax hints:   e. wcel 1433   RRcr 6980   1c1 6982

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

This theorem is referenced by:  0re  7119  1red  7134  0lt1  7236  peano2re  7244  peano2rem  7375  0reALT  7405  0le1  7585  1le1  7672  inelr  7684  1ap0  7690  eqneg  7820  ltp1  7922  ltm1  7924  recgt0  7928  mulgt1  7941  ltmulgt11  7942  lemulge11  7944  reclt1  7974  recgt1  7975  recgt1i  7976  recp1lt1  7977  recreclt  7978  cju  8038  peano5nni  8042  nnssre  8043  1nn  8050  nnge1  8062  nnle1eq1  8063  nngt0  8064  nnnlt1  8065  nn1gt1  8072  nngt1ne1  8073  nnrecre  8075  nnrecgt0  8076  nnsub  8077  2re  8109  3re  8113  4re  8116  5re  8118  6re  8120  7re  8122  8re  8124  9re  8126  0le2  8129  2pos  8130  3pos  8133  4pos  8136  5pos  8139  6pos  8140  7pos  8141  8pos  8142  9pos  8143  neg1rr  8145  neg1lt0  8147  1lt2  8201  1lt3  8203  1lt4  8206  1lt5  8210  1lt6  8215  1lt7  8221  1lt8  8228  1lt9  8236  1ne2  8238  1le2  8239  1le3  8242  halflt1  8248  iap0  8254  addltmul  8267  elnnnn0c  8333  nn0ge2m1nn  8348  elnnz1  8374  zltp1le  8405  zleltp1  8406  recnz  8440  gtndiv  8442  3halfnz  8444  1lt10  8615  eluzp1m1  8642  eluzp1p1  8644  eluz2b2  8690  1rp  8738  divlt1lt  8801  divle1le  8802  nnledivrp  8837  0elunit  9008  1elunit  9009  divelunit  9024  lincmb01cmp  9025  iccf1o  9026  unitssre  9027  fzpreddisj  9088  fznatpl1  9093  fztpval  9100  qbtwnxr  9266  flqbi2  9293  fldiv4p1lem1div2  9307  flqdiv  9323  reexpcl  9493  reexpclzap  9496  expge0  9512  expge1  9513  expgt1  9514  bernneq  9593  bernneq2  9594  expnbnd  9596  expnlbnd  9597  expnlbnd2  9598  facwordi  9667  faclbnd3  9670  faclbnd6  9671  facavg  9673  cjexp  9780  re1  9784  im1  9785  rei  9786  imi  9787  caucvgre  9867  sqrt1  9932  sqrt2gt1lt2  9935  abs1  9958  caubnd2  10003  mulcn2  10151  halfleoddlt  10294  flodddiv4  10334  isprm3  10500  sqnprm  10517  coprm  10523  ex-fl  10563