Theorem 1re 7232

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

Syntax hints:   e. wcel 1434   RRcr 7094   1c1 7096

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

This theorem is referenced by:  0re  7233  1red  7248  0lt1  7355  peano2re  7363  peano2rem  7494  0reALT  7524  0le1  7704  1le1  7791  inelr  7803  1ap0  7809  eqneg  7939  ltp1  8041  ltm1  8043  recgt0  8047  mulgt1  8060  ltmulgt11  8061  lemulge11  8063  reclt1  8093  recgt1  8094  recgt1i  8095  recp1lt1  8096  recreclt  8097  cju  8157  peano5nni  8161  nnssre  8162  1nn  8169  nnge1  8181  nnle1eq1  8182  nngt0  8183  nnnlt1  8184  nn1gt1  8191  nngt1ne1  8192  nnrecre  8194  nnrecgt0  8195  nnsub  8196  2re  8228  3re  8232  4re  8235  5re  8237  6re  8239  7re  8241  8re  8243  9re  8245  0le2  8248  2pos  8249  3pos  8252  4pos  8255  5pos  8258  6pos  8259  7pos  8260  8pos  8261  9pos  8262  neg1rr  8264  neg1lt0  8266  1lt2  8320  1lt3  8322  1lt4  8325  1lt5  8329  1lt6  8334  1lt7  8340  1lt8  8347  1lt9  8355  1ne2  8357  1le2  8358  1le3  8361  halflt1  8367  iap0  8373  addltmul  8386  elnnnn0c  8452  nn0ge2m1nn  8467  elnnz1  8507  zltp1le  8538  zleltp1  8539  recnz  8573  gtndiv  8575  3halfnz  8577  1lt10  8748  eluzp1m1  8775  eluzp1p1  8777  eluz2b2  8823  1rp  8871  divlt1lt  8934  divle1le  8935  nnledivrp  8970  0elunit  9136  1elunit  9137  divelunit  9152  lincmb01cmp  9153  iccf1o  9154  unitssre  9155  fzpreddisj  9216  fznatpl1  9221  fztpval  9228  qbtwnxr  9396  flqbi2  9425  fldiv4p1lem1div2  9439  flqdiv  9455  reexpcl  9642  reexpclzap  9645  expge0  9661  expge1  9662  expgt1  9663  bernneq  9742  bernneq2  9743  expnbnd  9745  expnlbnd  9746  expnlbnd2  9747  facwordi  9816  faclbnd3  9819  faclbnd6  9820  facavg  9822  cjexp  9981  re1  9985  im1  9986  rei  9987  imi  9988  caucvgre  10068  sqrt1  10133  sqrt2gt1lt2  10136  abs1  10159  caubnd2  10204  mulcn2  10352  halfleoddlt  10501  flodddiv4  10541  isprm3  10707  sqnprm  10724  coprm  10730  phibndlem  10799  ex-fl  10823