Theorem 1re 7919

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 7868	1 ⊢ 1 ∈ ℝ

Syntax hints:   ∈ wcel 2141  ℝcr 7773  1c1 7775

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

This theorem is referenced by:  0re  7920  1red  7935  1xr  7978  0lt1  8046  peano2re  8055  peano2rem  8186  0reALT  8216  0le1  8400  1le1  8491  inelr  8503  1ap0  8509  eqneg  8649  ltp1  8760  ltm1  8762  recgt0  8766  mulgt1  8779  ltmulgt11  8780  lemulge11  8782  reclt1  8812  recgt1  8813  recgt1i  8814  recp1lt1  8815  recreclt  8816  sup3exmid  8873  cju  8877  peano5nni  8881  nnssre  8882  1nn  8889  nnge1  8901  nnle1eq1  8902  nngt0  8903  nnnlt1  8904  nn1gt1  8912  nngt1ne1  8913  nnrecre  8915  nnrecgt0  8916  nnsub  8917  2re  8948  3re  8952  4re  8955  5re  8957  6re  8959  7re  8961  8re  8963  9re  8965  0le2  8968  2pos  8969  3pos  8972  4pos  8975  5pos  8978  6pos  8979  7pos  8980  8pos  8981  9pos  8982  neg1rr  8984  neg1lt0  8986  1lt2  9047  1lt3  9049  1lt4  9052  1lt5  9056  1lt6  9061  1lt7  9067  1lt8  9074  1lt9  9082  1ne2  9084  1ap2  9085  1le2  9086  1le3  9089  halflt1  9095  iap0  9101  addltmul  9114  elnnnn0c  9180  nn0ge2m1nn  9195  elnnz1  9235  zltp1le  9266  zleltp1  9267  recnz  9305  gtndiv  9307  3halfnz  9309  1lt10  9481  eluzp1m1  9510  eluzp1p1  9512  eluz2b2  9562  1rp  9614  divlt1lt  9681  divle1le  9682  nnledivrp  9723  0elunit  9943  1elunit  9944  divelunit  9959  lincmb01cmp  9960  iccf1o  9961  unitssre  9962  fzpreddisj  10027  fznatpl1  10032  fztpval  10039  qbtwnxr  10214  flqbi2  10247  fldiv4p1lem1div2  10261  flqdiv  10277  reexpcl  10493  reexpclzap  10496  expge0  10512  expge1  10513  expgt1  10514  bernneq  10596  bernneq2  10597  expnbnd  10599  expnlbnd  10600  expnlbnd2  10601  nn0ltexp2  10644  facwordi  10674  faclbnd3  10677  faclbnd6  10678  facavg  10680  cjexp  10857  re1  10861  im1  10862  rei  10863  imi  10864  caucvgre  10945  sqrt1  11010  sqrt2gt1lt2  11013  abs1  11036  caubnd2  11081  mulcn2  11275  reccn2ap  11276  expcnvap0  11465  geo2sum  11477  cvgratnnlemrate  11493  fprodge0  11600  fprodge1  11602  fprodle  11603  ere  11633  ege2le3  11634  efgt1  11660  resin4p  11681  recos4p  11682  sinbnd  11715  cosbnd  11716  sinbnd2  11717  cosbnd2  11718  ef01bndlem  11719  sin01bnd  11720  cos01bnd  11721  cos1bnd  11722  cos2bnd  11723  sin01gt0  11724  cos01gt0  11725  sin02gt0  11726  sincos1sgn  11727  cos12dec  11730  ene1  11747  eap1  11748  halfleoddlt  11853  flodddiv4  11893  isprm3  12072  sqnprm  12090  coprm  12098  phibndlem  12170  pythagtriplem3  12221  fldivp1  12300  pockthi  12310  exmidunben  12381  basendxnmulrndx  12532  setsmsbasg  13273  tgioo  13340  dveflem  13481  reeff1olem  13486  reeff1o  13488  cosz12  13495  sinhalfpilem  13506  tangtx  13553  sincos4thpi  13555  pigt3  13559  coskpi  13563  cos0pilt1  13567  ioocosf1o  13569  loge  13582  logrpap0b  13591  logdivlti  13596  2logb9irrALT  13686  sqrt2cxp2logb9e3  13687  lgsdir  13730  lgsne0  13733  lgsabs1  13734  lgsdinn0  13743  ex-fl  13760  cvgcmp2nlemabs  14064  iooref1o  14066  trilpolemclim  14068  trilpolemcl  14069  trilpolemisumle  14070  trilpolemeq1  14072  trilpolemlt1  14073  apdiff  14080  nconstwlpolemgt0  14095