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

Theorem 1re 6824
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 6777 1 1
Colors of variables: wff set class
Syntax hints:   wcel 1390  cr 6710  1c1 6712
This theorem was proved from axioms:  ax-1re 6777
This theorem is referenced by:  0re  6825  1red  6840  0lt1  6938  peano2re  6946  peano2rem  7074  0reALT  7104  0le1  7271  1le1  7356  inelr  7368  1ap0  7374  eqneg  7490  ltp1  7591  ltm1  7593  recgt0  7597  mulgt1  7610  ltmulgt11  7611  lemulge11  7613  reclt1  7643  recgt1  7644  recgt1i  7645  recp1lt1  7646  recreclt  7647  cju  7694  peano5nni  7698  nnssre  7699  1nn  7706  nnge1  7718  nnle1eq1  7719  nngt0  7720  nnnlt1  7721  nn1gt1  7728  nngt1ne1  7729  nnrecre  7731  nnrecgt0  7732  nnsub  7733  2re  7765  3re  7769  4re  7772  5re  7774  6re  7776  7re  7778  8re  7780  9re  7782  10re  7784  0le2  7786  2pos  7787  3pos  7790  4pos  7792  5pos  7794  6pos  7795  7pos  7796  8pos  7797  9pos  7798  10pos  7799  neg1rr  7801  neg1lt0  7803  1lt2  7864  1lt3  7866  1lt4  7869  1lt5  7873  1lt6  7878  1lt7  7884  1lt8  7891  1lt9  7899  1lt10  7908  1ne2  7910  1le2  7911  1le3  7914  halflt1  7919  iap0  7925  addltmul  7938  elnnnn0c  8003  nn0ge2m1nn  8018  elnnz1  8044  zltp1le  8074  zleltp1  8075  recnz  8109  gtndiv  8111  eluzp1m1  8272  eluzp1p1  8274  eluz2b2  8316  1rp  8362  0elunit  8624  1elunit  8625  divelunit  8640  lincmb01cmp  8641  iccf1o  8642  unitssre  8643  fzpreddisj  8703  fznatpl1  8708  fztpval  8715  reexpcl  8926  reexpclzap  8929  expge0  8945  expge1  8946  expgt1  8947  bernneq  9022  bernneq2  9023  expnbnd  9025  expnlbnd  9026  expnlbnd2  9027  cjexp  9121  re1  9125  im1  9126  rei  9127  imi  9128  sqrt1  9216  abs1  9226
  Copyright terms: Public domain W3C validator