Theorem 2re 9213

Description: The number 2 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
2re	|- 2 e. RR

Proof of Theorem 2re

Step	Hyp	Ref	Expression
1		df-2 9202	. 2 |- 2 = ( 1 + 1 )
2		1re 8178	. . 3 |- 1 e. RR
3	2, 2	readdcli 8192	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2304	1 |- 2 e. RR

Syntax hints:   e. wcel 2202  (class class class)co 6018   RRcr 8031   1c1 8033   + caddc 8035   2c2 9194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9202

This theorem is referenced by:  2cn  9214  3re  9217  2ne0  9235  2ap0  9236  3pos  9237  2lt3  9314  1lt3  9315  2lt4  9317  1lt4  9318  2lt5  9321  2lt6  9326  1lt6  9327  2lt7  9332  1lt7  9333  2lt8  9339  1lt8  9340  2lt9  9347  1lt9  9348  1ap2  9351  1le2  9352  2rene0  9354  halfre  9357  halfgt0  9359  halflt1  9361  rehalfcl  9371  halfpos2  9374  halfnneg2  9376  addltmul  9381  nominpos  9382  avglt1  9383  avglt2  9384  div4p1lem1div2  9398  nn0lele2xi  9453  nn0ge2m1nn  9462  halfnz  9576  3halfnz  9577  2lt10  9748  1lt10  9749  uzuzle23  9796  uzuzle24  9797  eluz4eluz2  9802  uz3m2nn  9807  2rp  9893  xleaddadd  10122  fztpval  10318  fz0to4untppr  10359  fzo0to42pr  10466  qbtwnrelemcalc  10516  qbtwnre  10517  2tnp1ge0ge0  10562  flhalf  10563  fldiv4p1lem1div2  10566  mulp1mod1  10628  expubnd  10859  nn0opthlem2d  10984  faclbnd2  11005  4bc2eq6  11037  wrdlenge2n0  11150  cvg1nlemres  11547  resqrexlemover  11572  resqrexlemga  11585  sqrt4  11609  sqrt2gt1lt2  11611  abstri  11666  amgm2  11680  maxabslemlub  11769  maxltsup  11780  bdtrilem  11801  efcllemp  12221  efcllem  12222  ege2le3  12234  ef01bndlem  12319  cos01bnd  12321  cos2bnd  12323  cos01gt0  12326  sin02gt0  12327  sincos2sgn  12329  sin4lt0  12330  cos12dec  12331  eirraplem  12340  egt2lt3  12343  epos  12344  ene1  12348  eap1  12349  oexpneg  12440  oddge22np1  12444  evennn02n  12445  evennn2n  12446  nn0ehalf  12466  nno  12469  nn0o  12470  nn0oddm1d2  12472  nnoddm1d2  12473  flodddiv4t2lthalf  12502  bitsp1o  12516  bitsfzolem  12517  bitsfzo  12518  bitsfi  12520  6gcd4e2  12568  ncoprmgcdne1b  12663  prmdc  12704  3lcm2e6  12734  sqrt2irrlem  12735  sqrt2re  12737  sqrt2irraplemnn  12753  sqrt2irrap  12754  4sqlem11  12976  4sqlem12  12977  2expltfac  13014  plusgndxnmulrndx  13218  starvndxnplusgndx  13228  scandxnplusgndx  13240  vscandxnplusgndx  13245  ipndxnplusgndx  13258  tsetndxnplusgndx  13277  plendxnplusgndx  13291  dsndxnplusgndx  13306  slotsdifunifndx  13317  bl2in  15130  hoverb  15375  ivthdichlem  15378  reeff1o  15500  cosz12  15507  sin0pilem1  15508  sin0pilem2  15509  pilem3  15510  pipos  15515  sinhalfpilem  15518  sincosq1lem  15552  sincosq4sgn  15556  sinq12gt0  15557  cosq23lt0  15560  coseq00topi  15562  coseq0negpitopi  15563  tangtx  15565  sincos4thpi  15567  tan4thpi  15568  sincos6thpi  15569  cosordlem  15576  cosq34lt1  15577  cos02pilt1  15578  cos0pilt1  15579  2logb9irr  15698  2logb3irr  15700  2logb9irrALT  15701  sqrt2cxp2logb9e3  15702  2logb9irrap  15704  mersenne  15724  perfectlem1  15726  perfectlem2  15727  lgslem1  15732  lgsdirprm  15766  gausslemma2dlem0c  15783  gausslemma2dlem1a  15790  gausslemma2dlem2  15794  gausslemma2dlem3  15795  gausslemma2dlem4  15796  lgseisenlem1  15802  lgseisenlem2  15803  lgseisenlem3  15804  lgseisen  15806  lgsquadlem1  15809  lgsquadlem2  15810  2lgslem1a1  15818  2lgslem1a2  15819  2lgslem1c  15822  2lgslem4  15835  usgrexmpldifpr  16103  clwwlkext2edg  16276  ex-fl  16338  taupi  16698