Theorem 2re 9218

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 9207	. 2 |- 2 = ( 1 + 1 )
2		1re 8183	. . 3 |- 1 e. RR
3	2, 2	readdcli 8197	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2303	1 |- 2 e. RR

Syntax hints:   e. wcel 2201  (class class class)co 6023   RRcr 8036   1c1 8038   + caddc 8040   2c2 9199

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 2212  ax-1re 8131  ax-addrcl 8134

This theorem depends on definitions:  df-bi 117  df-cleq 2223  df-clel 2226  df-2 9207

This theorem is referenced by:  2cn  9219  3re  9222  2ne0  9240  2ap0  9241  3pos  9242  2lt3  9319  1lt3  9320  2lt4  9322  1lt4  9323  2lt5  9326  2lt6  9331  1lt6  9332  2lt7  9337  1lt7  9338  2lt8  9344  1lt8  9345  2lt9  9352  1lt9  9353  1ap2  9356  1le2  9357  2rene0  9359  halfre  9362  halfgt0  9364  halflt1  9366  rehalfcl  9376  halfpos2  9379  halfnneg2  9381  addltmul  9386  nominpos  9387  avglt1  9388  avglt2  9389  div4p1lem1div2  9403  nn0lele2xi  9458  nn0ge2m1nn  9467  halfnz  9581  3halfnz  9582  2lt10  9753  1lt10  9754  uzuzle23  9801  uzuzle24  9802  eluz4eluz2  9807  uz3m2nn  9812  2rp  9898  xleaddadd  10127  fztpval  10323  fz0to4untppr  10364  fzo0to42pr  10471  qbtwnrelemcalc  10521  qbtwnre  10522  2tnp1ge0ge0  10567  flhalf  10568  fldiv4p1lem1div2  10571  mulp1mod1  10633  expubnd  10864  nn0opthlem2d  10989  faclbnd2  11010  4bc2eq6  11042  hashtpglem  11116  wrdlenge2n0  11158  cvg1nlemres  11568  resqrexlemover  11593  resqrexlemga  11606  sqrt4  11630  sqrt2gt1lt2  11632  abstri  11687  amgm2  11701  maxabslemlub  11790  maxltsup  11801  bdtrilem  11822  efcllemp  12242  efcllem  12243  ege2le3  12255  ef01bndlem  12340  cos01bnd  12342  cos2bnd  12344  cos01gt0  12347  sin02gt0  12348  sincos2sgn  12350  sin4lt0  12351  cos12dec  12352  eirraplem  12361  egt2lt3  12364  epos  12365  ene1  12369  eap1  12370  oexpneg  12461  oddge22np1  12465  evennn02n  12466  evennn2n  12467  nn0ehalf  12487  nno  12490  nn0o  12491  nn0oddm1d2  12493  nnoddm1d2  12494  flodddiv4t2lthalf  12523  bitsp1o  12537  bitsfzolem  12538  bitsfzo  12539  bitsfi  12541  6gcd4e2  12589  ncoprmgcdne1b  12684  prmdc  12725  3lcm2e6  12755  sqrt2irrlem  12756  sqrt2re  12758  sqrt2irraplemnn  12774  sqrt2irrap  12775  4sqlem11  12997  4sqlem12  12998  2expltfac  13035  plusgndxnmulrndx  13239  starvndxnplusgndx  13249  scandxnplusgndx  13261  vscandxnplusgndx  13266  ipndxnplusgndx  13279  tsetndxnplusgndx  13298  plendxnplusgndx  13312  dsndxnplusgndx  13327  slotsdifunifndx  13338  bl2in  15156  hoverb  15401  ivthdichlem  15404  reeff1o  15526  cosz12  15533  sin0pilem1  15534  sin0pilem2  15535  pilem3  15536  pipos  15541  sinhalfpilem  15544  sincosq1lem  15578  sincosq4sgn  15582  sinq12gt0  15583  cosq23lt0  15586  coseq00topi  15588  coseq0negpitopi  15589  tangtx  15591  sincos4thpi  15593  tan4thpi  15594  sincos6thpi  15595  cosordlem  15602  cosq34lt1  15603  cos02pilt1  15604  cos0pilt1  15605  2logb9irr  15724  2logb3irr  15726  2logb9irrALT  15727  sqrt2cxp2logb9e3  15728  2logb9irrap  15730  mersenne  15750  perfectlem1  15752  perfectlem2  15753  lgslem1  15758  lgsdirprm  15792  gausslemma2dlem0c  15809  gausslemma2dlem1a  15816  gausslemma2dlem2  15820  gausslemma2dlem3  15821  gausslemma2dlem4  15822  lgseisenlem1  15828  lgseisenlem2  15829  lgseisenlem3  15830  lgseisen  15832  lgsquadlem1  15835  lgsquadlem2  15836  2lgslem1a1  15844  2lgslem1a2  15845  2lgslem1c  15848  2lgslem4  15861  usgrexmpldifpr  16129  clwwlkext2edg  16302  konigsbergiedgwen  16364  konigsberglem1  16368  konigsberglem2  16369  konigsberglem3  16370  konigsberg  16373  ex-fl  16378  taupi  16745