Theorem 1re 8018

Description: 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)

Assertion

Ref	Expression
1re	⊢ 1 ∈ ℝ

Proof of Theorem 1re

Step	Hyp	Ref	Expression
1		ax-1re 7966	1 ⊢ 1 ∈ ℝ

Syntax hints:   ∈ wcel 2164  ℝcr 7871  1c1 7873

This theorem was proved from axioms:  ax-1re 7966

This theorem is referenced by:  0re  8019  1red  8034  1xr  8078  0lt1  8146  peano2re  8155  peano2rem  8286  0reALT  8316  0le1  8500  1le1  8591  inelr  8603  1ap0  8609  eqneg  8751  ltp1  8863  ltm1  8865  recgt0  8869  mulgt1  8882  ltmulgt11  8883  lemulge11  8885  reclt1  8915  recgt1  8916  recgt1i  8917  recp1lt1  8918  recreclt  8919  sup3exmid  8976  cju  8980  peano5nni  8985  nnssre  8986  1nn  8993  nnge1  9005  nnle1eq1  9006  nngt0  9007  nnnlt1  9008  nn1gt1  9016  nngt1ne1  9017  nnrecre  9019  nnrecgt0  9020  nnsub  9021  2re  9052  3re  9056  4re  9059  5re  9061  6re  9063  7re  9065  8re  9067  9re  9069  0le2  9072  2pos  9073  3pos  9076  4pos  9079  5pos  9082  6pos  9083  7pos  9084  8pos  9085  9pos  9086  neg1rr  9088  neg1lt0  9090  1lt2  9151  1lt3  9153  1lt4  9156  1lt5  9160  1lt6  9165  1lt7  9171  1lt8  9178  1lt9  9186  1ne2  9188  1ap2  9189  1le2  9190  1le3  9193  halflt1  9199  iap0  9205  addltmul  9219  elnnnn0c  9285  nn0ge2m1nn  9300  elnnz1  9340  zltp1le  9371  zleltp1  9372  recnz  9410  gtndiv  9412  3halfnz  9414  1lt10  9586  eluzp1m1  9616  eluzp1p1  9618  eluz2b2  9668  1rp  9723  divlt1lt  9790  divle1le  9791  nnledivrp  9832  0elunit  10052  1elunit  10053  divelunit  10068  lincmb01cmp  10069  iccf1o  10070  unitssre  10071  fzpreddisj  10137  fznatpl1  10142  fztpval  10149  qbtwnxr  10326  flqbi2  10360  fldiv4p1lem1div2  10374  flqdiv  10392  seqf1oglem1  10590  reexpcl  10627  reexpclzap  10630  expge0  10646  expge1  10647  expgt1  10648  bernneq  10731  bernneq2  10732  expnbnd  10734  expnlbnd  10735  expnlbnd2  10736  nn0ltexp2  10780  facwordi  10811  faclbnd3  10814  faclbnd6  10815  facavg  10817  cjexp  11037  re1  11041  im1  11042  rei  11043  imi  11044  caucvgre  11125  sqrt1  11190  sqrt2gt1lt2  11193  abs1  11216  caubnd2  11261  mulcn2  11455  reccn2ap  11456  expcnvap0  11645  geo2sum  11657  cvgratnnlemrate  11673  fprodge0  11780  fprodge1  11782  fprodle  11783  ere  11813  ege2le3  11814  efgt1  11840  resin4p  11861  recos4p  11862  sinbnd  11895  cosbnd  11896  sinbnd2  11897  cosbnd2  11898  ef01bndlem  11899  sin01bnd  11900  cos01bnd  11901  cos1bnd  11902  cos2bnd  11903  sinltxirr  11904  sin01gt0  11905  cos01gt0  11906  sin02gt0  11907  sincos1sgn  11908  cos12dec  11911  ene1  11928  eap1  11929  halfleoddlt  12035  flodddiv4  12075  isprm3  12256  sqnprm  12274  coprm  12282  phibndlem  12354  pythagtriplem3  12405  fldivp1  12486  pockthi  12496  exmidunben  12583  basendxnmulrndx  12751  starvndxnbasendx  12759  scandxnbasendx  12771  vscandxnbasendx  12776  ipndxnbasendx  12789  setsmsbasg  14647  tgioo  14714  dveflem  14872  reeff1olem  14906  reeff1o  14908  cosz12  14915  sinhalfpilem  14926  tangtx  14973  sincos4thpi  14975  pigt3  14979  coskpi  14983  cos0pilt1  14987  ioocosf1o  14989  loge  15002  logrpap0b  15011  logdivlti  15016  2logb9irrALT  15106  sqrt2cxp2logb9e3  15107  lgsdir  15151  lgsne0  15154  lgsabs1  15155  lgsdinn0  15164  gausslemma2dlem0i  15173  lgseisen  15190  ex-fl  15217  cvgcmp2nlemabs  15522  iooref1o  15524  trilpolemclim  15526  trilpolemcl  15527  trilpolemisumle  15528  trilpolemeq1  15530  trilpolemlt1  15531  apdiff  15538  nconstwlpolemgt0  15554