Theorem 2re 9384

Description: The number 2 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
2re	|- 2 e. RR

Proof of Theorem 2re

Step	Hyp	Ref	Expression
1		df-2 9373	. 2 |- 2 = ( 1 + 1 )
2		1re 8332	. . 3 |- 1 e. RR
3	2, 2	readdcli 8346	. 2 |- ( 1 + 1 ) e. RR
4	1, 3	eqeltri 2311	1 |- 2 e. RR

This proof depends on syntax axioms:   e. wcel 2209  (class class class)co 6088   RRcr 8185   1c1 8187   + caddc 8189   2c2 9365

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 8280  ax-addrcl 8283

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

This theorem is used by:  2cn  9385  3re  9388  2ne0  9406  2ap0  9407  3pos  9408  2lt3  9487  1lt3  9488  2lt4  9490  1lt4  9491  2lt5  9494  2lt6  9499  1lt6  9500  2lt7  9505  1lt7  9506  2lt8  9512  1lt8  9513  2lt9  9520  1lt9  9521  1ap2  9524  1le2  9525  2rene0  9527  halfre  9530  halfgt0  9532  halflt1  9534  rehalfcl  9544  halfpos2  9547  halfnneg2  9549  addltmul  9554  nominpos  9555  avglt1  9556  avglt2  9557  div4p1lem1div2  9571  nn0lele2xi  9626  nn0ge2m1nn  9637  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  15662  hoverb  15907  ivthdichlem  15910  reeff1o  16032  cosz12  16040  sin0pilem1  16041  sin0pilem2  16042  pilem3  16043  pipos  16048  sinhalfpilem  16051  sincosq1lem  16085  sincosq4sgn  16089  sinq12gt0  16090  cosq23lt0  16093  coseq00topi  16095  coseq0negpitopi  16096  tangtx  16098  sincos4thpi  16100  tan4thpi  16101  sincos6thpi  16102  sineq0re  16109  cosordlem  16110  cosq34lt1  16111  cos02pilt1  16112  cos0pilt1  16113  logdivlt  16157  2logb9irr  16240  2logb3irr  16242  2logb9irrALT  16243  sqrt2cxp2logb9e3  16244  2logb9irrap  16246  log2tlbndlog2  16253  log2ublem2  16255  log2ublog2  16257  pellexlem2  16263  ppiqfi  16275  chtdif  16297  ppidif  16302  chtqrpcl  16312  ppiqeq0  16313  ppiqub  16326  chtublem  16328  chtqub  16329  mersenne  16330  perfectlem1  16332  perfectlem2  16333  bcmono  16337  bclbnd  16340  bpos1lem  16342  bposlem1  16344  bposlem2  16345  bposlem3  16346  bposlem4  16347  bposlem5  16348  bposlem6  16349  bposlem7  16350  bposlem8  16351  bposlem9  16352  lgslem1  16357  lgsdirprm  16391  gausslemma2dlem0c  16408  gausslemma2dlem1a  16415  gausslemma2dlem2  16419  gausslemma2dlem3  16420  gausslemma2dlem4  16421  lgseisenlem1  16427  lgseisenlem2  16428  lgseisenlem3  16429  lgseisen  16431  lgsquadlem1  16434  lgsquadlem2  16435  2lgslem1a1  16443  2lgslem1a2  16444  2lgslem1c  16447  2lgslem4  16460  usgrexmpldifpr  16728  clwwlkext2edg  16901  konigsbergiedgwen  16963  konigsberglem1  16967  konigsberglem2  16968  konigsberglem3  16969  konigsberg  16972  ex-fl  16977  taupi  17363