Theorem 1re 7026

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

Syntax hints:   ∈ wcel 1393  ℝcr 6888  1c1 6890

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

This theorem is referenced by:  0re  7027  1red  7042  0lt1  7141  peano2re  7149  peano2rem  7278  0reALT  7308  0le1  7476  1le1  7563  inelr  7575  1ap0  7581  eqneg  7708  ltp1  7810  ltm1  7812  recgt0  7816  mulgt1  7829  ltmulgt11  7830  lemulge11  7832  reclt1  7862  recgt1  7863  recgt1i  7864  recp1lt1  7865  recreclt  7866  cju  7913  peano5nni  7917  nnssre  7918  1nn  7925  nnge1  7937  nnle1eq1  7938  nngt0  7939  nnnlt1  7940  nn1gt1  7947  nngt1ne1  7948  nnrecre  7950  nnrecgt0  7951  nnsub  7952  2re  7985  3re  7989  4re  7992  5re  7994  6re  7996  7re  7998  8re  8000  9re  8002  10re  8004  0le2  8006  2pos  8007  3pos  8010  4pos  8013  5pos  8016  6pos  8017  7pos  8018  8pos  8019  9pos  8020  10pos  8021  neg1rr  8023  neg1lt0  8025  1lt2  8086  1lt3  8088  1lt4  8091  1lt5  8095  1lt6  8100  1lt7  8106  1lt8  8113  1lt9  8121  1lt10  8130  1ne2  8132  1le2  8133  1le3  8136  halflt1  8142  iap0  8148  addltmul  8161  elnnnn0c  8227  nn0ge2m1nn  8242  elnnz1  8268  zltp1le  8298  zleltp1  8299  recnz  8333  gtndiv  8335  eluzp1m1  8496  eluzp1p1  8498  eluz2b2  8540  1rp  8587  divlt1lt  8650  divle1le  8651  0elunit  8854  1elunit  8855  divelunit  8870  lincmb01cmp  8871  iccf1o  8872  unitssre  8873  fzpreddisj  8933  fznatpl1  8938  fztpval  8945  flqbi2  9133  fldiv4p1lem1div2  9147  flqdiv  9163  reexpcl  9272  reexpclzap  9275  expge0  9291  expge1  9292  expgt1  9293  bernneq  9369  bernneq2  9370  expnbnd  9372  expnlbnd  9373  expnlbnd2  9374  cjexp  9493  re1  9497  im1  9498  rei  9499  imi  9500  caucvgre  9580  sqrt1  9644  sqrt2gt1lt2  9647  abs1  9670  caubnd2  9713  mulcn2  9833  ex-fl  9895