Theorem 3re 11983

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 11967	. 2 ⊢ 3 = (2 + 1)
2		2re 11977	. . 3 ⊢ 2 ∈ ℝ
3		1re 10906	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10921	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2835	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7255  ℝcr 10801  1c1 10803   + caddc 10805  2c2 11958  3c3 11959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-i2m1 10870  ax-1ne0 10871  ax-rrecex 10874  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-2 11966  df-3 11967

This theorem is referenced by:  4re  11987  3ne0  12009  4pos  12010  1lt3  12076  3lt4  12077  2lt4  12078  3lt5  12081  3lt6  12086  2lt6  12087  3lt7  12092  2lt7  12093  3lt8  12099  2lt8  12100  3lt9  12107  2lt9  12108  1le3  12115  3halfnz  12329  3lt10  12503  2lt10  12504  uzuzle23  12558  uz3m2nn  12560  nn01to3  12610  3rp  12665  fz0to4untppr  13288  expnass  13852  hashtpg  14127  sqrlem7  14888  sqrt9  14913  caucvgrlem  15312  bpoly4  15697  ef01bndlem  15821  sin01bnd  15822  cos2bnd  15825  sin01gt0  15827  cos01gt0  15828  egt2lt3  15843  rpnnen2lem3  15853  rpnnen2lem4  15854  rpnnen2lem9  15859  flodddiv4  16050  ge2nprmge4  16334  starvndxnmulrndx  16942  scandxnmulrndx  16954  vscandxnmulrndx  16959  ipndxnmulrndx  16970  tsetndxnmulrndx  16993  plendxnmulrndx  17006  dsndxnmulrndx  17022  cnfldfun  20522  matsca  21472  matvsca  21473  vitalilem4  24680  dveflem  25048  sincosq3sgn  25562  sincosq4sgn  25563  tangtx  25567  sincos6thpi  25577  pigt3  25579  pige3  25580  pige3ALT  25581  ang180lem2  25865  1cubrlem  25896  log2cnv  25999  log2tlbnd  26000  log2ub  26004  cxploglim2  26033  basellem5  26139  basellem9  26143  ppiublem1  26255  ppiub  26257  chtub  26265  bposlem2  26338  bposlem3  26339  bposlem4  26340  bposlem5  26341  bposlem6  26342  bposlem8  26344  bposlem9  26345  lgsdir2lem1  26378  2lgslem3  26457  chebbnd1lem2  26523  chebbnd1lem3  26524  chebbnd1  26525  chto1ub  26529  dchrvmasumlem2  26551  dchrvmasumlema  26553  dchrvmasumiflem1  26554  mulog2sumlem2  26588  pntibndlem1  26642  pntibndlem2  26644  pntlemb  26650  pntlemk  26659  pntlemo  26660  istrkg3ld  26726  tgcgr4  26796  axlowdimlem16  27228  axlowdimlem17  27229  axlowdim  27232  usgrexmplef  27529  upgr4cycl4dv4e  28450  konigsbergiedgw  28513  konigsberglem1  28517  konigsberglem2  28518  konigsberglem3  28519  konigsberglem4  28520  frgrogt3nreg  28662  friendshipgt3  28663  friendship  28664  ex-dif  28688  ex-in  28690  ex-fl  28712  ex-ceil  28713  ex-gcd  28722  threehalves  31091  resvmulrOLD  31441  prodfzo03  32483  hgt750lem  32531  hgt750lem2  32532  hgt750leme  32538  cusgracyclt3v  33018  problem3  33525  problem5  33527  poimirlem9  35713  itg2addnclem2  35756  heiborlem5  35900  heiborlem6  35901  heiborlem7  35902  heiborlem8  35903  3lexlogpow5ineq2  39991  3lexlogpow5ineq4  39992  3lexlogpow5ineq3  39993  3lexlogpow2ineq1  39994  3lexlogpow2ineq2  39995  3lexlogpow5ineq5  39996  aks4d1lem1  39998  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1p6  40009  aks4d1p1p5  40011  aks4d1p1  40012  aks4d1p2  40013  aks4d1p3  40014  aks4d1p5  40016  aks4d1p6  40017  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8  40023  aks4d1p9  40024  2np3bcnp1  40028  2ap1caineq  40029  2xp3dxp2ge1d  40090  acos1half  40098  sn-0ne2  40310  3cubeslem2  40423  3cubeslem4  40427  jm2.23  40734  jm2.20nn  40735  mnringscadOLD  41730  mnringvscadOLD  41732  lt4addmuld  42735  stoweidlem11  43442  stoweidlem13  43444  stoweidlem26  43457  stoweidlem34  43465  stoweidlem42  43473  stoweidlem59  43490  stoweidlem62  43493  stoweid  43494  wallispilem4  43499  fourierdlem87  43624  smfmullem4  44215  fmtnoge3  44870  fmtnoprmfac2lem1  44906  31prm  44937  9fppr8  45077  fpprel2  45081  nfermltl8rev  45082  nfermltl2rev  45083  gbegt5  45101  gboge9  45104  sbgoldbwt  45117  sbgoldbst  45118  sbgoldbalt  45121  sbgoldbo  45127  nnsum3primes4  45128  nnsum4primes4  45129  nnsum4primesprm  45131  nnsum3primesgbe  45132  nnsum4primesgbe  45133  nnsum3primesle9  45134  nnsum4primesle9  45135  evengpop3  45138  evengpoap3  45139  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  wtgoldbnnsum4prm  45142  bgoldbnnsum3prm  45144  pgrpgt2nabl  45590  ackval42  45930  sepfsepc  46109