Theorem 2re 9375

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 9364	. 2 |- 2 = ( 1 + 1 )
2		1re 8325	. . 3 |- 1 e. RR
3	2, 2	readdcli 8339	. 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 6085   RRcr 8178   1c1 8180   + caddc 8182   2c2 9356

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 8273  ax-addrcl 8276

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

This theorem is used by:  2cn  9376  3re  9379  2ne0  9397  2ap0  9398  3pos  9399  2lt3  9477  1lt3  9478  2lt4  9480  1lt4  9481  2lt5  9484  2lt6  9489  1lt6  9490  2lt7  9495  1lt7  9496  2lt8  9502  1lt8  9503  2lt9  9510  1lt9  9511  1ap2  9514  1le2  9515  2rene0  9517  halfre  9520  halfgt0  9522  halflt1  9524  rehalfcl  9534  halfpos2  9537  halfnneg2  9539  addltmul  9544  nominpos  9545  avglt1  9546  avglt2  9547  div4p1lem1div2  9561  nn0lele2xi  9616  nn0ge2m1nn  9629  halfnz  9744  3halfnz  9745  2lt10  9916  1lt10  9917  uzuzle23  9964  uzuzle24  9965  eluz4eluz2  9970  uz3m2nn  9975  2rp  10061  xleaddadd  10291  fztpval  10492  fz0to4untppr  10533  fzo0to42pr  10640  qbtwnrelemcalc  10692  qbtwnre  10693  2tnp1ge0ge0  10738  flhalf  10739  fldiv4p1lem1div2  10742  mulp1mod1  10804  expubnd  11035  nn0opthlem2d  11161  faclbnd2  11182  4bc2eq6  11215  hashtpglem  11300  wrdlenge2n0  11342  sq01  11662  cvg1nlemres  11753  resqrexlemover  11778  resqrexlemga  11791  sqrt4  11815  sqrt2gt1lt2  11817  abstri  11872  amgm2  11886  maxabslemlub  11975  maxltsup  11986  bdtrilem  12007  efcllemp  12427  efcllem  12428  ege2le3  12440  ef01bndlem  12525  cos01bnd  12527  cos2bnd  12529  cos01gt0  12532  sin02gt0  12533  sincos2sgn  12535  sin4lt0  12536  cos12dec  12537  eirraplem  12546  egt2lt3  12549  epos  12550  ene1  12554  eap1  12555  oexpneg  12646  oddge22np1  12650  evennn02n  12651  evennn2n  12652  nn0ehalf  12672  nno  12675  nn0o  12676  nn0oddm1d2  12678  nnoddm1d2  12679  flodddiv4t2lthalf  12708  bitsp1o  12722  bitsfzolem  12723  bitsfzo  12724  bitsfi  12726  6gcd4e2  12774  ncoprmgcdne1b  12869  prmdc  12910  3lcm2e6  12940  sqrt2irrlem  12941  sqrt2re  12943  sqrt2irraplemnn  12959  sqrt2irrap  12960  4sqlem11  13182  4sqlem12  13183  2expltfac  13220  ballotfilem2  13230  plusgndxnmulrndx  13489  starvndxnplusgndx  13499  scandxnplusgndx  13511  vscandxnplusgndx  13516  ipndxnplusgndx  13529  tsetndxnplusgndx  13548  plendxnplusgndx  13562  dsndxnplusgndx  13577  slotsdifunifndx  13588  bl2in  15506  hoverb  15751  ivthdichlem  15754  reeff1o  15876  cosz12  15884  sin0pilem1  15885  sin0pilem2  15886  pilem3  15887  pipos  15892  sinhalfpilem  15895  sincosq1lem  15929  sincosq4sgn  15933  sinq12gt0  15934  cosq23lt0  15937  coseq00topi  15939  coseq0negpitopi  15940  tangtx  15942  sincos4thpi  15944  tan4thpi  15945  sincos6thpi  15946  cosordlem  15953  cosq34lt1  15954  cos02pilt1  15955  cos0pilt1  15956  logdivlt  15999  2logb9irr  16079  2logb3irr  16081  2logb9irrALT  16082  sqrt2cxp2logb9e3  16083  2logb9irrap  16085  log2tlbndlog2  16088  log2ublem2  16090  log2ublog2  16092  pellexlem2  16098  mersenne  16117  perfectlem1  16119  perfectlem2  16120  bcmono  16124  bclbnd  16127  lgslem1  16131  lgsdirprm  16165  gausslemma2dlem0c  16182  gausslemma2dlem1a  16189  gausslemma2dlem2  16193  gausslemma2dlem3  16194  gausslemma2dlem4  16195  lgseisenlem1  16201  lgseisenlem2  16202  lgseisenlem3  16203  lgseisen  16205  lgsquadlem1  16208  lgsquadlem2  16209  2lgslem1a1  16217  2lgslem1a2  16218  2lgslem1c  16221  2lgslem4  16234  usgrexmpldifpr  16502  clwwlkext2edg  16675  konigsbergiedgwen  16737  konigsberglem1  16741  konigsberglem2  16742  konigsberglem3  16743  konigsberg  16746  ex-fl  16751  taupi  17135