Theorem 1re 8070

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

Syntax hints:   ∈ wcel 2175  ℝcr 7923  1c1 7925

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

This theorem is referenced by:  0re  8071  1red  8086  1xr  8130  0lt1  8198  peano2re  8207  peano2rem  8338  0reALT  8368  0le1  8553  1le1  8644  inelr  8656  1ap0  8662  eqneg  8804  ltp1  8916  ltm1  8918  recgt0  8922  mulgt1  8935  ltmulgt11  8936  lemulge11  8938  reclt1  8968  recgt1  8969  recgt1i  8970  recp1lt1  8971  recreclt  8972  sup3exmid  9029  cju  9033  peano5nni  9038  nnssre  9039  1nn  9046  nnge1  9058  nnle1eq1  9059  nngt0  9060  nnnlt1  9061  nn1gt1  9069  nngt1ne1  9070  nnrecre  9072  nnrecgt0  9073  nnsub  9074  2re  9105  3re  9109  4re  9112  5re  9114  6re  9116  7re  9118  8re  9120  9re  9122  0le2  9125  2pos  9126  3pos  9129  4pos  9132  5pos  9135  6pos  9136  7pos  9137  8pos  9138  9pos  9139  neg1rr  9141  neg1lt0  9143  1lt2  9205  1lt3  9207  1lt4  9210  1lt5  9214  1lt6  9219  1lt7  9225  1lt8  9232  1lt9  9240  1ne2  9242  1ap2  9243  1le2  9244  1le3  9247  halflt1  9253  iap0  9259  addltmul  9273  elnnnn0c  9339  nn0ge2m1nn  9354  elnnz1  9394  zltp1le  9426  zleltp1  9427  recnz  9465  gtndiv  9467  3halfnz  9469  1lt10  9641  eluzp1m1  9671  eluzp1p1  9673  eluz2b2  9723  1rp  9778  divlt1lt  9845  divle1le  9846  nnledivrp  9887  0elunit  10107  1elunit  10108  divelunit  10123  lincmb01cmp  10124  iccf1o  10125  unitssre  10126  fzpreddisj  10192  fznatpl1  10197  fztpval  10204  qbtwnxr  10398  flqbi2  10432  fldiv4p1lem1div2  10446  flqdiv  10464  seqf1oglem1  10662  reexpcl  10699  reexpclzap  10702  expge0  10718  expge1  10719  expgt1  10720  bernneq  10803  bernneq2  10804  expnbnd  10806  expnlbnd  10807  expnlbnd2  10808  nn0ltexp2  10852  facwordi  10883  faclbnd3  10886  faclbnd6  10887  facavg  10889  lsw0  11039  cjexp  11175  re1  11179  im1  11180  rei  11181  imi  11182  caucvgre  11263  sqrt1  11328  sqrt2gt1lt2  11331  abs1  11354  caubnd2  11399  mulcn2  11594  reccn2ap  11595  expcnvap0  11784  geo2sum  11796  cvgratnnlemrate  11812  fprodge0  11919  fprodge1  11921  fprodle  11922  ere  11952  ege2le3  11953  efgt1  11979  resin4p  12000  recos4p  12001  sinbnd  12034  cosbnd  12035  sinbnd2  12036  cosbnd2  12037  ef01bndlem  12038  sin01bnd  12039  cos01bnd  12040  cos1bnd  12041  cos2bnd  12042  sinltxirr  12043  sin01gt0  12044  cos01gt0  12045  sin02gt0  12046  sincos1sgn  12047  cos12dec  12050  ene1  12067  eap1  12068  3dvds  12146  halfleoddlt  12176  flodddiv4  12218  isprm3  12411  sqnprm  12429  coprm  12437  phibndlem  12509  pythagtriplem3  12561  fldivp1  12642  pockthi  12652  exmidunben  12768  basendxnmulrndx  12937  starvndxnbasendx  12945  scandxnbasendx  12957  vscandxnbasendx  12962  ipndxnbasendx  12975  basendxnocndx  13016  setsmsbasg  14922  tgioo  14997  dveflem  15169  reeff1olem  15214  reeff1o  15216  cosz12  15223  sinhalfpilem  15234  tangtx  15281  sincos4thpi  15283  pigt3  15287  coskpi  15291  cos0pilt1  15295  ioocosf1o  15297  loge  15310  logrpap0b  15319  logdivlti  15324  2logb9irrALT  15417  sqrt2cxp2logb9e3  15418  perfectlem2  15443  lgsdir  15483  lgsne0  15486  lgsabs1  15487  lgsdinn0  15496  gausslemma2dlem0i  15505  lgseisen  15522  2lgslem3  15549  ex-fl  15623  cvgcmp2nlemabs  15933  iooref1o  15935  trilpolemclim  15937  trilpolemcl  15938  trilpolemisumle  15939  trilpolemeq1  15941  trilpolemlt1  15942  apdiff  15949  nconstwlpolemgt0  15965