Theorem 1re 8325

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

This proof depends on syntax axioms:   e. wcel 2209   RRcr 8178   1c1 8180

This proof depends on axioms:  ax-1re 8273

This theorem is used by:  0re  8326  1red  8341  1xr  8384  0lt1  8454  peano2re  8463  peano2rem  8594  0reALT  8624  0le1  8810  1le1  8902  inelr  8914  1ap0  8920  eqneg  9064  ltp1  9176  ltm1  9178  recgt0  9182  mulgt1  9195  ltmulgt11  9196  lemulge11  9198  reclt1  9228  recgt1  9229  recgt1i  9230  recp1lt1  9231  recreclt  9232  sup3exmid  9289  cju  9293  indfval  9301  indconst1  9305  peano5nni  9309  nnssre  9310  1nn  9317  nnge1  9329  nnle1eq1  9330  nngt0  9331  nnnlt1  9332  nn1gt1  9340  nngt1ne1  9341  nnrecre  9343  nnrecgt0  9344  nnsub  9345  2re  9376  3re  9380  4re  9383  5re  9385  6re  9387  7re  9389  8re  9391  9re  9393  0le2  9396  2pos  9397  3pos  9400  4pos  9403  5pos  9406  6pos  9407  7pos  9408  8pos  9409  9pos  9410  neg1rr  9412  neg1lt0  9414  1lt2  9478  1lt3  9480  1lt4  9483  1lt5  9487  1lt6  9492  1lt7  9498  1lt8  9505  1lt9  9513  1ne2  9515  1ap2  9516  1le2  9517  1le3  9520  halflt1  9526  iap0  9532  addltmul  9546  elnnnn0c  9612  nn0ge2m1nn  9631  elnnz1  9671  zltp1le  9703  zleltp1  9704  recnz  9743  gtndiv  9745  3halfnz  9747  1lt10  9924  eluzp1m1  9955  eluzp1p1  9957  eluz2b2  10012  1rp  10068  divlt1lt  10135  divle1le  10136  nnledivrp  10177  0elunit  10398  1elunit  10399  divelunit  10414  lincmb01cmp  10415  lincmble  10416  iccf1o  10417  unitssre  10418  fzpreddisj  10488  fznatpl1  10493  fztpval  10500  qbtwnxr  10702  flqbi2  10739  fldiv4p1lem1div2  10753  flqdiv  10771  seqf1oglem1  10969  reexpcl  11006  reexpclzap  11009  expge0  11025  expge1  11026  expgt1  11027  resq01  11108  bernneq  11111  bernneq2  11112  expnbnd  11114  expnlbnd  11115  expnlbnd2  11116  nn0ltexp2  11161  facwordi  11192  faclbnd3  11195  faclbnd6  11196  facavg  11198  hashtpglem  11312  lsw0  11366  cjexp  11672  re1  11677  im1  11678  rei  11679  imi  11680  caucvgre  11761  sqrt1  11826  sqrt2gt1lt2  11829  abs1  11852  caubnd2  11898  mulcn2  12094  reccn2ap  12095  expcnvap0  12285  geo2sum  12297  cvgratnnlemrate  12313  fprodge0  12420  fprodge1  12422  fprodle  12423  ere  12453  ege2le3  12454  efgt1  12480  resin4p  12501  recos4p  12502  sinbnd  12535  cosbnd  12536  sinbnd2  12537  cosbnd2  12538  ef01bndlem  12539  sin01bnd  12540  cos01bnd  12541  cos1bnd  12542  cos2bnd  12543  sinltxirr  12544  sin01gt0  12545  cos01gt0  12546  sin02gt0  12547  sincos1sgn  12548  cos12dec  12551  ene1  12568  eap1  12569  3dvds  12647  halfleoddlt  12677  flodddiv4  12719  isprm3  12912  sqnprm  12931  coprm  12939  phibndlem  13014  pythagtriplem3  13066  fldivp1  13147  pockthi  13157  ballotfilem2  13277  ballotfilem4  13290  ballotfilemi1  13294  ballotfilemic  13299  exmidunben  13366  basendxnmulrndx  13537  starvndxnbasendx  13545  scandxnbasendx  13557  vscandxnbasendx  13562  ipndxnbasendx  13575  basendxnocndx  13616  setsmsbasg  15629  tgioo  15704  dveflem  15876  reeff1olem  15921  reeff1o  15923  cosz12  15931  sinhalfpilem  15942  tangtx  15989  sincos4thpi  15991  pigt3  15995  coskpi  15999  cos0pilt1  16003  ioocosf1o  16005  loge  16018  logrpap0b  16028  logdivlti  16033  2logb9irrALT  16129  sqrt2cxp2logb9e3  16130  birthdaylem3  16146  ppiublem1  16192  ppiqub  16194  perfectlem2  16198  bposlem1  16209  bposlem2  16210  bposlem5  16213  lgsdir  16252  lgsne0  16255  lgsabs1  16256  lgsdinn0  16265  gausslemma2dlem0i  16274  lgseisen  16291  2lgslem3  16318  usgrexmpldifpr  16588  konigsberglem2  16828  konigsberglem3  16829  konigsberglem5  16831  ex-fl  16837  cvgcmp2nlemabs  17179  iooref1o  17181  trilpolemclim  17183  trilpolemcl  17184  trilpolemisumle  17185  trilpolemeq1  17187  trilpolemlt1  17188  apdiff  17195  nconstwlpolemgt0  17212