Theorem 1re 8273

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

Syntax hints:   ∈ wcel 2203  ℝcr 8126  1c1 8128

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

This theorem is referenced by:  0re  8274  1red  8289  1xr  8332  0lt1  8400  peano2re  8409  peano2rem  8540  0reALT  8570  0le1  8755  1le1  8846  inelr  8858  1ap0  8864  eqneg  9006  ltp1  9118  ltm1  9120  recgt0  9124  mulgt1  9137  ltmulgt11  9138  lemulge11  9140  reclt1  9170  recgt1  9171  recgt1i  9172  recp1lt1  9173  recreclt  9174  sup3exmid  9231  cju  9235  peano5nni  9240  nnssre  9241  1nn  9248  nnge1  9260  nnle1eq1  9261  nngt0  9262  nnnlt1  9263  nn1gt1  9271  nngt1ne1  9272  nnrecre  9274  nnrecgt0  9275  nnsub  9276  2re  9307  3re  9311  4re  9314  5re  9316  6re  9318  7re  9320  8re  9322  9re  9324  0le2  9327  2pos  9328  3pos  9331  4pos  9334  5pos  9337  6pos  9338  7pos  9339  8pos  9340  9pos  9341  neg1rr  9343  neg1lt0  9345  1lt2  9407  1lt3  9409  1lt4  9412  1lt5  9416  1lt6  9421  1lt7  9427  1lt8  9434  1lt9  9442  1ne2  9444  1ap2  9445  1le2  9446  1le3  9449  halflt1  9455  iap0  9461  addltmul  9475  elnnnn0c  9541  nn0ge2m1nn  9560  elnnz1  9600  zltp1le  9632  zleltp1  9633  recnz  9671  gtndiv  9673  3halfnz  9675  1lt10  9847  eluzp1m1  9878  eluzp1p1  9880  eluz2b2  9935  1rp  9990  divlt1lt  10057  divle1le  10058  nnledivrp  10099  0elunit  10319  1elunit  10320  divelunit  10335  lincmb01cmp  10336  lincmble  10337  iccf1o  10338  unitssre  10339  fzpreddisj  10405  fznatpl1  10410  fztpval  10417  qbtwnxr  10617  flqbi2  10651  fldiv4p1lem1div2  10665  flqdiv  10683  seqf1oglem1  10881  reexpcl  10918  reexpclzap  10921  expge0  10937  expge1  10938  expgt1  10939  bernneq  11022  bernneq2  11023  expnbnd  11025  expnlbnd  11026  expnlbnd2  11027  nn0ltexp2  11071  facwordi  11102  faclbnd3  11105  faclbnd6  11106  facavg  11108  hashtpglem  11218  lsw0  11272  cjexp  11578  re1  11582  im1  11583  rei  11584  imi  11585  caucvgre  11666  sqrt1  11731  sqrt2gt1lt2  11734  abs1  11757  caubnd2  11802  mulcn2  11997  reccn2ap  11998  expcnvap0  12188  geo2sum  12200  cvgratnnlemrate  12216  fprodge0  12323  fprodge1  12325  fprodle  12326  ere  12356  ege2le3  12357  efgt1  12383  resin4p  12404  recos4p  12405  sinbnd  12438  cosbnd  12439  sinbnd2  12440  cosbnd2  12441  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  cos1bnd  12445  cos2bnd  12446  sinltxirr  12447  sin01gt0  12448  cos01gt0  12449  sin02gt0  12450  sincos1sgn  12451  cos12dec  12454  ene1  12471  eap1  12472  3dvds  12550  halfleoddlt  12580  flodddiv4  12622  isprm3  12815  sqnprm  12833  coprm  12841  phibndlem  12913  pythagtriplem3  12965  fldivp1  13046  pockthi  13056  ballotfilem2  13142  exmidunben  13177  basendxnmulrndx  13347  starvndxnbasendx  13355  scandxnbasendx  13367  vscandxnbasendx  13372  ipndxnbasendx  13385  basendxnocndx  13426  setsmsbasg  15344  tgioo  15419  dveflem  15591  reeff1olem  15636  reeff1o  15638  cosz12  15645  sinhalfpilem  15656  tangtx  15703  sincos4thpi  15705  pigt3  15709  coskpi  15713  cos0pilt1  15717  ioocosf1o  15719  loge  15732  logrpap0b  15741  logdivlti  15746  2logb9irrALT  15839  sqrt2cxp2logb9e3  15840  perfectlem2  15868  lgsdir  15908  lgsne0  15911  lgsabs1  15912  lgsdinn0  15921  gausslemma2dlem0i  15930  lgseisen  15947  2lgslem3  15974  usgrexmpldifpr  16244  konigsberglem2  16484  konigsberglem3  16485  konigsberglem5  16487  ex-fl  16493  cvgcmp2nlemabs  16816  iooref1o  16818  trilpolemclim  16820  trilpolemcl  16821  trilpolemisumle  16822  trilpolemeq1  16824  trilpolemlt1  16825  apdiff  16832  nconstwlpolemgt0  16850