Theorem 1re 8156

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

Syntax hints:   ∈ wcel 2200  ℝcr 8009  1c1 8011

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

This theorem is referenced by:  0re  8157  1red  8172  1xr  8216  0lt1  8284  peano2re  8293  peano2rem  8424  0reALT  8454  0le1  8639  1le1  8730  inelr  8742  1ap0  8748  eqneg  8890  ltp1  9002  ltm1  9004  recgt0  9008  mulgt1  9021  ltmulgt11  9022  lemulge11  9024  reclt1  9054  recgt1  9055  recgt1i  9056  recp1lt1  9057  recreclt  9058  sup3exmid  9115  cju  9119  peano5nni  9124  nnssre  9125  1nn  9132  nnge1  9144  nnle1eq1  9145  nngt0  9146  nnnlt1  9147  nn1gt1  9155  nngt1ne1  9156  nnrecre  9158  nnrecgt0  9159  nnsub  9160  2re  9191  3re  9195  4re  9198  5re  9200  6re  9202  7re  9204  8re  9206  9re  9208  0le2  9211  2pos  9212  3pos  9215  4pos  9218  5pos  9221  6pos  9222  7pos  9223  8pos  9224  9pos  9225  neg1rr  9227  neg1lt0  9229  1lt2  9291  1lt3  9293  1lt4  9296  1lt5  9300  1lt6  9305  1lt7  9311  1lt8  9318  1lt9  9326  1ne2  9328  1ap2  9329  1le2  9330  1le3  9333  halflt1  9339  iap0  9345  addltmul  9359  elnnnn0c  9425  nn0ge2m1nn  9440  elnnz1  9480  zltp1le  9512  zleltp1  9513  recnz  9551  gtndiv  9553  3halfnz  9555  1lt10  9727  eluzp1m1  9758  eluzp1p1  9760  eluz2b2  9810  1rp  9865  divlt1lt  9932  divle1le  9933  nnledivrp  9974  0elunit  10194  1elunit  10195  divelunit  10210  lincmb01cmp  10211  iccf1o  10212  unitssre  10213  fzpreddisj  10279  fznatpl1  10284  fztpval  10291  qbtwnxr  10489  flqbi2  10523  fldiv4p1lem1div2  10537  flqdiv  10555  seqf1oglem1  10753  reexpcl  10790  reexpclzap  10793  expge0  10809  expge1  10810  expgt1  10811  bernneq  10894  bernneq2  10895  expnbnd  10897  expnlbnd  10898  expnlbnd2  10899  nn0ltexp2  10943  facwordi  10974  faclbnd3  10977  faclbnd6  10978  facavg  10980  lsw0  11132  cjexp  11419  re1  11423  im1  11424  rei  11425  imi  11426  caucvgre  11507  sqrt1  11572  sqrt2gt1lt2  11575  abs1  11598  caubnd2  11643  mulcn2  11838  reccn2ap  11839  expcnvap0  12028  geo2sum  12040  cvgratnnlemrate  12056  fprodge0  12163  fprodge1  12165  fprodle  12166  ere  12196  ege2le3  12197  efgt1  12223  resin4p  12244  recos4p  12245  sinbnd  12278  cosbnd  12279  sinbnd2  12280  cosbnd2  12281  ef01bndlem  12282  sin01bnd  12283  cos01bnd  12284  cos1bnd  12285  cos2bnd  12286  sinltxirr  12287  sin01gt0  12288  cos01gt0  12289  sin02gt0  12290  sincos1sgn  12291  cos12dec  12294  ene1  12311  eap1  12312  3dvds  12390  halfleoddlt  12420  flodddiv4  12462  isprm3  12655  sqnprm  12673  coprm  12681  phibndlem  12753  pythagtriplem3  12805  fldivp1  12886  pockthi  12896  exmidunben  13012  basendxnmulrndx  13182  starvndxnbasendx  13190  scandxnbasendx  13202  vscandxnbasendx  13207  ipndxnbasendx  13220  basendxnocndx  13261  setsmsbasg  15168  tgioo  15243  dveflem  15415  reeff1olem  15460  reeff1o  15462  cosz12  15469  sinhalfpilem  15480  tangtx  15527  sincos4thpi  15529  pigt3  15533  coskpi  15537  cos0pilt1  15541  ioocosf1o  15543  loge  15556  logrpap0b  15565  logdivlti  15570  2logb9irrALT  15663  sqrt2cxp2logb9e3  15664  perfectlem2  15689  lgsdir  15729  lgsne0  15732  lgsabs1  15733  lgsdinn0  15742  gausslemma2dlem0i  15751  lgseisen  15768  2lgslem3  15795  ex-fl  16144  cvgcmp2nlemabs  16460  iooref1o  16462  trilpolemclim  16464  trilpolemcl  16465  trilpolemisumle  16466  trilpolemeq1  16468  trilpolemlt1  16469  apdiff  16476  nconstwlpolemgt0  16492