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

Theorem 1re 7084
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 7036 1 1 ∈ ℝ
Colors of variables: wff set class
Syntax hints:  wcel 1409  cr 6946  1c1 6948
This theorem was proved from axioms:  ax-1re 7036
This theorem is referenced by:  0re  7085  1red  7100  0lt1  7202  peano2re  7210  peano2rem  7341  0reALT  7371  0le1  7550  1le1  7637  inelr  7649  1ap0  7655  eqneg  7783  ltp1  7885  ltm1  7887  recgt0  7891  mulgt1  7904  ltmulgt11  7905  lemulge11  7907  reclt1  7937  recgt1  7938  recgt1i  7939  recp1lt1  7940  recreclt  7941  cju  7989  peano5nni  7993  nnssre  7994  1nn  8001  nnge1  8013  nnle1eq1  8014  nngt0  8015  nnnlt1  8016  nn1gt1  8023  nngt1ne1  8024  nnrecre  8026  nnrecgt0  8027  nnsub  8028  2re  8060  3re  8064  4re  8067  5re  8069  6re  8071  7re  8073  8re  8075  9re  8077  0le2  8080  2pos  8081  3pos  8084  4pos  8087  5pos  8090  6pos  8091  7pos  8092  8pos  8093  9pos  8094  neg1rr  8096  neg1lt0  8098  1lt2  8152  1lt3  8154  1lt4  8157  1lt5  8161  1lt6  8166  1lt7  8172  1lt8  8179  1lt9  8187  1ne2  8189  1le2  8190  1le3  8193  halflt1  8199  iap0  8205  addltmul  8218  elnnnn0c  8284  nn0ge2m1nn  8299  elnnz1  8325  zltp1le  8356  zleltp1  8357  recnz  8391  gtndiv  8393  3halfnz  8395  1lt10  8565  eluzp1m1  8592  eluzp1p1  8594  eluz2b2  8637  1rp  8685  divlt1lt  8748  divle1le  8749  nnledivrp  8784  0elunit  8955  1elunit  8956  divelunit  8971  lincmb01cmp  8972  iccf1o  8973  unitssre  8974  fzpreddisj  9035  fznatpl1  9040  fztpval  9047  qbtwnxr  9214  flqbi2  9241  fldiv4p1lem1div2  9255  flqdiv  9271  reexpcl  9437  reexpclzap  9440  expge0  9456  expge1  9457  expgt1  9458  bernneq  9537  bernneq2  9538  expnbnd  9540  expnlbnd  9541  expnlbnd2  9542  facwordi  9608  faclbnd3  9611  faclbnd6  9612  facavg  9614  cjexp  9721  re1  9725  im1  9726  rei  9727  imi  9728  caucvgre  9808  sqrt1  9873  sqrt2gt1lt2  9876  abs1  9899  caubnd2  9944  mulcn2  10064  halfleoddlt  10206  flodddiv4  10246  ex-fl  10279
  Copyright terms: Public domain W3C validator