Theorem 2re 9213

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 9202	. 2 ⊢ 2 = (1 + 1)
2		1re 8178	. . 3 ⊢ 1 ∈ ℝ
3	2, 2	readdcli 8192	. 2 ⊢ (1 + 1) ∈ ℝ
4	1, 3	eqeltri 2304	1 ⊢ 2 ∈ ℝ

Syntax hints:   ∈ wcel 2202  (class class class)co 6018  ℝcr 8031  1c1 8033   + caddc 8035  2c2 9194

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 2213  ax-1re 8126  ax-addrcl 8129

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227  df-2 9202

This theorem is referenced by:  2cn  9214  3re  9217  2ne0  9235  2ap0  9236  3pos  9237  2lt3  9314  1lt3  9315  2lt4  9317  1lt4  9318  2lt5  9321  2lt6  9326  1lt6  9327  2lt7  9332  1lt7  9333  2lt8  9339  1lt8  9340  2lt9  9347  1lt9  9348  1ap2  9351  1le2  9352  2rene0  9354  halfre  9357  halfgt0  9359  halflt1  9361  rehalfcl  9371  halfpos2  9374  halfnneg2  9376  addltmul  9381  nominpos  9382  avglt1  9383  avglt2  9384  div4p1lem1div2  9398  nn0lele2xi  9453  nn0ge2m1nn  9462  halfnz  9576  3halfnz  9577  2lt10  9748  1lt10  9749  uzuzle23  9796  uzuzle24  9797  eluz4eluz2  9802  uz3m2nn  9807  2rp  9893  xleaddadd  10122  fztpval  10318  fz0to4untppr  10359  fzo0to42pr  10466  qbtwnrelemcalc  10516  qbtwnre  10517  2tnp1ge0ge0  10562  flhalf  10563  fldiv4p1lem1div2  10566  mulp1mod1  10628  expubnd  10859  nn0opthlem2d  10984  faclbnd2  11005  4bc2eq6  11037  hashtpglem  11111  wrdlenge2n0  11153  cvg1nlemres  11563  resqrexlemover  11588  resqrexlemga  11601  sqrt4  11625  sqrt2gt1lt2  11627  abstri  11682  amgm2  11696  maxabslemlub  11785  maxltsup  11796  bdtrilem  11817  efcllemp  12237  efcllem  12238  ege2le3  12250  ef01bndlem  12335  cos01bnd  12337  cos2bnd  12339  cos01gt0  12342  sin02gt0  12343  sincos2sgn  12345  sin4lt0  12346  cos12dec  12347  eirraplem  12356  egt2lt3  12359  epos  12360  ene1  12364  eap1  12365  oexpneg  12456  oddge22np1  12460  evennn02n  12461  evennn2n  12462  nn0ehalf  12482  nno  12485  nn0o  12486  nn0oddm1d2  12488  nnoddm1d2  12489  flodddiv4t2lthalf  12518  bitsp1o  12532  bitsfzolem  12533  bitsfzo  12534  bitsfi  12536  6gcd4e2  12584  ncoprmgcdne1b  12679  prmdc  12720  3lcm2e6  12750  sqrt2irrlem  12751  sqrt2re  12753  sqrt2irraplemnn  12769  sqrt2irrap  12770  4sqlem11  12992  4sqlem12  12993  2expltfac  13030  plusgndxnmulrndx  13234  starvndxnplusgndx  13244  scandxnplusgndx  13256  vscandxnplusgndx  13261  ipndxnplusgndx  13274  tsetndxnplusgndx  13293  plendxnplusgndx  13307  dsndxnplusgndx  13322  slotsdifunifndx  13333  bl2in  15146  hoverb  15391  ivthdichlem  15394  reeff1o  15516  cosz12  15523  sin0pilem1  15524  sin0pilem2  15525  pilem3  15526  pipos  15531  sinhalfpilem  15534  sincosq1lem  15568  sincosq4sgn  15572  sinq12gt0  15573  cosq23lt0  15576  coseq00topi  15578  coseq0negpitopi  15579  tangtx  15581  sincos4thpi  15583  tan4thpi  15584  sincos6thpi  15585  cosordlem  15592  cosq34lt1  15593  cos02pilt1  15594  cos0pilt1  15595  2logb9irr  15714  2logb3irr  15716  2logb9irrALT  15717  sqrt2cxp2logb9e3  15718  2logb9irrap  15720  mersenne  15740  perfectlem1  15742  perfectlem2  15743  lgslem1  15748  lgsdirprm  15782  gausslemma2dlem0c  15799  gausslemma2dlem1a  15806  gausslemma2dlem2  15810  gausslemma2dlem3  15811  gausslemma2dlem4  15812  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisen  15822  lgsquadlem1  15825  lgsquadlem2  15826  2lgslem1a1  15834  2lgslem1a2  15835  2lgslem1c  15838  2lgslem4  15851  usgrexmpldifpr  16119  clwwlkext2edg  16292  konigsbergiedgwen  16354  konigsberglem1  16358  konigsberglem2  16359  konigsberglem3  16360  konigsberg  16363  ex-fl  16368  taupi  16729