Theorem 1re 7955

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

Syntax hints:   ∈ wcel 2148  ℝcr 7809  1c1 7811

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

This theorem is referenced by:  0re  7956  1red  7971  1xr  8015  0lt1  8083  peano2re  8092  peano2rem  8223  0reALT  8253  0le1  8437  1le1  8528  inelr  8540  1ap0  8546  eqneg  8688  ltp1  8800  ltm1  8802  recgt0  8806  mulgt1  8819  ltmulgt11  8820  lemulge11  8822  reclt1  8852  recgt1  8853  recgt1i  8854  recp1lt1  8855  recreclt  8856  sup3exmid  8913  cju  8917  peano5nni  8921  nnssre  8922  1nn  8929  nnge1  8941  nnle1eq1  8942  nngt0  8943  nnnlt1  8944  nn1gt1  8952  nngt1ne1  8953  nnrecre  8955  nnrecgt0  8956  nnsub  8957  2re  8988  3re  8992  4re  8995  5re  8997  6re  8999  7re  9001  8re  9003  9re  9005  0le2  9008  2pos  9009  3pos  9012  4pos  9015  5pos  9018  6pos  9019  7pos  9020  8pos  9021  9pos  9022  neg1rr  9024  neg1lt0  9026  1lt2  9087  1lt3  9089  1lt4  9092  1lt5  9096  1lt6  9101  1lt7  9107  1lt8  9114  1lt9  9122  1ne2  9124  1ap2  9125  1le2  9126  1le3  9129  halflt1  9135  iap0  9141  addltmul  9154  elnnnn0c  9220  nn0ge2m1nn  9235  elnnz1  9275  zltp1le  9306  zleltp1  9307  recnz  9345  gtndiv  9347  3halfnz  9349  1lt10  9521  eluzp1m1  9550  eluzp1p1  9552  eluz2b2  9602  1rp  9656  divlt1lt  9723  divle1le  9724  nnledivrp  9765  0elunit  9985  1elunit  9986  divelunit  10001  lincmb01cmp  10002  iccf1o  10003  unitssre  10004  fzpreddisj  10070  fznatpl1  10075  fztpval  10082  qbtwnxr  10257  flqbi2  10290  fldiv4p1lem1div2  10304  flqdiv  10320  reexpcl  10536  reexpclzap  10539  expge0  10555  expge1  10556  expgt1  10557  bernneq  10640  bernneq2  10641  expnbnd  10643  expnlbnd  10644  expnlbnd2  10645  nn0ltexp2  10688  facwordi  10719  faclbnd3  10722  faclbnd6  10723  facavg  10725  cjexp  10901  re1  10905  im1  10906  rei  10907  imi  10908  caucvgre  10989  sqrt1  11054  sqrt2gt1lt2  11057  abs1  11080  caubnd2  11125  mulcn2  11319  reccn2ap  11320  expcnvap0  11509  geo2sum  11521  cvgratnnlemrate  11537  fprodge0  11644  fprodge1  11646  fprodle  11647  ere  11677  ege2le3  11678  efgt1  11704  resin4p  11725  recos4p  11726  sinbnd  11759  cosbnd  11760  sinbnd2  11761  cosbnd2  11762  ef01bndlem  11763  sin01bnd  11764  cos01bnd  11765  cos1bnd  11766  cos2bnd  11767  sin01gt0  11768  cos01gt0  11769  sin02gt0  11770  sincos1sgn  11771  cos12dec  11774  ene1  11791  eap1  11792  halfleoddlt  11898  flodddiv4  11938  isprm3  12117  sqnprm  12135  coprm  12143  phibndlem  12215  pythagtriplem3  12266  fldivp1  12345  pockthi  12355  exmidunben  12426  basendxnmulrndx  12591  starvndxnbasendx  12599  scandxnbasendx  12611  vscandxnbasendx  12616  ipndxnbasendx  12629  setsmsbasg  13949  tgioo  14016  dveflem  14157  reeff1olem  14162  reeff1o  14164  cosz12  14171  sinhalfpilem  14182  tangtx  14229  sincos4thpi  14231  pigt3  14235  coskpi  14239  cos0pilt1  14243  ioocosf1o  14245  loge  14258  logrpap0b  14267  logdivlti  14272  2logb9irrALT  14362  sqrt2cxp2logb9e3  14363  lgsdir  14406  lgsne0  14409  lgsabs1  14410  lgsdinn0  14419  ex-fl  14447  cvgcmp2nlemabs  14750  iooref1o  14752  trilpolemclim  14754  trilpolemcl  14755  trilpolemisumle  14756  trilpolemeq1  14758  trilpolemlt1  14759  apdiff  14766  nconstwlpolemgt0  14781