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  8453  peano2re  8462  peano2rem  8593  0reALT  8623  0le1  8809  1le1  8900  inelr  8912  1ap0  8918  eqneg  9062  ltp1  9174  ltm1  9176  recgt0  9180  mulgt1  9193  ltmulgt11  9194  lemulge11  9196  reclt1  9226  recgt1  9227  recgt1i  9228  recp1lt1  9229  recreclt  9230  sup3exmid  9287  cju  9291  indfval  9299  indconst1  9303  peano5nni  9307  nnssre  9308  1nn  9315  nnge1  9327  nnle1eq1  9328  nngt0  9329  nnnlt1  9330  nn1gt1  9338  nngt1ne1  9339  nnrecre  9341  nnrecgt0  9342  nnsub  9343  2re  9374  3re  9378  4re  9381  5re  9383  6re  9385  7re  9387  8re  9389  9re  9391  0le2  9394  2pos  9395  3pos  9398  4pos  9401  5pos  9404  6pos  9405  7pos  9406  8pos  9407  9pos  9408  neg1rr  9410  neg1lt0  9412  1lt2  9474  1lt3  9476  1lt4  9479  1lt5  9483  1lt6  9488  1lt7  9494  1lt8  9501  1lt9  9509  1ne2  9511  1ap2  9512  1le2  9513  1le3  9516  halflt1  9522  iap0  9528  addltmul  9542  elnnnn0c  9608  nn0ge2m1nn  9627  elnnz1  9667  zltp1le  9699  zleltp1  9700  recnz  9739  gtndiv  9741  3halfnz  9743  1lt10  9915  eluzp1m1  9946  eluzp1p1  9948  eluz2b2  10003  1rp  10058  divlt1lt  10125  divle1le  10126  nnledivrp  10167  0elunit  10388  1elunit  10389  divelunit  10404  lincmb01cmp  10405  lincmble  10406  iccf1o  10407  unitssre  10408  fzpreddisj  10478  fznatpl1  10483  fztpval  10490  qbtwnxr  10692  flqbi2  10726  fldiv4p1lem1div2  10740  flqdiv  10758  seqf1oglem1  10956  reexpcl  10993  reexpclzap  10996  expge0  11012  expge1  11013  expgt1  11014  resq01  11095  bernneq  11098  bernneq2  11099  expnbnd  11101  expnlbnd  11102  expnlbnd2  11103  nn0ltexp2  11147  facwordi  11178  faclbnd3  11181  faclbnd6  11182  facavg  11184  hashtpglem  11298  lsw0  11352  cjexp  11658  re1  11663  im1  11664  rei  11665  imi  11666  caucvgre  11747  sqrt1  11812  sqrt2gt1lt2  11815  abs1  11838  caubnd2  11883  mulcn2  12078  reccn2ap  12079  expcnvap0  12269  geo2sum  12281  cvgratnnlemrate  12297  fprodge0  12404  fprodge1  12406  fprodle  12407  ere  12437  ege2le3  12438  efgt1  12464  resin4p  12485  recos4p  12486  sinbnd  12519  cosbnd  12520  sinbnd2  12521  cosbnd2  12522  ef01bndlem  12523  sin01bnd  12524  cos01bnd  12525  cos1bnd  12526  cos2bnd  12527  sinltxirr  12528  sin01gt0  12529  cos01gt0  12530  sin02gt0  12531  sincos1sgn  12532  cos12dec  12535  ene1  12552  eap1  12553  3dvds  12631  halfleoddlt  12661  flodddiv4  12703  isprm3  12896  sqnprm  12914  coprm  12922  phibndlem  12994  pythagtriplem3  13046  fldivp1  13127  pockthi  13137  ballotfilem2  13228  ballotfilem4  13241  ballotfilemi1  13245  ballotfilemic  13250  exmidunben  13317  basendxnmulrndx  13488  starvndxnbasendx  13496  scandxnbasendx  13508  vscandxnbasendx  13513  ipndxnbasendx  13526  basendxnocndx  13567  setsmsbasg  15580  tgioo  15655  dveflem  15827  reeff1olem  15872  reeff1o  15874  cosz12  15881  sinhalfpilem  15892  tangtx  15939  sincos4thpi  15941  pigt3  15945  coskpi  15949  cos0pilt1  15953  ioocosf1o  15955  loge  15968  logrpap0b  15977  logdivlti  15982  2logb9irrALT  16076  sqrt2cxp2logb9e3  16077  birthdaylem3  16089  perfectlem2  16114  lgsdir  16154  lgsne0  16157  lgsabs1  16158  lgsdinn0  16167  gausslemma2dlem0i  16176  lgseisen  16193  2lgslem3  16220  usgrexmpldifpr  16490  konigsberglem2  16730  konigsberglem3  16731  konigsberglem5  16733  ex-fl  16739  cvgcmp2nlemabs  17081  iooref1o  17083  trilpolemclim  17085  trilpolemcl  17086  trilpolemisumle  17087  trilpolemeq1  17089  trilpolemlt1  17090  apdiff  17097  nconstwlpolemgt0  17114