Theorem 3re 10711

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

Assertion

Ref	Expression
3re	|- 3 e. RR

Proof of Theorem 3re

Step	Hyp	Ref	Expression
1		df-3 10697	. 2 |- 3 = ( 2 + 1 )
2		2re 10707	. . 3 |- 2 e. RR
3		1re 9668	. . 3 |- 1 e. RR
4	2, 3	readdcli 9682	. 2 |- ( 2 + 1 ) e. RR
5	1, 4	eqeltri 2536	1 |- 3 e. RR

Syntax hints:   e. wcel 1898  (class class class)co 6315   RRcr 9564   1c1 9566   + caddc 9568   2c2 10687   3c3 10688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-i2m1 9633  ax-1ne0 9634  ax-rrecex 9637  ax-cnre 9638

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-iota 5565  df-fv 5609  df-ov 6318  df-2 10696  df-3 10697

This theorem is referenced by:  3cn  10712  4re  10714  3ne0  10732  4pos  10733  1lt3  10807  3lt4  10808  2lt4  10809  3lt5  10812  3lt6  10817  2lt6  10818  3lt7  10823  2lt7  10824  3lt8  10830  2lt8  10831  3lt9  10838  2lt9  10839  3lt10  10847  2lt10  10848  1le3  10855  uzuzle23  11228  uz3m2nn  11230  nn01to3  11286  expnass  12412  hashtpg  12674  sqrlem7  13361  sqrt9  13386  caucvgrlem  13785  caucvgrlemOLD  13786  caurcvgr  13787  caurcvgrOLD  13788  bpoly4  14161  ef01bndlem  14287  sin01bnd  14288  cos2bnd  14291  sin01gt0  14293  cos01gt0  14294  egt2lt3  14307  rpnnen2lem3  14318  rpnnen2lem4  14319  rpnnen2lem9  14324  matsca  19489  matvsca  19490  vitalilem4  22618  dveflem  22980  sincosq3sgn  23504  sincosq4sgn  23505  tangtx  23509  sincos6thpi  23519  pige3  23521  ang180lem2  23788  1cubrlem  23816  log2cnv  23919  log2tlbnd  23920  log2ub  23924  cxploglim2  23953  basellem5  24060  basellem9  24064  cht3  24149  ppiublem1  24179  ppiub  24181  chtub  24189  bposlem2  24262  bposlem3  24263  bposlem4  24264  bposlem5  24265  bposlem6  24266  bposlem8  24268  bposlem9  24269  lgsdir2lem1  24300  chebbnd1lem2  24357  chebbnd1lem3  24358  chebbnd1  24359  chto1ub  24363  dchrvmasumlem2  24385  dchrvmasumlema  24387  dchrvmasumiflem1  24388  mulog2sumlem2  24422  pntibndlem1  24476  pntibndlem2  24478  pntlemb  24484  pntlemk  24493  pntlemo  24494  istrkg3ld  24558  axlowdimlem8  25028  axlowdimlem9  25029  axlowdimlem16  25036  axlowdimlem17  25037  axlowdim  25040  usgraexmplvtxlem  25171  usgraex3elv  25175  constr3pthlem3  25434  4cycl4v4e  25443  4cycl4dv4e  25445  konigsberg  25764  extwwlkfablem2  25855  numclwlk1lem2f1  25871  frgraogt3nreg  25897  friendshipgt3  25898  friendship  25899  ex-dif  25922  ex-in  25924  ex-1st  25943  ex-2nd  25944  ex-fl  25946  stadd3i  27950  resvmulr  28647  problem3  30348  problem5  30350  pigt3  31983  poimirlem9  31994  itg2addnclem2  32039  heiborlem5  32192  heiborlem6  32193  heiborlem7  32194  heiborlem8  32195  jm2.23  35896  jm2.20nn  35897  3rp  37535  lt4addmuld  37562  stoweidlem11  37909  stoweidlem13  37911  stoweidlem26  37924  stoweidlem34  37933  stoweidlem42  37941  stoweidlem59  37958  stoweidlem62  37961  stoweidlem62OLD  37962  stoweid  37963  wallispilem4  37968  fourierdlem87  38095  gbegt5  38900  gboage9  38903  bgoldbwt  38916  bgoldbst  38917  sgoldbalt  38920  nnsum3primes4  38921  nnsum4primes4  38922  nnsum3primesprm  38923  nnsum4primesprm  38924  nnsum3primesgbe  38925  nnsum4primesgbe  38926  nnsum3primesle9  38927  nnsum4primesle9  38928  evengpop3  38931  evengpoap3  38932  nnsum4primeseven  38933  nnsum4primesevenALTV  38934  wtgoldbnnsum4prm  38935  bgoldbnnsum3prm  38937  upgr4cycl4dv4e  39926  pgrpgt2nabl  40424  3halfnz  40590