Theorem 1re 8044

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

Syntax hints:   ∈ wcel 2167  ℝcr 7897  1c1 7899

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

This theorem is referenced by:  0re  8045  1red  8060  1xr  8104  0lt1  8172  peano2re  8181  peano2rem  8312  0reALT  8342  0le1  8527  1le1  8618  inelr  8630  1ap0  8636  eqneg  8778  ltp1  8890  ltm1  8892  recgt0  8896  mulgt1  8909  ltmulgt11  8910  lemulge11  8912  reclt1  8942  recgt1  8943  recgt1i  8944  recp1lt1  8945  recreclt  8946  sup3exmid  9003  cju  9007  peano5nni  9012  nnssre  9013  1nn  9020  nnge1  9032  nnle1eq1  9033  nngt0  9034  nnnlt1  9035  nn1gt1  9043  nngt1ne1  9044  nnrecre  9046  nnrecgt0  9047  nnsub  9048  2re  9079  3re  9083  4re  9086  5re  9088  6re  9090  7re  9092  8re  9094  9re  9096  0le2  9099  2pos  9100  3pos  9103  4pos  9106  5pos  9109  6pos  9110  7pos  9111  8pos  9112  9pos  9113  neg1rr  9115  neg1lt0  9117  1lt2  9179  1lt3  9181  1lt4  9184  1lt5  9188  1lt6  9193  1lt7  9199  1lt8  9206  1lt9  9214  1ne2  9216  1ap2  9217  1le2  9218  1le3  9221  halflt1  9227  iap0  9233  addltmul  9247  elnnnn0c  9313  nn0ge2m1nn  9328  elnnz1  9368  zltp1le  9399  zleltp1  9400  recnz  9438  gtndiv  9440  3halfnz  9442  1lt10  9614  eluzp1m1  9644  eluzp1p1  9646  eluz2b2  9696  1rp  9751  divlt1lt  9818  divle1le  9819  nnledivrp  9860  0elunit  10080  1elunit  10081  divelunit  10096  lincmb01cmp  10097  iccf1o  10098  unitssre  10099  fzpreddisj  10165  fznatpl1  10170  fztpval  10177  qbtwnxr  10366  flqbi2  10400  fldiv4p1lem1div2  10414  flqdiv  10432  seqf1oglem1  10630  reexpcl  10667  reexpclzap  10670  expge0  10686  expge1  10687  expgt1  10688  bernneq  10771  bernneq2  10772  expnbnd  10774  expnlbnd  10775  expnlbnd2  10776  nn0ltexp2  10820  facwordi  10851  faclbnd3  10854  faclbnd6  10855  facavg  10857  cjexp  11077  re1  11081  im1  11082  rei  11083  imi  11084  caucvgre  11165  sqrt1  11230  sqrt2gt1lt2  11233  abs1  11256  caubnd2  11301  mulcn2  11496  reccn2ap  11497  expcnvap0  11686  geo2sum  11698  cvgratnnlemrate  11714  fprodge0  11821  fprodge1  11823  fprodle  11824  ere  11854  ege2le3  11855  efgt1  11881  resin4p  11902  recos4p  11903  sinbnd  11936  cosbnd  11937  sinbnd2  11938  cosbnd2  11939  ef01bndlem  11940  sin01bnd  11941  cos01bnd  11942  cos1bnd  11943  cos2bnd  11944  sinltxirr  11945  sin01gt0  11946  cos01gt0  11947  sin02gt0  11948  sincos1sgn  11949  cos12dec  11952  ene1  11969  eap1  11970  3dvds  12048  halfleoddlt  12078  flodddiv4  12120  isprm3  12313  sqnprm  12331  coprm  12339  phibndlem  12411  pythagtriplem3  12463  fldivp1  12544  pockthi  12554  exmidunben  12670  basendxnmulrndx  12838  starvndxnbasendx  12846  scandxnbasendx  12858  vscandxnbasendx  12863  ipndxnbasendx  12876  basendxnocndx  12917  setsmsbasg  14823  tgioo  14898  dveflem  15070  reeff1olem  15115  reeff1o  15117  cosz12  15124  sinhalfpilem  15135  tangtx  15182  sincos4thpi  15184  pigt3  15188  coskpi  15192  cos0pilt1  15196  ioocosf1o  15198  loge  15211  logrpap0b  15220  logdivlti  15225  2logb9irrALT  15318  sqrt2cxp2logb9e3  15319  perfectlem2  15344  lgsdir  15384  lgsne0  15387  lgsabs1  15388  lgsdinn0  15397  gausslemma2dlem0i  15406  lgseisen  15423  2lgslem3  15450  ex-fl  15479  cvgcmp2nlemabs  15789  iooref1o  15791  trilpolemclim  15793  trilpolemcl  15794  trilpolemisumle  15795  trilpolemeq1  15797  trilpolemlt1  15798  apdiff  15805  nconstwlpolemgt0  15821