Theorem 1re 7637

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

Syntax hints:   ∈ wcel 1448  ℝcr 7499  1c1 7501

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

This theorem is referenced by:  0re  7638  1red  7653  0lt1  7760  peano2re  7769  peano2rem  7900  0reALT  7930  0le1  8110  1le1  8200  inelr  8212  1ap0  8218  eqneg  8353  ltp1  8460  ltm1  8462  recgt0  8466  mulgt1  8479  ltmulgt11  8480  lemulge11  8482  reclt1  8512  recgt1  8513  recgt1i  8514  recp1lt1  8515  recreclt  8516  sup3exmid  8573  cju  8577  peano5nni  8581  nnssre  8582  1nn  8589  nnge1  8601  nnle1eq1  8602  nngt0  8603  nnnlt1  8604  nn1gt1  8612  nngt1ne1  8613  nnrecre  8615  nnrecgt0  8616  nnsub  8617  2re  8648  3re  8652  4re  8655  5re  8657  6re  8659  7re  8661  8re  8663  9re  8665  0le2  8668  2pos  8669  3pos  8672  4pos  8675  5pos  8678  6pos  8679  7pos  8680  8pos  8681  9pos  8682  neg1rr  8684  neg1lt0  8686  1lt2  8741  1lt3  8743  1lt4  8746  1lt5  8750  1lt6  8755  1lt7  8761  1lt8  8768  1lt9  8776  1ne2  8778  1ap2  8779  1le2  8780  1le3  8783  halflt1  8789  iap0  8795  addltmul  8808  elnnnn0c  8874  nn0ge2m1nn  8889  elnnz1  8929  zltp1le  8960  zleltp1  8961  recnz  8996  gtndiv  8998  3halfnz  9000  1lt10  9172  eluzp1m1  9199  eluzp1p1  9201  eluz2b2  9247  1rp  9295  divlt1lt  9358  divle1le  9359  nnledivrp  9394  0elunit  9610  1elunit  9611  divelunit  9626  lincmb01cmp  9627  iccf1o  9628  unitssre  9629  fzpreddisj  9692  fznatpl1  9697  fztpval  9704  qbtwnxr  9876  flqbi2  9905  fldiv4p1lem1div2  9919  flqdiv  9935  reexpcl  10151  reexpclzap  10154  expge0  10170  expge1  10171  expgt1  10172  bernneq  10253  bernneq2  10254  expnbnd  10256  expnlbnd  10257  expnlbnd2  10258  facwordi  10327  faclbnd3  10330  faclbnd6  10331  facavg  10333  cjexp  10506  re1  10510  im1  10511  rei  10512  imi  10513  caucvgre  10593  sqrt1  10658  sqrt2gt1lt2  10661  abs1  10684  caubnd2  10729  mulcn2  10920  reccn2ap  10921  expcnvap0  11110  geo2sum  11122  cvgratnnlemrate  11138  ere  11174  ege2le3  11175  efgt1  11201  resin4p  11223  recos4p  11224  sinbnd  11257  cosbnd  11258  sinbnd2  11259  cosbnd2  11260  ef01bndlem  11261  sin01bnd  11262  cos01bnd  11263  cos1bnd  11264  cos2bnd  11265  sin01gt0  11266  cos01gt0  11267  sin02gt0  11268  sincos1sgn  11269  ene1  11286  eap1  11287  halfleoddlt  11386  flodddiv4  11426  isprm3  11592  sqnprm  11609  coprm  11615  phibndlem  11684  exmidunben  11731  basendxnmulrndx  11855  setsmsbasg  12407  tgioo  12465  ex-fl  12540  cvgcmp2nlemabs  12811  trilpolemclim  12813  trilpolemcl  12814  trilpolemisumle  12815  trilpolemeq1  12817  trilpolemlt1  12818