ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  1re GIF version

Theorem 1re 6916
Description: 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
Assertion
Ref Expression
1re 1

Proof of Theorem 1re
StepHypRef Expression
1 ax-1re 6868 1 1
Colors of variables: wff set class
Syntax hints:   wcel 1393  cr 6778  1c1 6780
This theorem was proved from axioms:  ax-1re 6868
This theorem is referenced by:  0re  6917  1red  6932  0lt1  7030  peano2re  7038  peano2rem  7166  0reALT  7196  0le1  7363  1le1  7448  inelr  7460  1ap0  7466  eqneg  7582  ltp1  7683  ltm1  7685  recgt0  7689  mulgt1  7702  ltmulgt11  7703  lemulge11  7705  reclt1  7735  recgt1  7736  recgt1i  7737  recp1lt1  7738  recreclt  7739  cju  7786  peano5nni  7790  nnssre  7791  1nn  7798  nnge1  7810  nnle1eq1  7811  nngt0  7812  nnnlt1  7813  nn1gt1  7820  nngt1ne1  7821  nnrecre  7823  nnrecgt0  7824  nnsub  7825  2re  7857  3re  7861  4re  7864  5re  7866  6re  7868  7re  7870  8re  7872  9re  7874  10re  7876  0le2  7878  2pos  7879  3pos  7882  4pos  7884  5pos  7886  6pos  7887  7pos  7888  8pos  7889  9pos  7890  10pos  7891  neg1rr  7893  neg1lt0  7895  1lt2  7956  1lt3  7958  1lt4  7961  1lt5  7965  1lt6  7970  1lt7  7976  1lt8  7983  1lt9  7991  1lt10  8000  1ne2  8002  1le2  8003  1le3  8006  halflt1  8011  iap0  8017  addltmul  8030  elnnnn0c  8095  nn0ge2m1nn  8110  elnnz1  8136  zltp1le  8166  zleltp1  8167  recnz  8201  gtndiv  8203  eluzp1m1  8364  eluzp1p1  8366  eluz2b2  8408  1rp  8454  0elunit  8716  1elunit  8717  divelunit  8732  lincmb01cmp  8733  iccf1o  8734  unitssre  8735  fzpreddisj  8795  fznatpl1  8800  fztpval  8807  reexpcl  9019  reexpclzap  9022  expge0  9038  expge1  9039  expgt1  9040  bernneq  9115  bernneq2  9116  expnbnd  9118  expnlbnd  9119  expnlbnd2  9120  cjexp  9214  re1  9218  im1  9219  rei  9220  imi  9221  caucvgre  9300  sqrt1  9312  abs1  9322
  Copyright terms: Public domain W3C validator