Theorem 1re 8326

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

This proof depends on syntax axioms:   e. wcel 2209   RRcr 8179   1c1 8181

This proof depends on axioms:  ax-1re 8274

This theorem is used by:  0re  8327  1red  8342  1xr  8385  0lt1  8455  peano2re  8464  peano2rem  8595  0reALT  8625  0le1  8811  1le1  8903  inelr  8915  1ap0  8921  eqneg  9065  ltp1  9177  ltm1  9179  recgt0  9183  mulgt1  9196  ltmulgt11  9197  lemulge11  9199  reclt1  9229  recgt1  9230  recgt1i  9231  recp1lt1  9232  recreclt  9233  sup3exmid  9290  cju  9294  indfval  9302  indconst1  9306  peano5nni  9310  nnssre  9311  1nn  9318  nnge1  9330  nnle1eq1  9331  nngt0  9332  nnnlt1  9333  nn1gt1  9341  nngt1ne1  9342  nnrecre  9344  nnrecgt0  9345  nnsub  9346  2re  9377  3re  9381  4re  9384  5re  9386  6re  9388  7re  9390  8re  9392  9re  9394  0le2  9397  2pos  9398  3pos  9401  4pos  9404  5pos  9407  6pos  9408  7pos  9409  8pos  9410  9pos  9411  neg1rr  9413  neg1lt0  9415  1lt2  9479  1lt3  9481  1lt4  9484  1lt5  9488  1lt6  9493  1lt7  9499  1lt8  9506  1lt9  9514  1ne2  9516  1ap2  9517  1le2  9518  1le3  9521  halflt1  9527  iap0  9533  addltmul  9547  elnnnn0c  9613  nn0ge2m1nn  9632  elnnz1  9672  zltp1le  9704  zleltp1  9705  recnz  9744  gtndiv  9746  3halfnz  9748  1lt10  9925  eluzp1m1  9956  eluzp1p1  9958  eluz2b2  10013  1rp  10069  divlt1lt  10136  divle1le  10137  nnledivrp  10178  0elunit  10399  1elunit  10400  divelunit  10415  lincmb01cmp  10416  lincmble  10417  iccf1o  10418  unitssre  10419  fzpreddisj  10489  fznatpl1  10494  fztpval  10501  qbtwnxr  10703  flqbi2  10741  fldiv4p1lem1div2  10755  flqdiv  10773  seqf1oglem1  10971  reexpcl  11008  reexpclzap  11011  expge0  11027  expge1  11028  expgt1  11029  resq01  11110  bernneq  11113  bernneq2  11114  expnbnd  11116  expnlbnd  11117  expnlbnd2  11118  nn0ltexp2  11163  facwordi  11194  faclbnd3  11197  faclbnd6  11198  facavg  11200  hashtpglem  11314  lsw0  11368  cjexp  11674  re1  11679  im1  11680  rei  11681  imi  11682  caucvgre  11763  sqrt1  11828  sqrt2gt1lt2  11831  abs1  11854  caubnd2  11900  mulcn2  12097  reccn2ap  12098  expcnvap0  12288  geo2sum  12300  cvgratnnlemrate  12316  fprodge0  12423  fprodge1  12425  fprodle  12426  ere  12456  ege2le3  12457  efgt1  12483  resin4p  12504  recos4p  12505  sinbnd  12538  cosbnd  12539  sinbnd2  12540  cosbnd2  12541  ef01bndlem  12542  sin01bnd  12543  cos01bnd  12544  cos1bnd  12545  cos2bnd  12546  sinltxirr  12547  sin01gt0  12548  cos01gt0  12549  sin02gt0  12550  sincos1sgn  12551  cos12dec  12554  ene1  12571  eap1  12572  3dvds  12650  halfleoddlt  12680  flodddiv4  12722  isprm3  12915  sqnprm  12934  coprm  12942  phibndlem  13017  pythagtriplem3  13069  fldivp1  13150  pockthi  13160  ballotfilem2  13280  ballotfilem4  13293  ballotfilemi1  13297  ballotfilemic  13302  exmidunben  13369  basendxnmulrndx  13541  starvndxnbasendx  13549  scandxnbasendx  13561  vscandxnbasendx  13566  ipndxnbasendx  13579  basendxnocndx  13620  setsmsbasg  15671  tgioo  15746  dveflem  15918  reeff1olem  15963  reeff1o  15965  cosz12  15973  sinhalfpilem  15984  tangtx  16031  sincos4thpi  16033  pigt3  16037  coskpi  16041  cos0pilt1  16045  ioocosf1o  16047  loge  16060  logrpap0b  16070  logdivlti  16075  2logb9irrALT  16171  sqrt2cxp2logb9e3  16172  birthdaylem3  16188  ppiublem1  16252  ppiqub  16254  chtublem  16256  chtqub  16257  perfectlem2  16261  bposlem1  16272  bposlem2  16273  bposlem5  16276  bposlem8  16279  lgsdir  16320  lgsne0  16323  lgsabs1  16324  lgsdinn0  16333  gausslemma2dlem0i  16342  lgseisen  16359  2lgslem3  16386  usgrexmpldifpr  16656  konigsberglem2  16896  konigsberglem3  16897  konigsberglem5  16899  ex-fl  16905  cvgcmp2nlemabs  17247  iooref1o  17249  trilpolemclim  17252  trilpolemcl  17253  trilpolemisumle  17254  trilpolemeq1  17256  trilpolemlt1  17257  apdiff  17264  nconstwlpolemgt0  17281