Theorem 1re 8156

Description: 1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)

Assertion

Ref	Expression
1re	|- 1 e. RR

Proof of Theorem 1re

Step	Hyp	Ref	Expression
1		ax-1re 8104	1 |- 1 e. RR

Syntax hints:   e. wcel 2200   RRcr 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  11420  re1  11424  im1  11425  rei  11426  imi  11427  caucvgre  11508  sqrt1  11573  sqrt2gt1lt2  11576  abs1  11599  caubnd2  11644  mulcn2  11839  reccn2ap  11840  expcnvap0  12029  geo2sum  12041  cvgratnnlemrate  12057  fprodge0  12164  fprodge1  12166  fprodle  12167  ere  12197  ege2le3  12198  efgt1  12224  resin4p  12245  recos4p  12246  sinbnd  12279  cosbnd  12280  sinbnd2  12281  cosbnd2  12282  ef01bndlem  12283  sin01bnd  12284  cos01bnd  12285  cos1bnd  12286  cos2bnd  12287  sinltxirr  12288  sin01gt0  12289  cos01gt0  12290  sin02gt0  12291  sincos1sgn  12292  cos12dec  12295  ene1  12312  eap1  12313  3dvds  12391  halfleoddlt  12421  flodddiv4  12463  isprm3  12656  sqnprm  12674  coprm  12682  phibndlem  12754  pythagtriplem3  12806  fldivp1  12887  pockthi  12897  exmidunben  13013  basendxnmulrndx  13183  starvndxnbasendx  13191  scandxnbasendx  13203  vscandxnbasendx  13208  ipndxnbasendx  13221  basendxnocndx  13262  setsmsbasg  15169  tgioo  15244  dveflem  15416  reeff1olem  15461  reeff1o  15463  cosz12  15470  sinhalfpilem  15481  tangtx  15528  sincos4thpi  15530  pigt3  15534  coskpi  15538  cos0pilt1  15542  ioocosf1o  15544  loge  15557  logrpap0b  15566  logdivlti  15571  2logb9irrALT  15664  sqrt2cxp2logb9e3  15665  perfectlem2  15690  lgsdir  15730  lgsne0  15733  lgsabs1  15734  lgsdinn0  15743  gausslemma2dlem0i  15752  lgseisen  15769  2lgslem3  15796  ex-fl  16172  cvgcmp2nlemabs  16488  iooref1o  16490  trilpolemclim  16492  trilpolemcl  16493  trilpolemisumle  16494  trilpolemeq1  16496  trilpolemlt1  16497  apdiff  16504  nconstwlpolemgt0  16520