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  9639  halfnz  9754  3halfnz  9755  2lt10  9931  1lt10  9932  uzuzle23  9979  uzuzle24  9980  eluz4eluz2  9985  uz3m2nn  9990  2rp  10077  xleaddadd  10307  fztpval  10508  fz0to4untppr  10549  fzo0to42pr  10656  qbtwnrelemcalc  10708  qbtwnre  10709  2tnp1ge0ge0  10758  flhalf  10759  fldiv4p1lem1div2  10762  mulp1mod1  10824  expubnd  11055  nn0opthlem2d  11182  faclbnd2  11203  4bc2eq6  11236  hashtpglem  11321  wrdlenge2n0  11363  sq01  11683  cvg1nlemres  11774  resqrexlemover  11799  resqrexlemga  11812  sqrt4  11836  sqrt2gt1lt2  11838  abstri  11894  amgm2  11908  maxabslemlub  11997  maxltsup  12008  bdtrilem  12031  efcllemp  12451  efcllem  12452  ege2le3  12464  ef01bndlem  12549  cos01bnd  12551  cos2bnd  12553  cos01gt0  12556  sin02gt0  12557  sincos2sgn  12559  sin4lt0  12560  cos12dec  12561  eirraplem  12570  egt2lt3  12573  epos  12574  ene1  12578  eap1  12579  oexpneg  12670  oddge22np1  12674  evennn02n  12675  evennn2n  12676  nn0ehalf  12696  nno  12699  nn0o  12700  nn0oddm1d2  12702  nnoddm1d2  12703  flodddiv4t2lthalf  12732  bitsp1o  12746  bitsfzolem  12747  bitsfzo  12748  bitsfi  12750  6gcd4e2  12798  ncoprmgcdne1b  12893  prmdc  12934  3lcm2e6  12965  sqrt2irrlem  12966  sqrt2re  12968  sqrt2irraplemnn  12985  sqrt2irrap  12986  4sqlem11  13210  4sqlem12  13211  2expltfac  13249  ballotfilem2  13287  plusgndxnmulrndx  13547  starvndxnplusgndx  13557  scandxnplusgndx  13569  vscandxnplusgndx  13574  ipndxnplusgndx  13587  tsetndxnplusgndx  13606  plendxnplusgndx  13620  dsndxnplusgndx  13635  slotsdifunifndx  13646  bl2in  15641  hoverb  15886  ivthdichlem  15889  reeff1o  16011  cosz12  16019  sin0pilem1  16020  sin0pilem2  16021  pilem3  16022  pipos  16027  sinhalfpilem  16030  sincosq1lem  16064  sincosq4sgn  16068  sinq12gt0  16069  cosq23lt0  16072  coseq00topi  16074  coseq0negpitopi  16075  tangtx  16077  sincos4thpi  16079  tan4thpi  16080  sincos6thpi  16081  sineq0re  16088  cosordlem  16089  cosq34lt1  16090  cos02pilt1  16091  cos0pilt1  16092  logdivlt  16136  2logb9irr  16219  2logb3irr  16221  2logb9irrALT  16222  sqrt2cxp2logb9e3  16223  2logb9irrap  16225  log2tlbndlog2  16232  log2ublem2  16234  log2ublog2  16236  pellexlem2  16242  ppiqfi  16254  chtdif  16276  ppidif  16281  chtqrpcl  16291  ppiqeq0  16292  ppiqub  16305  chtublem  16307  chtqub  16308  mersenne  16309  perfectlem1  16311  perfectlem2  16312  bcmono  16316  bclbnd  16319  bpos1lem  16321  bposlem1  16323  bposlem2  16324  bposlem3  16325  bposlem4  16326  bposlem5  16327  bposlem6  16328  bposlem7  16329  bposlem8  16330  bposlem9  16331  lgslem1  16336  lgsdirprm  16370  gausslemma2dlem0c  16387  gausslemma2dlem1a  16394  gausslemma2dlem2  16398  gausslemma2dlem3  16399  gausslemma2dlem4  16400  lgseisenlem1  16406  lgseisenlem2  16407  lgseisenlem3  16408  lgseisen  16410  lgsquadlem1  16413  lgsquadlem2  16414  2lgslem1a1  16422  2lgslem1a2  16423  2lgslem1c  16426  2lgslem4  16439  usgrexmpldifpr  16707  clwwlkext2edg  16880  konigsbergiedgwen  16942  konigsberglem1  16946  konigsberglem2  16947  konigsberglem3  16948  konigsberg  16951  ex-fl  16956  taupi  17342