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  11146  re1  11150  im1  11151  rei  11152  imi  11153  caucvgre  11234  sqrt1  11299  sqrt2gt1lt2  11302  abs1  11325  caubnd2  11370  mulcn2  11565  reccn2ap  11566  expcnvap0  11755  geo2sum  11767  cvgratnnlemrate  11783  fprodge0  11890  fprodge1  11892  fprodle  11893  ere  11923  ege2le3  11924  efgt1  11950  resin4p  11971  recos4p  11972  sinbnd  12005  cosbnd  12006  sinbnd2  12007  cosbnd2  12008  ef01bndlem  12009  sin01bnd  12010  cos01bnd  12011  cos1bnd  12012  cos2bnd  12013  sinltxirr  12014  sin01gt0  12015  cos01gt0  12016  sin02gt0  12017  sincos1sgn  12018  cos12dec  12021  ene1  12038  eap1  12039  3dvds  12117  halfleoddlt  12147  flodddiv4  12189  isprm3  12382  sqnprm  12400  coprm  12408  phibndlem  12480  pythagtriplem3  12532  fldivp1  12613  pockthi  12623  exmidunben  12739  basendxnmulrndx  12908  starvndxnbasendx  12916  scandxnbasendx  12928  vscandxnbasendx  12933  ipndxnbasendx  12946  basendxnocndx  12987  setsmsbasg  14893  tgioo  14968  dveflem  15140  reeff1olem  15185  reeff1o  15187  cosz12  15194  sinhalfpilem  15205  tangtx  15252  sincos4thpi  15254  pigt3  15258  coskpi  15262  cos0pilt1  15266  ioocosf1o  15268  loge  15281  logrpap0b  15290  logdivlti  15295  2logb9irrALT  15388  sqrt2cxp2logb9e3  15389  perfectlem2  15414  lgsdir  15454  lgsne0  15457  lgsabs1  15458  lgsdinn0  15467  gausslemma2dlem0i  15476  lgseisen  15493  2lgslem3  15520  ex-fl  15594  cvgcmp2nlemabs  15904  iooref1o  15906  trilpolemclim  15908  trilpolemcl  15909  trilpolemisumle  15910  trilpolemeq1  15912  trilpolemlt1  15913  apdiff  15920  nconstwlpolemgt0  15936