Theorem 1re 8168

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

Syntax hints:   ∈ wcel 2200  ℝcr 8021  1c1 8023

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

This theorem is referenced by:  0re  8169  1red  8184  1xr  8228  0lt1  8296  peano2re  8305  peano2rem  8436  0reALT  8466  0le1  8651  1le1  8742  inelr  8754  1ap0  8760  eqneg  8902  ltp1  9014  ltm1  9016  recgt0  9020  mulgt1  9033  ltmulgt11  9034  lemulge11  9036  reclt1  9066  recgt1  9067  recgt1i  9068  recp1lt1  9069  recreclt  9070  sup3exmid  9127  cju  9131  peano5nni  9136  nnssre  9137  1nn  9144  nnge1  9156  nnle1eq1  9157  nngt0  9158  nnnlt1  9159  nn1gt1  9167  nngt1ne1  9168  nnrecre  9170  nnrecgt0  9171  nnsub  9172  2re  9203  3re  9207  4re  9210  5re  9212  6re  9214  7re  9216  8re  9218  9re  9220  0le2  9223  2pos  9224  3pos  9227  4pos  9230  5pos  9233  6pos  9234  7pos  9235  8pos  9236  9pos  9237  neg1rr  9239  neg1lt0  9241  1lt2  9303  1lt3  9305  1lt4  9308  1lt5  9312  1lt6  9317  1lt7  9323  1lt8  9330  1lt9  9338  1ne2  9340  1ap2  9341  1le2  9342  1le3  9345  halflt1  9351  iap0  9357  addltmul  9371  elnnnn0c  9437  nn0ge2m1nn  9452  elnnz1  9492  zltp1le  9524  zleltp1  9525  recnz  9563  gtndiv  9565  3halfnz  9567  1lt10  9739  eluzp1m1  9770  eluzp1p1  9772  eluz2b2  9827  1rp  9882  divlt1lt  9949  divle1le  9950  nnledivrp  9991  0elunit  10211  1elunit  10212  divelunit  10227  lincmb01cmp  10228  iccf1o  10229  unitssre  10230  fzpreddisj  10296  fznatpl1  10301  fztpval  10308  qbtwnxr  10507  flqbi2  10541  fldiv4p1lem1div2  10555  flqdiv  10573  seqf1oglem1  10771  reexpcl  10808  reexpclzap  10811  expge0  10827  expge1  10828  expgt1  10829  bernneq  10912  bernneq2  10913  expnbnd  10915  expnlbnd  10916  expnlbnd2  10917  nn0ltexp2  10961  facwordi  10992  faclbnd3  10995  faclbnd6  10996  facavg  10998  lsw0  11151  cjexp  11444  re1  11448  im1  11449  rei  11450  imi  11451  caucvgre  11532  sqrt1  11597  sqrt2gt1lt2  11600  abs1  11623  caubnd2  11668  mulcn2  11863  reccn2ap  11864  expcnvap0  12053  geo2sum  12065  cvgratnnlemrate  12081  fprodge0  12188  fprodge1  12190  fprodle  12191  ere  12221  ege2le3  12222  efgt1  12248  resin4p  12269  recos4p  12270  sinbnd  12303  cosbnd  12304  sinbnd2  12305  cosbnd2  12306  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  cos1bnd  12310  cos2bnd  12311  sinltxirr  12312  sin01gt0  12313  cos01gt0  12314  sin02gt0  12315  sincos1sgn  12316  cos12dec  12319  ene1  12336  eap1  12337  3dvds  12415  halfleoddlt  12445  flodddiv4  12487  isprm3  12680  sqnprm  12698  coprm  12706  phibndlem  12778  pythagtriplem3  12830  fldivp1  12911  pockthi  12921  exmidunben  13037  basendxnmulrndx  13207  starvndxnbasendx  13215  scandxnbasendx  13227  vscandxnbasendx  13232  ipndxnbasendx  13245  basendxnocndx  13286  setsmsbasg  15193  tgioo  15268  dveflem  15440  reeff1olem  15485  reeff1o  15487  cosz12  15494  sinhalfpilem  15505  tangtx  15552  sincos4thpi  15554  pigt3  15558  coskpi  15562  cos0pilt1  15566  ioocosf1o  15568  loge  15581  logrpap0b  15590  logdivlti  15595  2logb9irrALT  15688  sqrt2cxp2logb9e3  15689  perfectlem2  15714  lgsdir  15754  lgsne0  15757  lgsabs1  15758  lgsdinn0  15767  gausslemma2dlem0i  15776  lgseisen  15793  2lgslem3  15820  usgrexmpldifpr  16088  ex-fl  16257  cvgcmp2nlemabs  16572  iooref1o  16574  trilpolemclim  16576  trilpolemcl  16577  trilpolemisumle  16578  trilpolemeq1  16580  trilpolemlt1  16581  apdiff  16588  nconstwlpolemgt0  16604