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  11267  resqrexlemover  11292  resqrexlemga  11305  sqrt4  11329  sqrt2gt1lt2  11331  abstri  11386  amgm2  11400  maxabslemlub  11489  maxltsup  11500  bdtrilem  11521  efcllemp  11940  efcllem  11941  ege2le3  11953  ef01bndlem  12038  cos01bnd  12040  cos2bnd  12042  cos01gt0  12045  sin02gt0  12046  sincos2sgn  12048  sin4lt0  12049  cos12dec  12050  eirraplem  12059  egt2lt3  12062  epos  12063  ene1  12067  eap1  12068  oexpneg  12159  oddge22np1  12163  evennn02n  12164  evennn2n  12165  nn0ehalf  12185  nno  12188  nn0o  12189  nn0oddm1d2  12191  nnoddm1d2  12192  flodddiv4t2lthalf  12221  bitsp1o  12235  bitsfzolem  12236  bitsfzo  12237  bitsfi  12239  6gcd4e2  12287  ncoprmgcdne1b  12382  prmdc  12423  3lcm2e6  12453  sqrt2irrlem  12454  sqrt2re  12456  sqrt2irraplemnn  12472  sqrt2irrap  12473  4sqlem11  12695  4sqlem12  12696  2expltfac  12733  plusgndxnmulrndx  12936  starvndxnplusgndx  12946  scandxnplusgndx  12958  vscandxnplusgndx  12963  ipndxnplusgndx  12976  tsetndxnplusgndx  12995  plendxnplusgndx  13009  dsndxnplusgndx  13024  slotsdifunifndx  13035  bl2in  14846  hoverb  15091  ivthdichlem  15094  reeff1o  15216  cosz12  15223  sin0pilem1  15224  sin0pilem2  15225  pilem3  15226  pipos  15231  sinhalfpilem  15234  sincosq1lem  15268  sincosq4sgn  15272  sinq12gt0  15273  cosq23lt0  15276  coseq00topi  15278  coseq0negpitopi  15279  tangtx  15281  sincos4thpi  15283  tan4thpi  15284  sincos6thpi  15285  cosordlem  15292  cosq34lt1  15293  cos02pilt1  15294  cos0pilt1  15295  2logb9irr  15414  2logb3irr  15416  2logb9irrALT  15417  sqrt2cxp2logb9e3  15418  2logb9irrap  15420  mersenne  15440  perfectlem1  15442  perfectlem2  15443  lgslem1  15448  lgsdirprm  15482  gausslemma2dlem0c  15499  gausslemma2dlem1a  15506  gausslemma2dlem2  15510  gausslemma2dlem3  15511  gausslemma2dlem4  15512  lgseisenlem1  15518  lgseisenlem2  15519  lgseisenlem3  15520  lgseisen  15522  lgsquadlem1  15525  lgsquadlem2  15526  2lgslem1a1  15534  2lgslem1a2  15535  2lgslem1c  15538  2lgslem4  15551  ex-fl  15623  taupi  15974