Theorem 1re 8178

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

Syntax hints:   ∈ wcel 2202  ℝcr 8031  1c1 8033

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

This theorem is referenced by:  0re  8179  1red  8194  1xr  8238  0lt1  8306  peano2re  8315  peano2rem  8446  0reALT  8476  0le1  8661  1le1  8752  inelr  8764  1ap0  8770  eqneg  8912  ltp1  9024  ltm1  9026  recgt0  9030  mulgt1  9043  ltmulgt11  9044  lemulge11  9046  reclt1  9076  recgt1  9077  recgt1i  9078  recp1lt1  9079  recreclt  9080  sup3exmid  9137  cju  9141  peano5nni  9146  nnssre  9147  1nn  9154  nnge1  9166  nnle1eq1  9167  nngt0  9168  nnnlt1  9169  nn1gt1  9177  nngt1ne1  9178  nnrecre  9180  nnrecgt0  9181  nnsub  9182  2re  9213  3re  9217  4re  9220  5re  9222  6re  9224  7re  9226  8re  9228  9re  9230  0le2  9233  2pos  9234  3pos  9237  4pos  9240  5pos  9243  6pos  9244  7pos  9245  8pos  9246  9pos  9247  neg1rr  9249  neg1lt0  9251  1lt2  9313  1lt3  9315  1lt4  9318  1lt5  9322  1lt6  9327  1lt7  9333  1lt8  9340  1lt9  9348  1ne2  9350  1ap2  9351  1le2  9352  1le3  9355  halflt1  9361  iap0  9367  addltmul  9381  elnnnn0c  9447  nn0ge2m1nn  9462  elnnz1  9502  zltp1le  9534  zleltp1  9535  recnz  9573  gtndiv  9575  3halfnz  9577  1lt10  9749  eluzp1m1  9780  eluzp1p1  9782  eluz2b2  9837  1rp  9892  divlt1lt  9959  divle1le  9960  nnledivrp  10001  0elunit  10221  1elunit  10222  divelunit  10237  lincmb01cmp  10238  iccf1o  10239  unitssre  10240  fzpreddisj  10306  fznatpl1  10311  fztpval  10318  qbtwnxr  10518  flqbi2  10552  fldiv4p1lem1div2  10566  flqdiv  10584  seqf1oglem1  10782  reexpcl  10819  reexpclzap  10822  expge0  10838  expge1  10839  expgt1  10840  bernneq  10923  bernneq2  10924  expnbnd  10926  expnlbnd  10927  expnlbnd2  10928  nn0ltexp2  10972  facwordi  11003  faclbnd3  11006  faclbnd6  11007  facavg  11009  hashtpglem  11111  lsw0  11165  cjexp  11458  re1  11462  im1  11463  rei  11464  imi  11465  caucvgre  11546  sqrt1  11611  sqrt2gt1lt2  11614  abs1  11637  caubnd2  11682  mulcn2  11877  reccn2ap  11878  expcnvap0  12068  geo2sum  12080  cvgratnnlemrate  12096  fprodge0  12203  fprodge1  12205  fprodle  12206  ere  12236  ege2le3  12237  efgt1  12263  resin4p  12284  recos4p  12285  sinbnd  12318  cosbnd  12319  sinbnd2  12320  cosbnd2  12321  ef01bndlem  12322  sin01bnd  12323  cos01bnd  12324  cos1bnd  12325  cos2bnd  12326  sinltxirr  12327  sin01gt0  12328  cos01gt0  12329  sin02gt0  12330  sincos1sgn  12331  cos12dec  12334  ene1  12351  eap1  12352  3dvds  12430  halfleoddlt  12460  flodddiv4  12502  isprm3  12695  sqnprm  12713  coprm  12721  phibndlem  12793  pythagtriplem3  12845  fldivp1  12926  pockthi  12936  exmidunben  13052  basendxnmulrndx  13222  starvndxnbasendx  13230  scandxnbasendx  13242  vscandxnbasendx  13247  ipndxnbasendx  13260  basendxnocndx  13301  setsmsbasg  15209  tgioo  15284  dveflem  15456  reeff1olem  15501  reeff1o  15503  cosz12  15510  sinhalfpilem  15521  tangtx  15568  sincos4thpi  15570  pigt3  15574  coskpi  15578  cos0pilt1  15582  ioocosf1o  15584  loge  15597  logrpap0b  15606  logdivlti  15611  2logb9irrALT  15704  sqrt2cxp2logb9e3  15705  perfectlem2  15730  lgsdir  15770  lgsne0  15773  lgsabs1  15774  lgsdinn0  15783  gausslemma2dlem0i  15792  lgseisen  15809  2lgslem3  15836  usgrexmpldifpr  16106  ex-fl  16343  cvgcmp2nlemabs  16662  iooref1o  16664  trilpolemclim  16666  trilpolemcl  16667  trilpolemisumle  16668  trilpolemeq1  16670  trilpolemlt1  16671  apdiff  16678  nconstwlpolemgt0  16695