Theorem 2re 9376

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 9365	. 2 ⊢ 2 = (1 + 1)
2		1re 8325	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 8339	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2311	1 ⊢ 2 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2209  (class class class)co 6085  ℝcr 8178  1c1 8180   + caddc 8182  2c2 9357

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220  ax-1re 8273  ax-addrcl 8276

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234  df-2 9365

This theorem is used by:  2cn  9377  3re  9380  2ne0  9398  2ap0  9399  3pos  9400  2lt3  9479  1lt3  9480  2lt4  9482  1lt4  9483  2lt5  9486  2lt6  9491  1lt6  9492  2lt7  9497  1lt7  9498  2lt8  9504  1lt8  9505  2lt9  9512  1lt9  9513  1ap2  9516  1le2  9517  2rene0  9519  halfre  9522  halfgt0  9524  halflt1  9526  rehalfcl  9536  halfpos2  9539  halfnneg2  9541  addltmul  9546  nominpos  9547  avglt1  9548  avglt2  9549  div4p1lem1div2  9563  nn0lele2xi  9618  nn0ge2m1nn  9631  halfnz  9746  3halfnz  9747  2lt10  9923  1lt10  9924  uzuzle23  9971  uzuzle24  9972  eluz4eluz2  9977  uz3m2nn  9982  2rp  10069  xleaddadd  10299  fztpval  10500  fz0to4untppr  10541  fzo0to42pr  10648  qbtwnrelemcalc  10700  qbtwnre  10701  2tnp1ge0ge0  10749  flhalf  10750  fldiv4p1lem1div2  10753  mulp1mod1  10815  expubnd  11046  nn0opthlem2d  11173  faclbnd2  11194  4bc2eq6  11227  hashtpglem  11312  wrdlenge2n0  11354  sq01  11674  cvg1nlemres  11765  resqrexlemover  11790  resqrexlemga  11803  sqrt4  11827  sqrt2gt1lt2  11829  abstri  11885  amgm2  11899  maxabslemlub  11988  maxltsup  11999  bdtrilem  12021  efcllemp  12441  efcllem  12442  ege2le3  12454  ef01bndlem  12539  cos01bnd  12541  cos2bnd  12543  cos01gt0  12546  sin02gt0  12547  sincos2sgn  12549  sin4lt0  12550  cos12dec  12551  eirraplem  12560  egt2lt3  12563  epos  12564  ene1  12568  eap1  12569  oexpneg  12660  oddge22np1  12664  evennn02n  12665  evennn2n  12666  nn0ehalf  12686  nno  12689  nn0o  12690  nn0oddm1d2  12692  nnoddm1d2  12693  flodddiv4t2lthalf  12722  bitsp1o  12736  bitsfzolem  12737  bitsfzo  12738  bitsfi  12740  6gcd4e2  12788  ncoprmgcdne1b  12883  prmdc  12924  3lcm2e6  12955  sqrt2irrlem  12956  sqrt2re  12958  sqrt2irraplemnn  12975  sqrt2irrap  12976  4sqlem11  13200  4sqlem12  13201  2expltfac  13239  ballotfilem2  13277  plusgndxnmulrndx  13536  starvndxnplusgndx  13546  scandxnplusgndx  13558  vscandxnplusgndx  13563  ipndxnplusgndx  13576  tsetndxnplusgndx  13595  plendxnplusgndx  13609  dsndxnplusgndx  13624  slotsdifunifndx  13635  bl2in  15553  hoverb  15798  ivthdichlem  15801  reeff1o  15923  cosz12  15931  sin0pilem1  15932  sin0pilem2  15933  pilem3  15934  pipos  15939  sinhalfpilem  15942  sincosq1lem  15976  sincosq4sgn  15980  sinq12gt0  15981  cosq23lt0  15984  coseq00topi  15986  coseq0negpitopi  15987  tangtx  15989  sincos4thpi  15991  tan4thpi  15992  sincos6thpi  15993  cosordlem  16000  cosq34lt1  16001  cos02pilt1  16002  cos0pilt1  16003  logdivlt  16046  2logb9irr  16126  2logb3irr  16128  2logb9irrALT  16129  sqrt2cxp2logb9e3  16130  2logb9irrap  16132  log2tlbndlog2  16139  log2ublem2  16141  log2ublog2  16143  pellexlem2  16149  ppiqfi  16158  ppidif  16175  ppiqeq0  16182  ppiqub  16194  mersenne  16195  perfectlem1  16197  perfectlem2  16198  bcmono  16202  bclbnd  16205  bpos1lem  16207  bposlem1  16209  bposlem2  16210  bposlem3  16211  bposlem4  16212  bposlem5  16213  lgslem1  16217  lgsdirprm  16251  gausslemma2dlem0c  16268  gausslemma2dlem1a  16275  gausslemma2dlem2  16279  gausslemma2dlem3  16280  gausslemma2dlem4  16281  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisen  16291  lgsquadlem1  16294  lgsquadlem2  16295  2lgslem1a1  16303  2lgslem1a2  16304  2lgslem1c  16307  2lgslem4  16320  usgrexmpldifpr  16588  clwwlkext2edg  16761  konigsbergiedgwen  16823  konigsberglem1  16827  konigsberglem2  16828  konigsberglem3  16829  konigsberg  16832  ex-fl  16837  taupi  17221