Theorem 1re 8177

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

Syntax hints:   ∈ wcel 2202  ℝcr 8030  1c1 8032

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

This theorem is referenced by:  0re  8178  1red  8193  1xr  8237  0lt1  8305  peano2re  8314  peano2rem  8445  0reALT  8475  0le1  8660  1le1  8751  inelr  8763  1ap0  8769  eqneg  8911  ltp1  9023  ltm1  9025  recgt0  9029  mulgt1  9042  ltmulgt11  9043  lemulge11  9045  reclt1  9075  recgt1  9076  recgt1i  9077  recp1lt1  9078  recreclt  9079  sup3exmid  9136  cju  9140  peano5nni  9145  nnssre  9146  1nn  9153  nnge1  9165  nnle1eq1  9166  nngt0  9167  nnnlt1  9168  nn1gt1  9176  nngt1ne1  9177  nnrecre  9179  nnrecgt0  9180  nnsub  9181  2re  9212  3re  9216  4re  9219  5re  9221  6re  9223  7re  9225  8re  9227  9re  9229  0le2  9232  2pos  9233  3pos  9236  4pos  9239  5pos  9242  6pos  9243  7pos  9244  8pos  9245  9pos  9246  neg1rr  9248  neg1lt0  9250  1lt2  9312  1lt3  9314  1lt4  9317  1lt5  9321  1lt6  9326  1lt7  9332  1lt8  9339  1lt9  9347  1ne2  9349  1ap2  9350  1le2  9351  1le3  9354  halflt1  9360  iap0  9366  addltmul  9380  elnnnn0c  9446  nn0ge2m1nn  9461  elnnz1  9501  zltp1le  9533  zleltp1  9534  recnz  9572  gtndiv  9574  3halfnz  9576  1lt10  9748  eluzp1m1  9779  eluzp1p1  9781  eluz2b2  9836  1rp  9891  divlt1lt  9958  divle1le  9959  nnledivrp  10000  0elunit  10220  1elunit  10221  divelunit  10236  lincmb01cmp  10237  iccf1o  10238  unitssre  10239  fzpreddisj  10305  fznatpl1  10310  fztpval  10317  qbtwnxr  10516  flqbi2  10550  fldiv4p1lem1div2  10564  flqdiv  10582  seqf1oglem1  10780  reexpcl  10817  reexpclzap  10820  expge0  10836  expge1  10837  expgt1  10838  bernneq  10921  bernneq2  10922  expnbnd  10924  expnlbnd  10925  expnlbnd2  10926  nn0ltexp2  10970  facwordi  11001  faclbnd3  11004  faclbnd6  11005  facavg  11007  lsw0  11160  cjexp  11453  re1  11457  im1  11458  rei  11459  imi  11460  caucvgre  11541  sqrt1  11606  sqrt2gt1lt2  11609  abs1  11632  caubnd2  11677  mulcn2  11872  reccn2ap  11873  expcnvap0  12062  geo2sum  12074  cvgratnnlemrate  12090  fprodge0  12197  fprodge1  12199  fprodle  12200  ere  12230  ege2le3  12231  efgt1  12257  resin4p  12278  recos4p  12279  sinbnd  12312  cosbnd  12313  sinbnd2  12314  cosbnd2  12315  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  cos1bnd  12319  cos2bnd  12320  sinltxirr  12321  sin01gt0  12322  cos01gt0  12323  sin02gt0  12324  sincos1sgn  12325  cos12dec  12328  ene1  12345  eap1  12346  3dvds  12424  halfleoddlt  12454  flodddiv4  12496  isprm3  12689  sqnprm  12707  coprm  12715  phibndlem  12787  pythagtriplem3  12839  fldivp1  12920  pockthi  12930  exmidunben  13046  basendxnmulrndx  13216  starvndxnbasendx  13224  scandxnbasendx  13236  vscandxnbasendx  13241  ipndxnbasendx  13254  basendxnocndx  13295  setsmsbasg  15202  tgioo  15277  dveflem  15449  reeff1olem  15494  reeff1o  15496  cosz12  15503  sinhalfpilem  15514  tangtx  15561  sincos4thpi  15563  pigt3  15567  coskpi  15571  cos0pilt1  15575  ioocosf1o  15577  loge  15590  logrpap0b  15599  logdivlti  15604  2logb9irrALT  15697  sqrt2cxp2logb9e3  15698  perfectlem2  15723  lgsdir  15763  lgsne0  15766  lgsabs1  15767  lgsdinn0  15776  gausslemma2dlem0i  15785  lgseisen  15802  2lgslem3  15829  usgrexmpldifpr  16099  ex-fl  16321  cvgcmp2nlemabs  16636  iooref1o  16638  trilpolemclim  16640  trilpolemcl  16641  trilpolemisumle  16642  trilpolemeq1  16644  trilpolemlt1  16645  apdiff  16652  nconstwlpolemgt0  16668