Theorem 2re 9203

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

Assertion

Ref	Expression
2re	⊢ 2 ∈ ℝ

Proof of Theorem 2re

Step	Hyp	Ref	Expression
1		df-2 9192	. 2 ⊢ 2 = (1 + 1)
2		1re 8168	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 8182	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2302	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2200  (class class class)co 6013  ℝcr 8021  1c1 8023   + caddc 8025  2c2 9184

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211  ax-1re 8116  ax-addrcl 8119

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225  df-2 9192

This theorem is referenced by:  2cn  9204  3re  9207  2ne0  9225  2ap0  9226  3pos  9227  2lt3  9304  1lt3  9305  2lt4  9307  1lt4  9308  2lt5  9311  2lt6  9316  1lt6  9317  2lt7  9322  1lt7  9323  2lt8  9329  1lt8  9330  2lt9  9337  1lt9  9338  1ap2  9341  1le2  9342  2rene0  9344  halfre  9347  halfgt0  9349  halflt1  9351  rehalfcl  9361  halfpos2  9364  halfnneg2  9366  addltmul  9371  nominpos  9372  avglt1  9373  avglt2  9374  div4p1lem1div2  9388  nn0lele2xi  9443  nn0ge2m1nn  9452  halfnz  9566  3halfnz  9567  2lt10  9738  1lt10  9739  uzuzle23  9786  uzuzle24  9787  eluz4eluz2  9792  uz3m2nn  9797  2rp  9883  xleaddadd  10112  fztpval  10308  fz0to4untppr  10349  fzo0to42pr  10455  qbtwnrelemcalc  10505  qbtwnre  10506  2tnp1ge0ge0  10551  flhalf  10552  fldiv4p1lem1div2  10555  mulp1mod1  10617  expubnd  10848  nn0opthlem2d  10973  faclbnd2  10994  4bc2eq6  11026  wrdlenge2n0  11139  cvg1nlemres  11536  resqrexlemover  11561  resqrexlemga  11574  sqrt4  11598  sqrt2gt1lt2  11600  abstri  11655  amgm2  11669  maxabslemlub  11758  maxltsup  11769  bdtrilem  11790  efcllemp  12209  efcllem  12210  ege2le3  12222  ef01bndlem  12307  cos01bnd  12309  cos2bnd  12311  cos01gt0  12314  sin02gt0  12315  sincos2sgn  12317  sin4lt0  12318  cos12dec  12319  eirraplem  12328  egt2lt3  12331  epos  12332  ene1  12336  eap1  12337  oexpneg  12428  oddge22np1  12432  evennn02n  12433  evennn2n  12434  nn0ehalf  12454  nno  12457  nn0o  12458  nn0oddm1d2  12460  nnoddm1d2  12461  flodddiv4t2lthalf  12490  bitsp1o  12504  bitsfzolem  12505  bitsfzo  12506  bitsfi  12508  6gcd4e2  12556  ncoprmgcdne1b  12651  prmdc  12692  3lcm2e6  12722  sqrt2irrlem  12723  sqrt2re  12725  sqrt2irraplemnn  12741  sqrt2irrap  12742  4sqlem11  12964  4sqlem12  12965  2expltfac  13002  plusgndxnmulrndx  13206  starvndxnplusgndx  13216  scandxnplusgndx  13228  vscandxnplusgndx  13233  ipndxnplusgndx  13246  tsetndxnplusgndx  13265  plendxnplusgndx  13279  dsndxnplusgndx  13294  slotsdifunifndx  13305  bl2in  15117  hoverb  15362  ivthdichlem  15365  reeff1o  15487  cosz12  15494  sin0pilem1  15495  sin0pilem2  15496  pilem3  15497  pipos  15502  sinhalfpilem  15505  sincosq1lem  15539  sincosq4sgn  15543  sinq12gt0  15544  cosq23lt0  15547  coseq00topi  15549  coseq0negpitopi  15550  tangtx  15552  sincos4thpi  15554  tan4thpi  15555  sincos6thpi  15556  cosordlem  15563  cosq34lt1  15564  cos02pilt1  15565  cos0pilt1  15566  2logb9irr  15685  2logb3irr  15687  2logb9irrALT  15688  sqrt2cxp2logb9e3  15689  2logb9irrap  15691  mersenne  15711  perfectlem1  15713  perfectlem2  15714  lgslem1  15719  lgsdirprm  15753  gausslemma2dlem0c  15770  gausslemma2dlem1a  15777  gausslemma2dlem2  15781  gausslemma2dlem3  15782  gausslemma2dlem4  15783  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisen  15793  lgsquadlem1  15796  lgsquadlem2  15797  2lgslem1a1  15805  2lgslem1a2  15806  2lgslem1c  15809  2lgslem4  15822  usgrexmpldifpr  16088  clwwlkext2edg  16217  ex-fl  16257  taupi  16613