Theorem 2re 9212

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

Syntax hints:   ∈ wcel 2202  (class class class)co 6017  ℝcr 8030  1c1 8032   + caddc 8034  2c2 9193

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 8125  ax-addrcl 8128

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

This theorem is referenced by:  2cn  9213  3re  9216  2ne0  9234  2ap0  9235  3pos  9236  2lt3  9313  1lt3  9314  2lt4  9316  1lt4  9317  2lt5  9320  2lt6  9325  1lt6  9326  2lt7  9331  1lt7  9332  2lt8  9338  1lt8  9339  2lt9  9346  1lt9  9347  1ap2  9350  1le2  9351  2rene0  9353  halfre  9356  halfgt0  9358  halflt1  9360  rehalfcl  9370  halfpos2  9373  halfnneg2  9375  addltmul  9380  nominpos  9381  avglt1  9382  avglt2  9383  div4p1lem1div2  9397  nn0lele2xi  9452  nn0ge2m1nn  9461  halfnz  9575  3halfnz  9576  2lt10  9747  1lt10  9748  uzuzle23  9795  uzuzle24  9796  eluz4eluz2  9801  uz3m2nn  9806  2rp  9892  xleaddadd  10121  fztpval  10317  fz0to4untppr  10358  fzo0to42pr  10464  qbtwnrelemcalc  10514  qbtwnre  10515  2tnp1ge0ge0  10560  flhalf  10561  fldiv4p1lem1div2  10564  mulp1mod1  10626  expubnd  10857  nn0opthlem2d  10982  faclbnd2  11003  4bc2eq6  11035  wrdlenge2n0  11148  cvg1nlemres  11545  resqrexlemover  11570  resqrexlemga  11583  sqrt4  11607  sqrt2gt1lt2  11609  abstri  11664  amgm2  11678  maxabslemlub  11767  maxltsup  11778  bdtrilem  11799  efcllemp  12218  efcllem  12219  ege2le3  12231  ef01bndlem  12316  cos01bnd  12318  cos2bnd  12320  cos01gt0  12323  sin02gt0  12324  sincos2sgn  12326  sin4lt0  12327  cos12dec  12328  eirraplem  12337  egt2lt3  12340  epos  12341  ene1  12345  eap1  12346  oexpneg  12437  oddge22np1  12441  evennn02n  12442  evennn2n  12443  nn0ehalf  12463  nno  12466  nn0o  12467  nn0oddm1d2  12469  nnoddm1d2  12470  flodddiv4t2lthalf  12499  bitsp1o  12513  bitsfzolem  12514  bitsfzo  12515  bitsfi  12517  6gcd4e2  12565  ncoprmgcdne1b  12660  prmdc  12701  3lcm2e6  12731  sqrt2irrlem  12732  sqrt2re  12734  sqrt2irraplemnn  12750  sqrt2irrap  12751  4sqlem11  12973  4sqlem12  12974  2expltfac  13011  plusgndxnmulrndx  13215  starvndxnplusgndx  13225  scandxnplusgndx  13237  vscandxnplusgndx  13242  ipndxnplusgndx  13255  tsetndxnplusgndx  13274  plendxnplusgndx  13288  dsndxnplusgndx  13303  slotsdifunifndx  13314  bl2in  15126  hoverb  15371  ivthdichlem  15374  reeff1o  15496  cosz12  15503  sin0pilem1  15504  sin0pilem2  15505  pilem3  15506  pipos  15511  sinhalfpilem  15514  sincosq1lem  15548  sincosq4sgn  15552  sinq12gt0  15553  cosq23lt0  15556  coseq00topi  15558  coseq0negpitopi  15559  tangtx  15561  sincos4thpi  15563  tan4thpi  15564  sincos6thpi  15565  cosordlem  15572  cosq34lt1  15573  cos02pilt1  15574  cos0pilt1  15575  2logb9irr  15694  2logb3irr  15696  2logb9irrALT  15697  sqrt2cxp2logb9e3  15698  2logb9irrap  15700  mersenne  15720  perfectlem1  15722  perfectlem2  15723  lgslem1  15728  lgsdirprm  15762  gausslemma2dlem0c  15779  gausslemma2dlem1a  15786  gausslemma2dlem2  15790  gausslemma2dlem3  15791  gausslemma2dlem4  15792  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisen  15802  lgsquadlem1  15805  lgsquadlem2  15806  2lgslem1a1  15814  2lgslem1a2  15815  2lgslem1c  15818  2lgslem4  15831  usgrexmpldifpr  16099  clwwlkext2edg  16272  ex-fl  16321  taupi  16677