Theorem 1re 8101

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

Syntax hints:   ∈ wcel 2177  ℝcr 7954  1c1 7956

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

This theorem is referenced by:  0re  8102  1red  8117  1xr  8161  0lt1  8229  peano2re  8238  peano2rem  8369  0reALT  8399  0le1  8584  1le1  8675  inelr  8687  1ap0  8693  eqneg  8835  ltp1  8947  ltm1  8949  recgt0  8953  mulgt1  8966  ltmulgt11  8967  lemulge11  8969  reclt1  8999  recgt1  9000  recgt1i  9001  recp1lt1  9002  recreclt  9003  sup3exmid  9060  cju  9064  peano5nni  9069  nnssre  9070  1nn  9077  nnge1  9089  nnle1eq1  9090  nngt0  9091  nnnlt1  9092  nn1gt1  9100  nngt1ne1  9101  nnrecre  9103  nnrecgt0  9104  nnsub  9105  2re  9136  3re  9140  4re  9143  5re  9145  6re  9147  7re  9149  8re  9151  9re  9153  0le2  9156  2pos  9157  3pos  9160  4pos  9163  5pos  9166  6pos  9167  7pos  9168  8pos  9169  9pos  9170  neg1rr  9172  neg1lt0  9174  1lt2  9236  1lt3  9238  1lt4  9241  1lt5  9245  1lt6  9250  1lt7  9256  1lt8  9263  1lt9  9271  1ne2  9273  1ap2  9274  1le2  9275  1le3  9278  halflt1  9284  iap0  9290  addltmul  9304  elnnnn0c  9370  nn0ge2m1nn  9385  elnnz1  9425  zltp1le  9457  zleltp1  9458  recnz  9496  gtndiv  9498  3halfnz  9500  1lt10  9672  eluzp1m1  9702  eluzp1p1  9704  eluz2b2  9754  1rp  9809  divlt1lt  9876  divle1le  9877  nnledivrp  9918  0elunit  10138  1elunit  10139  divelunit  10154  lincmb01cmp  10155  iccf1o  10156  unitssre  10157  fzpreddisj  10223  fznatpl1  10228  fztpval  10235  qbtwnxr  10432  flqbi2  10466  fldiv4p1lem1div2  10480  flqdiv  10498  seqf1oglem1  10696  reexpcl  10733  reexpclzap  10736  expge0  10752  expge1  10753  expgt1  10754  bernneq  10837  bernneq2  10838  expnbnd  10840  expnlbnd  10841  expnlbnd2  10842  nn0ltexp2  10886  facwordi  10917  faclbnd3  10920  faclbnd6  10921  facavg  10923  lsw0  11073  cjexp  11289  re1  11293  im1  11294  rei  11295  imi  11296  caucvgre  11377  sqrt1  11442  sqrt2gt1lt2  11445  abs1  11468  caubnd2  11513  mulcn2  11708  reccn2ap  11709  expcnvap0  11898  geo2sum  11910  cvgratnnlemrate  11926  fprodge0  12033  fprodge1  12035  fprodle  12036  ere  12066  ege2le3  12067  efgt1  12093  resin4p  12114  recos4p  12115  sinbnd  12148  cosbnd  12149  sinbnd2  12150  cosbnd2  12151  ef01bndlem  12152  sin01bnd  12153  cos01bnd  12154  cos1bnd  12155  cos2bnd  12156  sinltxirr  12157  sin01gt0  12158  cos01gt0  12159  sin02gt0  12160  sincos1sgn  12161  cos12dec  12164  ene1  12181  eap1  12182  3dvds  12260  halfleoddlt  12290  flodddiv4  12332  isprm3  12525  sqnprm  12543  coprm  12551  phibndlem  12623  pythagtriplem3  12675  fldivp1  12756  pockthi  12766  exmidunben  12882  basendxnmulrndx  13051  starvndxnbasendx  13059  scandxnbasendx  13071  vscandxnbasendx  13076  ipndxnbasendx  13089  basendxnocndx  13130  setsmsbasg  15036  tgioo  15111  dveflem  15283  reeff1olem  15328  reeff1o  15330  cosz12  15337  sinhalfpilem  15348  tangtx  15395  sincos4thpi  15397  pigt3  15401  coskpi  15405  cos0pilt1  15409  ioocosf1o  15411  loge  15424  logrpap0b  15433  logdivlti  15438  2logb9irrALT  15531  sqrt2cxp2logb9e3  15532  perfectlem2  15557  lgsdir  15597  lgsne0  15600  lgsabs1  15601  lgsdinn0  15610  gausslemma2dlem0i  15619  lgseisen  15636  2lgslem3  15663  ex-fl  15831  cvgcmp2nlemabs  16143  iooref1o  16145  trilpolemclim  16147  trilpolemcl  16148  trilpolemisumle  16149  trilpolemeq1  16151  trilpolemlt1  16152  apdiff  16159  nconstwlpolemgt0  16175