Theorem 1re 8141

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

Syntax hints:   ∈ wcel 2200  ℝcr 7994  1c1 7996

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

This theorem is referenced by:  0re  8142  1red  8157  1xr  8201  0lt1  8269  peano2re  8278  peano2rem  8409  0reALT  8439  0le1  8624  1le1  8715  inelr  8727  1ap0  8733  eqneg  8875  ltp1  8987  ltm1  8989  recgt0  8993  mulgt1  9006  ltmulgt11  9007  lemulge11  9009  reclt1  9039  recgt1  9040  recgt1i  9041  recp1lt1  9042  recreclt  9043  sup3exmid  9100  cju  9104  peano5nni  9109  nnssre  9110  1nn  9117  nnge1  9129  nnle1eq1  9130  nngt0  9131  nnnlt1  9132  nn1gt1  9140  nngt1ne1  9141  nnrecre  9143  nnrecgt0  9144  nnsub  9145  2re  9176  3re  9180  4re  9183  5re  9185  6re  9187  7re  9189  8re  9191  9re  9193  0le2  9196  2pos  9197  3pos  9200  4pos  9203  5pos  9206  6pos  9207  7pos  9208  8pos  9209  9pos  9210  neg1rr  9212  neg1lt0  9214  1lt2  9276  1lt3  9278  1lt4  9281  1lt5  9285  1lt6  9290  1lt7  9296  1lt8  9303  1lt9  9311  1ne2  9313  1ap2  9314  1le2  9315  1le3  9318  halflt1  9324  iap0  9330  addltmul  9344  elnnnn0c  9410  nn0ge2m1nn  9425  elnnz1  9465  zltp1le  9497  zleltp1  9498  recnz  9536  gtndiv  9538  3halfnz  9540  1lt10  9712  eluzp1m1  9742  eluzp1p1  9744  eluz2b2  9794  1rp  9849  divlt1lt  9916  divle1le  9917  nnledivrp  9958  0elunit  10178  1elunit  10179  divelunit  10194  lincmb01cmp  10195  iccf1o  10196  unitssre  10197  fzpreddisj  10263  fznatpl1  10268  fztpval  10275  qbtwnxr  10472  flqbi2  10506  fldiv4p1lem1div2  10520  flqdiv  10538  seqf1oglem1  10736  reexpcl  10773  reexpclzap  10776  expge0  10792  expge1  10793  expgt1  10794  bernneq  10877  bernneq2  10878  expnbnd  10880  expnlbnd  10881  expnlbnd2  10882  nn0ltexp2  10926  facwordi  10957  faclbnd3  10960  faclbnd6  10961  facavg  10963  lsw0  11114  cjexp  11399  re1  11403  im1  11404  rei  11405  imi  11406  caucvgre  11487  sqrt1  11552  sqrt2gt1lt2  11555  abs1  11578  caubnd2  11623  mulcn2  11818  reccn2ap  11819  expcnvap0  12008  geo2sum  12020  cvgratnnlemrate  12036  fprodge0  12143  fprodge1  12145  fprodle  12146  ere  12176  ege2le3  12177  efgt1  12203  resin4p  12224  recos4p  12225  sinbnd  12258  cosbnd  12259  sinbnd2  12260  cosbnd2  12261  ef01bndlem  12262  sin01bnd  12263  cos01bnd  12264  cos1bnd  12265  cos2bnd  12266  sinltxirr  12267  sin01gt0  12268  cos01gt0  12269  sin02gt0  12270  sincos1sgn  12271  cos12dec  12274  ene1  12291  eap1  12292  3dvds  12370  halfleoddlt  12400  flodddiv4  12442  isprm3  12635  sqnprm  12653  coprm  12661  phibndlem  12733  pythagtriplem3  12785  fldivp1  12866  pockthi  12876  exmidunben  12992  basendxnmulrndx  13162  starvndxnbasendx  13170  scandxnbasendx  13182  vscandxnbasendx  13187  ipndxnbasendx  13200  basendxnocndx  13241  setsmsbasg  15147  tgioo  15222  dveflem  15394  reeff1olem  15439  reeff1o  15441  cosz12  15448  sinhalfpilem  15459  tangtx  15506  sincos4thpi  15508  pigt3  15512  coskpi  15516  cos0pilt1  15520  ioocosf1o  15522  loge  15535  logrpap0b  15544  logdivlti  15549  2logb9irrALT  15642  sqrt2cxp2logb9e3  15643  perfectlem2  15668  lgsdir  15708  lgsne0  15711  lgsabs1  15712  lgsdinn0  15721  gausslemma2dlem0i  15730  lgseisen  15747  2lgslem3  15774  ex-fl  16047  cvgcmp2nlemabs  16359  iooref1o  16361  trilpolemclim  16363  trilpolemcl  16364  trilpolemisumle  16365  trilpolemeq1  16367  trilpolemlt1  16368  apdiff  16375  nconstwlpolemgt0  16391