Theorem 2re 9383

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

This proof depends on syntax axioms:   ∈ wcel 2209  (class class class)co 6088  ℝcr 8184  1c1 8186   + caddc 8188  2c2 9364

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 8279  ax-addrcl 8282

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

This theorem is used by:  2cn  9384  3re  9387  2ne0  9405  2ap0  9406  3pos  9407  2lt3  9486  1lt3  9487  2lt4  9489  1lt4  9490  2lt5  9493  2lt6  9498  1lt6  9499  2lt7  9504  1lt7  9505  2lt8  9511  1lt8  9512  2lt9  9519  1lt9  9520  1ap2  9523  1le2  9524  2rene0  9526  halfre  9529  halfgt0  9531  halflt1  9533  rehalfcl  9543  halfpos2  9546  halfnneg2  9548  addltmul  9553  nominpos  9554  avglt1  9555  avglt2  9556  div4p1lem1div2  9570  nn0lele2xi  9625  nn0ge2m1nn  9638  halfnz  9753  3halfnz  9754  2lt10  9930  1lt10  9931  uzuzle23  9978  uzuzle24  9979  eluz4eluz2  9984  uz3m2nn  9989  2rp  10076  xleaddadd  10306  fztpval  10507  fz0to4untppr  10548  fzo0to42pr  10655  qbtwnrelemcalc  10707  qbtwnre  10708  2tnp1ge0ge0  10757  flhalf  10758  fldiv4p1lem1div2  10761  mulp1mod1  10823  expubnd  11054  nn0opthlem2d  11181  faclbnd2  11202  4bc2eq6  11235  hashtpglem  11320  wrdlenge2n0  11362  sq01  11682  cvg1nlemres  11773  resqrexlemover  11798  resqrexlemga  11811  sqrt4  11835  sqrt2gt1lt2  11837  abstri  11893  amgm2  11907  maxabslemlub  11996  maxltsup  12007  bdtrilem  12030  efcllemp  12450  efcllem  12451  ege2le3  12463  ef01bndlem  12548  cos01bnd  12550  cos2bnd  12552  cos01gt0  12555  sin02gt0  12556  sincos2sgn  12558  sin4lt0  12559  cos12dec  12560  eirraplem  12569  egt2lt3  12572  epos  12573  ene1  12577  eap1  12578  oexpneg  12669  oddge22np1  12673  evennn02n  12674  evennn2n  12675  nn0ehalf  12695  nno  12698  nn0o  12699  nn0oddm1d2  12701  nnoddm1d2  12702  flodddiv4t2lthalf  12731  bitsp1o  12745  bitsfzolem  12746  bitsfzo  12747  bitsfi  12749  6gcd4e2  12797  ncoprmgcdne1b  12892  prmdc  12933  3lcm2e6  12964  sqrt2irrlem  12965  sqrt2re  12967  sqrt2irraplemnn  12984  sqrt2irrap  12985  4sqlem11  13209  4sqlem12  13210  2expltfac  13248  ballotfilem2  13286  plusgndxnmulrndx  13546  starvndxnplusgndx  13556  scandxnplusgndx  13568  vscandxnplusgndx  13573  ipndxnplusgndx  13586  tsetndxnplusgndx  13605  plendxnplusgndx  13619  dsndxnplusgndx  13634  slotsdifunifndx  13645  bl2in  15629  hoverb  15874  ivthdichlem  15877  reeff1o  15999  cosz12  16007  sin0pilem1  16008  sin0pilem2  16009  pilem3  16010  pipos  16015  sinhalfpilem  16018  sincosq1lem  16052  sincosq4sgn  16056  sinq12gt0  16057  cosq23lt0  16060  coseq00topi  16062  coseq0negpitopi  16063  tangtx  16065  sincos4thpi  16067  tan4thpi  16068  sincos6thpi  16069  sineq0re  16076  cosordlem  16077  cosq34lt1  16078  cos02pilt1  16079  cos0pilt1  16080  logdivlt  16124  2logb9irr  16207  2logb3irr  16209  2logb9irrALT  16210  sqrt2cxp2logb9e3  16211  2logb9irrap  16213  log2tlbndlog2  16220  log2ublem2  16222  log2ublog2  16224  pellexlem2  16230  ppiqfi  16242  chtdif  16264  ppidif  16269  chtqrpcl  16279  ppiqeq0  16280  ppiqub  16293  chtublem  16295  chtqub  16296  mersenne  16297  perfectlem1  16299  perfectlem2  16300  bcmono  16304  bclbnd  16307  bpos1lem  16309  bposlem1  16311  bposlem2  16312  bposlem3  16313  bposlem4  16314  bposlem5  16315  bposlem6  16316  bposlem7  16317  bposlem8  16318  bposlem9  16319  lgslem1  16324  lgsdirprm  16358  gausslemma2dlem0c  16375  gausslemma2dlem1a  16382  gausslemma2dlem2  16386  gausslemma2dlem3  16387  gausslemma2dlem4  16388  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem3  16396  lgseisen  16398  lgsquadlem1  16401  lgsquadlem2  16402  2lgslem1a1  16410  2lgslem1a2  16411  2lgslem1c  16414  2lgslem4  16427  usgrexmpldifpr  16695  clwwlkext2edg  16868  konigsbergiedgwen  16930  konigsberglem1  16934  konigsberglem2  16935  konigsberglem3  16936  konigsberg  16939  ex-fl  16944  taupi  17330