Theorem 1re 8221

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

Syntax hints:   ∈ wcel 2202  ℝcr 8074  1c1 8076

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

This theorem is referenced by:  0re  8222  1red  8237  1xr  8280  0lt1  8348  peano2re  8357  peano2rem  8488  0reALT  8518  0le1  8703  1le1  8794  inelr  8806  1ap0  8812  eqneg  8954  ltp1  9066  ltm1  9068  recgt0  9072  mulgt1  9085  ltmulgt11  9086  lemulge11  9088  reclt1  9118  recgt1  9119  recgt1i  9120  recp1lt1  9121  recreclt  9122  sup3exmid  9179  cju  9183  peano5nni  9188  nnssre  9189  1nn  9196  nnge1  9208  nnle1eq1  9209  nngt0  9210  nnnlt1  9211  nn1gt1  9219  nngt1ne1  9220  nnrecre  9222  nnrecgt0  9223  nnsub  9224  2re  9255  3re  9259  4re  9262  5re  9264  6re  9266  7re  9268  8re  9270  9re  9272  0le2  9275  2pos  9276  3pos  9279  4pos  9282  5pos  9285  6pos  9286  7pos  9287  8pos  9288  9pos  9289  neg1rr  9291  neg1lt0  9293  1lt2  9355  1lt3  9357  1lt4  9360  1lt5  9364  1lt6  9369  1lt7  9375  1lt8  9382  1lt9  9390  1ne2  9392  1ap2  9393  1le2  9394  1le3  9397  halflt1  9403  iap0  9409  addltmul  9423  elnnnn0c  9489  nn0ge2m1nn  9506  elnnz1  9546  zltp1le  9578  zleltp1  9579  recnz  9617  gtndiv  9619  3halfnz  9621  1lt10  9793  eluzp1m1  9824  eluzp1p1  9826  eluz2b2  9881  1rp  9936  divlt1lt  10003  divle1le  10004  nnledivrp  10045  0elunit  10265  1elunit  10266  divelunit  10281  lincmb01cmp  10282  lincmble  10283  iccf1o  10284  unitssre  10285  fzpreddisj  10351  fznatpl1  10356  fztpval  10363  qbtwnxr  10563  flqbi2  10597  fldiv4p1lem1div2  10611  flqdiv  10629  seqf1oglem1  10827  reexpcl  10864  reexpclzap  10867  expge0  10883  expge1  10884  expgt1  10885  bernneq  10968  bernneq2  10969  expnbnd  10971  expnlbnd  10972  expnlbnd2  10973  nn0ltexp2  11017  facwordi  11048  faclbnd3  11051  faclbnd6  11052  facavg  11054  hashtpglem  11156  lsw0  11210  cjexp  11516  re1  11520  im1  11521  rei  11522  imi  11523  caucvgre  11604  sqrt1  11669  sqrt2gt1lt2  11672  abs1  11695  caubnd2  11740  mulcn2  11935  reccn2ap  11936  expcnvap0  12126  geo2sum  12138  cvgratnnlemrate  12154  fprodge0  12261  fprodge1  12263  fprodle  12264  ere  12294  ege2le3  12295  efgt1  12321  resin4p  12342  recos4p  12343  sinbnd  12376  cosbnd  12377  sinbnd2  12378  cosbnd2  12379  ef01bndlem  12380  sin01bnd  12381  cos01bnd  12382  cos1bnd  12383  cos2bnd  12384  sinltxirr  12385  sin01gt0  12386  cos01gt0  12387  sin02gt0  12388  sincos1sgn  12389  cos12dec  12392  ene1  12409  eap1  12410  3dvds  12488  halfleoddlt  12518  flodddiv4  12560  isprm3  12753  sqnprm  12771  coprm  12779  phibndlem  12851  pythagtriplem3  12903  fldivp1  12984  pockthi  12994  exmidunben  13110  basendxnmulrndx  13280  starvndxnbasendx  13288  scandxnbasendx  13300  vscandxnbasendx  13305  ipndxnbasendx  13318  basendxnocndx  13359  setsmsbasg  15273  tgioo  15348  dveflem  15520  reeff1olem  15565  reeff1o  15567  cosz12  15574  sinhalfpilem  15585  tangtx  15632  sincos4thpi  15634  pigt3  15638  coskpi  15642  cos0pilt1  15646  ioocosf1o  15648  loge  15661  logrpap0b  15670  logdivlti  15675  2logb9irrALT  15768  sqrt2cxp2logb9e3  15769  perfectlem2  15797  lgsdir  15837  lgsne0  15840  lgsabs1  15841  lgsdinn0  15850  gausslemma2dlem0i  15859  lgseisen  15876  2lgslem3  15903  usgrexmpldifpr  16173  konigsberglem2  16413  konigsberglem3  16414  konigsberglem5  16416  ex-fl  16422  cvgcmp2nlemabs  16747  iooref1o  16749  trilpolemclim  16751  trilpolemcl  16752  trilpolemisumle  16753  trilpolemeq1  16755  trilpolemlt1  16756  apdiff  16763  nconstwlpolemgt0  16780