Theorem 3re 11352

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

Assertion

Ref	Expression
3re	⊢ 3 ∈ ℝ

Proof of Theorem 3re

Step	Hyp	Ref	Expression
1		df-3 11336	. 2 ⊢ 3 = (2 + 1)
2		2re 11346	. . 3 ⊢ 2 ∈ ℝ
3		1re 10293	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10309	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2840	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2155  (class class class)co 6842  ℝcr 10188  1c1 10190   + caddc 10192  2c2 11327  3c3 11328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-1cn 10247  ax-icn 10248  ax-addcl 10249  ax-addrcl 10250  ax-mulcl 10251  ax-mulrcl 10252  ax-i2m1 10257  ax-1ne0 10258  ax-rrecex 10261  ax-cnre 10262

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-br 4810  df-iota 6031  df-fv 6076  df-ov 6845  df-2 11335  df-3 11336

This theorem is referenced by:  3cnOLD  11354  4re  11357  3ne0  11385  4pos  11386  1lt3  11451  3lt4  11452  2lt4  11453  3lt5  11456  3lt6  11461  2lt6  11462  3lt7  11467  2lt7  11468  3lt8  11474  2lt8  11475  3lt9  11482  2lt9  11483  1le3  11490  3halfnz  11703  3lt10  11878  2lt10  11879  uzuzle23  11929  uz3m2nn  11931  nn01to3  11982  3rp  12034  fz0to4untppr  12650  expnass  13177  hashtpg  13468  sqrlem7  14276  sqrt9  14301  caucvgrlem  14690  caurcvgr  14691  bpoly4  15074  ef01bndlem  15198  sin01bnd  15199  cos2bnd  15202  sin01gt0  15204  cos01gt0  15205  egt2lt3  15218  rpnnen2lem3  15229  rpnnen2lem4  15230  rpnnen2lem9  15235  flodddiv4  15420  cnfldfun  20031  matsca  20497  matvsca  20498  vitalilem4  23669  dveflem  24033  sincosq3sgn  24544  sincosq4sgn  24545  tangtx  24549  sincos6thpi  24559  pige3  24561  ang180lem2  24831  1cubrlem  24859  log2cnv  24962  log2tlbnd  24963  log2ub  24967  cxploglim2  24996  basellem5  25102  basellem9  25106  cht3  25190  ppiublem1  25218  ppiub  25220  chtub  25228  bposlem2  25301  bposlem3  25302  bposlem4  25303  bposlem5  25304  bposlem6  25305  bposlem8  25307  bposlem9  25308  lgsdir2lem1  25341  2lgslem3  25420  chebbnd1lem2  25450  chebbnd1lem3  25451  chebbnd1  25452  chto1ub  25456  dchrvmasumlem2  25478  dchrvmasumlema  25480  dchrvmasumiflem1  25481  mulog2sumlem2  25515  pntibndlem1  25569  pntibndlem2  25571  pntlemb  25577  pntlemk  25586  pntlemo  25587  istrkg3ld  25651  axlowdimlem8  26120  axlowdimlem9  26121  axlowdimlem16  26128  axlowdimlem17  26129  axlowdim  26132  usgrexmplef  26430  upgr4cycl4dv4e  27421  konigsbergiedgw  27484  konigsberglem1  27488  konigsberglem2  27489  konigsberglem3  27490  konigsberglem4  27491  frgrogt3nreg  27648  friendshipgt3  27649  friendship  27650  ex-dif  27674  ex-in  27676  ex-1st  27695  ex-2nd  27696  ex-fl  27698  ex-ceil  27699  ex-gcd  27708  threehalves  30005  resvmulr  30217  prodfzo03  31064  hgt750lem  31112  hgt750lem2  31113  hgt750leme  31119  problem3  31939  problem5  31941  pigt3  33758  poimirlem9  33774  itg2addnclem2  33817  heiborlem5  33968  heiborlem6  33969  heiborlem7  33970  heiborlem8  33971  jm2.23  38172  jm2.20nn  38173  lt4addmuld  40091  stoweidlem11  40797  stoweidlem13  40799  stoweidlem26  40812  stoweidlem34  40820  stoweidlem42  40828  stoweidlem59  40845  stoweidlem62  40848  stoweid  40849  wallispilem4  40854  fourierdlem87  40979  smfmullem4  41573  fmtnoge3  42050  fmtnoprmfac2lem1  42086  31prm  42120  gbegt5  42257  gboge9  42260  sbgoldbwt  42273  sbgoldbst  42274  sbgoldbalt  42277  sbgoldbo  42283  nnsum3primes4  42284  nnsum4primes4  42285  nnsum4primesprm  42287  nnsum3primesgbe  42288  nnsum4primesgbe  42289  nnsum3primesle9  42290  nnsum4primesle9  42291  evengpop3  42294  evengpoap3  42295  nnsum4primeseven  42296  nnsum4primesevenALTV  42297  wtgoldbnnsum4prm  42298  bgoldbnnsum3prm  42300  pgrpgt2nabl  42748