Theorem 2re 9105

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 9094	. 2 ⊢ 2 = (1 + 1)
2		1re 8070	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 8084	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2277	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2175  (class class class)co 5943  ℝcr 7923  1c1 7925   + caddc 7927  2c2 9086

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186  ax-1re 8018  ax-addrcl 8021

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200  df-2 9094

This theorem is referenced by:  2cn  9106  3re  9109  2ne0  9127  2ap0  9128  3pos  9129  2lt3  9206  1lt3  9207  2lt4  9209  1lt4  9210  2lt5  9213  2lt6  9218  1lt6  9219  2lt7  9224  1lt7  9225  2lt8  9231  1lt8  9232  2lt9  9239  1lt9  9240  1ap2  9243  1le2  9244  2rene0  9246  halfre  9249  halfgt0  9251  halflt1  9253  rehalfcl  9263  halfpos2  9266  halfnneg2  9268  addltmul  9273  nominpos  9274  avglt1  9275  avglt2  9276  div4p1lem1div2  9290  nn0lele2xi  9345  nn0ge2m1nn  9354  halfnz  9468  3halfnz  9469  2lt10  9640  1lt10  9641  eluz4eluz2  9687  uzuzle23  9691  uz3m2nn  9693  2rp  9779  xleaddadd  10008  fztpval  10204  fz0to4untppr  10245  fzo0to42pr  10347  qbtwnrelemcalc  10396  qbtwnre  10397  2tnp1ge0ge0  10442  flhalf  10443  fldiv4p1lem1div2  10446  mulp1mod1  10508  expubnd  10739  nn0opthlem2d  10864  faclbnd2  10885  4bc2eq6  10917  wrdlenge2n0  11027  cvg1nlemres  11238  resqrexlemover  11263  resqrexlemga  11276  sqrt4  11300  sqrt2gt1lt2  11302  abstri  11357  amgm2  11371  maxabslemlub  11460  maxltsup  11471  bdtrilem  11492  efcllemp  11911  efcllem  11912  ege2le3  11924  ef01bndlem  12009  cos01bnd  12011  cos2bnd  12013  cos01gt0  12016  sin02gt0  12017  sincos2sgn  12019  sin4lt0  12020  cos12dec  12021  eirraplem  12030  egt2lt3  12033  epos  12034  ene1  12038  eap1  12039  oexpneg  12130  oddge22np1  12134  evennn02n  12135  evennn2n  12136  nn0ehalf  12156  nno  12159  nn0o  12160  nn0oddm1d2  12162  nnoddm1d2  12163  flodddiv4t2lthalf  12192  bitsp1o  12206  bitsfzolem  12207  bitsfzo  12208  bitsfi  12210  6gcd4e2  12258  ncoprmgcdne1b  12353  prmdc  12394  3lcm2e6  12424  sqrt2irrlem  12425  sqrt2re  12427  sqrt2irraplemnn  12443  sqrt2irrap  12444  4sqlem11  12666  4sqlem12  12667  2expltfac  12704  plusgndxnmulrndx  12907  starvndxnplusgndx  12917  scandxnplusgndx  12929  vscandxnplusgndx  12934  ipndxnplusgndx  12947  tsetndxnplusgndx  12966  plendxnplusgndx  12980  dsndxnplusgndx  12995  slotsdifunifndx  13006  bl2in  14817  hoverb  15062  ivthdichlem  15065  reeff1o  15187  cosz12  15194  sin0pilem1  15195  sin0pilem2  15196  pilem3  15197  pipos  15202  sinhalfpilem  15205  sincosq1lem  15239  sincosq4sgn  15243  sinq12gt0  15244  cosq23lt0  15247  coseq00topi  15249  coseq0negpitopi  15250  tangtx  15252  sincos4thpi  15254  tan4thpi  15255  sincos6thpi  15256  cosordlem  15263  cosq34lt1  15264  cos02pilt1  15265  cos0pilt1  15266  2logb9irr  15385  2logb3irr  15387  2logb9irrALT  15388  sqrt2cxp2logb9e3  15389  2logb9irrap  15391  mersenne  15411  perfectlem1  15413  perfectlem2  15414  lgslem1  15419  lgsdirprm  15453  gausslemma2dlem0c  15470  gausslemma2dlem1a  15477  gausslemma2dlem2  15481  gausslemma2dlem3  15482  gausslemma2dlem4  15483  lgseisenlem1  15489  lgseisenlem2  15490  lgseisenlem3  15491  lgseisen  15493  lgsquadlem1  15496  lgsquadlem2  15497  2lgslem1a1  15505  2lgslem1a2  15506  2lgslem1c  15509  2lgslem4  15522  ex-fl  15594  taupi  15945