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

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

Proof of Theorem 1re
StepHypRef Expression
1 ax-1re 7737 1  |-  1  e.  RR
Colors of variables: wff set class
Syntax hints:    e. wcel 1481   RRcr 7642   1c1 7644
This theorem was proved from axioms:  ax-1re 7737
This theorem is referenced by:  0re  7789  1red  7804  0lt1  7912  peano2re  7921  peano2rem  8052  0reALT  8082  0le1  8266  1le1  8357  inelr  8369  1ap0  8375  eqneg  8515  ltp1  8625  ltm1  8627  recgt0  8631  mulgt1  8644  ltmulgt11  8645  lemulge11  8647  reclt1  8677  recgt1  8678  recgt1i  8679  recp1lt1  8680  recreclt  8681  sup3exmid  8738  cju  8742  peano5nni  8746  nnssre  8747  1nn  8754  nnge1  8766  nnle1eq1  8767  nngt0  8768  nnnlt1  8769  nn1gt1  8777  nngt1ne1  8778  nnrecre  8780  nnrecgt0  8781  nnsub  8782  2re  8813  3re  8817  4re  8820  5re  8822  6re  8824  7re  8826  8re  8828  9re  8830  0le2  8833  2pos  8834  3pos  8837  4pos  8840  5pos  8843  6pos  8844  7pos  8845  8pos  8846  9pos  8847  neg1rr  8849  neg1lt0  8851  1lt2  8912  1lt3  8914  1lt4  8917  1lt5  8921  1lt6  8926  1lt7  8932  1lt8  8939  1lt9  8947  1ne2  8949  1ap2  8950  1le2  8951  1le3  8954  halflt1  8960  iap0  8966  addltmul  8979  elnnnn0c  9045  nn0ge2m1nn  9060  elnnz1  9100  zltp1le  9131  zleltp1  9132  recnz  9167  gtndiv  9169  3halfnz  9171  1lt10  9343  eluzp1m1  9372  eluzp1p1  9374  eluz2b2  9423  1rp  9473  divlt1lt  9540  divle1le  9541  nnledivrp  9582  0elunit  9798  1elunit  9799  divelunit  9814  lincmb01cmp  9815  iccf1o  9816  unitssre  9817  fzpreddisj  9881  fznatpl1  9886  fztpval  9893  qbtwnxr  10065  flqbi2  10094  fldiv4p1lem1div2  10108  flqdiv  10124  reexpcl  10340  reexpclzap  10343  expge0  10359  expge1  10360  expgt1  10361  bernneq  10442  bernneq2  10443  expnbnd  10445  expnlbnd  10446  expnlbnd2  10447  facwordi  10517  faclbnd3  10520  faclbnd6  10521  facavg  10523  cjexp  10696  re1  10700  im1  10701  rei  10702  imi  10703  caucvgre  10784  sqrt1  10849  sqrt2gt1lt2  10852  abs1  10875  caubnd2  10920  mulcn2  11112  reccn2ap  11113  expcnvap0  11302  geo2sum  11314  cvgratnnlemrate  11330  ere  11411  ege2le3  11412  efgt1  11438  resin4p  11459  recos4p  11460  sinbnd  11493  cosbnd  11494  sinbnd2  11495  cosbnd2  11496  ef01bndlem  11497  sin01bnd  11498  cos01bnd  11499  cos1bnd  11500  cos2bnd  11501  sin01gt0  11502  cos01gt0  11503  sin02gt0  11504  sincos1sgn  11505  cos12dec  11508  ene1  11525  eap1  11526  halfleoddlt  11625  flodddiv4  11665  isprm3  11833  sqnprm  11850  coprm  11856  phibndlem  11926  exmidunben  11973  basendxnmulrndx  12110  setsmsbasg  12685  tgioo  12752  dveflem  12893  reeff1olem  12898  reeff1o  12900  cosz12  12907  sinhalfpilem  12918  tangtx  12965  sincos4thpi  12967  pigt3  12971  coskpi  12975  cos0pilt1  12979  ioocosf1o  12981  loge  12994  logrpap0b  13003  logdivlti  13008  2logb9irrALT  13097  sqrt2cxp2logb9e3  13098  ex-fl  13106  cvgcmp2nlemabs  13400  trilpolemclim  13402  trilpolemcl  13403  trilpolemisumle  13404  trilpolemeq1  13406  trilpolemlt1  13407  apdiff  13414  iooref1o  13424
  Copyright terms: Public domain W3C validator