Theorem 1re 7758

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

Syntax hints:   e. wcel 1480   RRcr 7612   1c1 7614

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

This theorem is referenced by:  0re  7759  1red  7774  0lt1  7882  peano2re  7891  peano2rem  8022  0reALT  8052  0le1  8236  1le1  8327  inelr  8339  1ap0  8345  eqneg  8485  ltp1  8595  ltm1  8597  recgt0  8601  mulgt1  8614  ltmulgt11  8615  lemulge11  8617  reclt1  8647  recgt1  8648  recgt1i  8649  recp1lt1  8650  recreclt  8651  sup3exmid  8708  cju  8712  peano5nni  8716  nnssre  8717  1nn  8724  nnge1  8736  nnle1eq1  8737  nngt0  8738  nnnlt1  8739  nn1gt1  8747  nngt1ne1  8748  nnrecre  8750  nnrecgt0  8751  nnsub  8752  2re  8783  3re  8787  4re  8790  5re  8792  6re  8794  7re  8796  8re  8798  9re  8800  0le2  8803  2pos  8804  3pos  8807  4pos  8810  5pos  8813  6pos  8814  7pos  8815  8pos  8816  9pos  8817  neg1rr  8819  neg1lt0  8821  1lt2  8882  1lt3  8884  1lt4  8887  1lt5  8891  1lt6  8896  1lt7  8902  1lt8  8909  1lt9  8917  1ne2  8919  1ap2  8920  1le2  8921  1le3  8924  halflt1  8930  iap0  8936  addltmul  8949  elnnnn0c  9015  nn0ge2m1nn  9030  elnnz1  9070  zltp1le  9101  zleltp1  9102  recnz  9137  gtndiv  9139  3halfnz  9141  1lt10  9313  eluzp1m1  9342  eluzp1p1  9344  eluz2b2  9390  1rp  9438  divlt1lt  9504  divle1le  9505  nnledivrp  9546  0elunit  9762  1elunit  9763  divelunit  9778  lincmb01cmp  9779  iccf1o  9780  unitssre  9781  fzpreddisj  9844  fznatpl1  9849  fztpval  9856  qbtwnxr  10028  flqbi2  10057  fldiv4p1lem1div2  10071  flqdiv  10087  reexpcl  10303  reexpclzap  10306  expge0  10322  expge1  10323  expgt1  10324  bernneq  10405  bernneq2  10406  expnbnd  10408  expnlbnd  10409  expnlbnd2  10410  facwordi  10479  faclbnd3  10482  faclbnd6  10483  facavg  10485  cjexp  10658  re1  10662  im1  10663  rei  10664  imi  10665  caucvgre  10746  sqrt1  10811  sqrt2gt1lt2  10814  abs1  10837  caubnd2  10882  mulcn2  11074  reccn2ap  11075  expcnvap0  11264  geo2sum  11276  cvgratnnlemrate  11292  ere  11365  ege2le3  11366  efgt1  11392  resin4p  11414  recos4p  11415  sinbnd  11448  cosbnd  11449  sinbnd2  11450  cosbnd2  11451  ef01bndlem  11452  sin01bnd  11453  cos01bnd  11454  cos1bnd  11455  cos2bnd  11456  sin01gt0  11457  cos01gt0  11458  sin02gt0  11459  sincos1sgn  11460  cos12dec  11463  ene1  11480  eap1  11481  halfleoddlt  11580  flodddiv4  11620  isprm3  11788  sqnprm  11805  coprm  11811  phibndlem  11881  exmidunben  11928  basendxnmulrndx  12062  setsmsbasg  12637  tgioo  12704  dveflem  12844  cosz12  12850  sinhalfpilem  12861  tangtx  12908  sincos4thpi  12910  pigt3  12914  coskpi  12918  ex-fl  12926  cvgcmp2nlemabs  13216  trilpolemclim  13218  trilpolemcl  13219  trilpolemisumle  13220  trilpolemeq1  13222  trilpolemlt1  13223