Theorem 1re 8331

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

This proof depends on syntax axioms:   ∈ wcel 2209  ℝcr 8184  1c1 8186

This proof depends on axioms:  ax-1re 8279

This theorem is used by:  0re  8332  1red  8347  1xr  8390  0lt1  8460  peano2re  8469  peano2rem  8600  0reALT  8630  0le1  8816  1le1  8908  inelr  8920  1ap0  8926  eqneg  9070  ltp1  9182  ltm1  9184  recgt0  9188  mulgt1  9201  ltmulgt11  9202  lemulge11  9204  reclt1  9234  recgt1  9235  recgt1i  9236  recp1lt1  9237  recreclt  9238  sup3exmid  9295  cju  9299  indfval  9308  indconst1  9312  peano5nni  9316  nnssre  9317  1nn  9324  nnge1  9336  nnle1eq1  9337  nngt0  9338  nnnlt1  9339  nn1gt1  9347  nngt1ne1  9348  nnrecre  9350  nnrecgt0  9351  nnsub  9352  2re  9383  3re  9387  4re  9390  5re  9392  6re  9394  7re  9396  8re  9398  9re  9400  0le2  9403  2pos  9404  3pos  9407  4pos  9410  5pos  9413  6pos  9414  7pos  9415  8pos  9416  9pos  9417  neg1rr  9419  neg1lt0  9421  1lt2  9485  1lt3  9487  1lt4  9490  1lt5  9494  1lt6  9499  1lt7  9505  1lt8  9512  1lt9  9520  1ne2  9522  1ap2  9523  1le2  9524  1le3  9527  halflt1  9533  iap0  9539  addltmul  9553  elnnnn0c  9619  nn0ge2m1nn  9638  elnnz1  9678  zltp1le  9710  zleltp1  9711  recnz  9750  gtndiv  9752  3halfnz  9754  1lt10  9931  eluzp1m1  9962  eluzp1p1  9964  eluz2b2  10019  1rp  10075  divlt1lt  10142  divle1le  10143  nnledivrp  10184  0elunit  10405  1elunit  10406  divelunit  10421  lincmb01cmp  10422  lincmble  10423  iccf1o  10424  unitssre  10425  fzpreddisj  10495  fznatpl1  10500  fztpval  10507  qbtwnxr  10709  flqbi2  10747  fldiv4p1lem1div2  10761  flqdiv  10779  seqf1oglem1  10977  reexpcl  11014  reexpclzap  11017  expge0  11033  expge1  11034  expgt1  11035  resq01  11116  bernneq  11119  bernneq2  11120  expnbnd  11122  expnlbnd  11123  expnlbnd2  11124  nn0ltexp2  11169  facwordi  11200  faclbnd3  11203  faclbnd6  11204  facavg  11206  hashtpglem  11320  lsw0  11374  cjexp  11680  re1  11685  im1  11686  rei  11687  imi  11688  caucvgre  11769  sqrt1  11834  sqrt2gt1lt2  11837  abs1  11860  caubnd2  11906  mulcn2  12103  reccn2ap  12104  expcnvap0  12294  geo2sum  12306  cvgratnnlemrate  12322  fprodge0  12429  fprodge1  12431  fprodle  12432  ere  12462  ege2le3  12463  efgt1  12489  resin4p  12510  recos4p  12511  sinbnd  12544  cosbnd  12545  sinbnd2  12546  cosbnd2  12547  ef01bndlem  12548  sin01bnd  12549  cos01bnd  12550  cos1bnd  12551  cos2bnd  12552  sinltxirr  12553  sin01gt0  12554  cos01gt0  12555  sin02gt0  12556  sincos1sgn  12557  cos12dec  12560  ene1  12577  eap1  12578  3dvds  12656  halfleoddlt  12686  flodddiv4  12728  isprm3  12921  sqnprm  12940  coprm  12948  phibndlem  13023  pythagtriplem3  13075  fldivp1  13156  pockthi  13166  ballotfilem2  13286  ballotfilem4  13299  ballotfilemi1  13303  ballotfilemic  13308  exmidunben  13375  basendxnmulrndx  13547  starvndxnbasendx  13555  scandxnbasendx  13567  vscandxnbasendx  13572  ipndxnbasendx  13585  basendxnocndx  13626  setsmsbasg  15705  tgioo  15780  dveflem  15952  reeff1olem  15997  reeff1o  15999  cosz12  16007  sinhalfpilem  16018  tangtx  16065  sincos4thpi  16067  pigt3  16071  coskpi  16075  cos0pilt1  16080  ioocosf1o  16082  loge  16096  logrpap0b  16106  logdivlti  16111  2logb9irrALT  16210  sqrt2cxp2logb9e3  16211  birthdaylem3  16227  ppiublem1  16291  ppiqub  16293  chtublem  16295  chtqub  16296  perfectlem2  16300  bposlem1  16311  bposlem2  16312  bposlem5  16315  bposlem8  16318  lgsdir  16359  lgsne0  16362  lgsabs1  16363  lgsdinn0  16372  gausslemma2dlem0i  16381  lgseisen  16398  2lgslem3  16425  usgrexmpldifpr  16695  konigsberglem2  16935  konigsberglem3  16936  konigsberglem5  16938  ex-fl  16944  cvgcmp2nlemabs  17287  iooref1o  17289  trilpolemclim  17292  trilpolemcl  17293  trilpolemisumle  17294  trilpolemeq1  17296  trilpolemlt1  17297  apdiff  17304  nconstwlpolemgt0  17321