Theorem 3re 12320

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 12304	. 2 ⊢ 3 = (2 + 1)
2		2re 12314	. . 3 ⊢ 2 ∈ ℝ
3		1re 11235	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11250	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2830	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7405  ℝcr 11128  1c1 11130   + caddc 11132  2c2 12295  3c3 12296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11187  ax-icn 11188  ax-addcl 11189  ax-addrcl 11190  ax-mulcl 11191  ax-mulrcl 11192  ax-i2m1 11197  ax-1ne0 11198  ax-rrecex 11201  ax-cnre 11202

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408  df-2 12303  df-3 12304

This theorem is referenced by:  4re  12324  4pos  12347  1lt3  12413  3lt4  12414  2lt4  12415  3lt5  12418  3lt6  12423  2lt6  12424  3lt7  12429  2lt7  12430  3lt8  12436  2lt8  12437  3lt9  12444  2lt9  12445  1le3  12452  3halfnz  12672  3lt10  12845  2lt10  12846  eluz4eluz3  12900  5eluz3  12901  uzuzle23  12905  uz3m2nn  12907  nn01to3  12957  3rp  13014  fz0to4untppr  13647  fz0to5un2tp  13648  expnass  14226  hashtpg  14503  hash3tpde  14511  01sqrexlem7  15267  sqrt9  15292  caucvgrlem  15689  bpoly4  16075  ef01bndlem  16202  sin01bnd  16203  cos2bnd  16206  sin01gt0  16208  cos01gt0  16209  egt2lt3  16224  rpnnen2lem3  16234  rpnnen2lem4  16235  rpnnen2lem9  16240  flodddiv4  16434  ge2nprmge4  16720  starvndxnmulrndx  17320  scandxnmulrndx  17332  vscandxnmulrndx  17337  ipndxnmulrndx  17348  tsetndxnmulrndx  17372  plendxnmulrndx  17386  dsndxnmulrndx  17405  slotsdifunifndx  17415  vitalilem4  25564  dveflem  25935  sincosq3sgn  26461  sincosq4sgn  26462  tangtx  26466  sincos6thpi  26477  pigt3  26479  pige3  26480  pige3ALT  26481  ang180lem2  26772  1cubrlem  26803  log2cnv  26906  log2tlbnd  26907  log2ub  26911  cxploglim2  26941  basellem5  27047  basellem9  27051  ppiublem1  27165  ppiub  27167  chtub  27175  bposlem2  27248  bposlem3  27249  bposlem4  27250  bposlem5  27251  bposlem6  27252  bposlem8  27254  bposlem9  27255  lgsdir2lem1  27288  2lgslem3  27367  chebbnd1lem2  27433  chebbnd1lem3  27434  chebbnd1  27435  chto1ub  27439  dchrvmasumlem2  27461  dchrvmasumlema  27463  dchrvmasumiflem1  27464  mulog2sumlem2  27498  pntibndlem1  27552  pntibndlem2  27554  pntlemb  27560  pntlemk  27569  pntlemo  27570  istrkg3ld  28440  tgcgr4  28510  axlowdimlem16  28936  axlowdimlem17  28937  axlowdim  28940  usgrexmplef  29238  upgr4cycl4dv4e  30166  konigsbergiedgw  30229  konigsberglem1  30233  konigsberglem2  30234  konigsberglem3  30235  konigsberglem4  30236  frgrogt3nreg  30378  friendshipgt3  30379  friendship  30380  ex-dif  30404  ex-in  30406  ex-fl  30428  ex-ceil  30429  ex-gcd  30438  threehalves  32889  iconstr  33800  2sqr3minply  33814  cos9thpiminplylem3  33818  cos9thpinconstrlem1  33823  prodfzo03  34635  hgt750lem  34683  hgt750lem2  34684  hgt750leme  34690  cusgracyclt3v  35178  problem3  35689  problem5  35691  poimirlem9  37653  itg2addnclem2  37696  heiborlem5  37839  heiborlem6  37840  heiborlem7  37841  heiborlem8  37842  3lexlogpow5ineq2  42068  3lexlogpow5ineq4  42069  3lexlogpow5ineq3  42070  3lexlogpow2ineq1  42071  3lexlogpow2ineq2  42072  3lexlogpow5ineq5  42073  aks4d1lem1  42075  aks4d1p1p3  42082  aks4d1p1p2  42083  aks4d1p1p4  42084  aks4d1p1p6  42086  aks4d1p1p5  42088  aks4d1p1  42089  aks4d1p2  42090  aks4d1p3  42091  aks4d1p5  42093  aks4d1p6  42094  aks4d1p7d1  42095  aks4d1p7  42096  aks4d1p8  42100  aks4d1p9  42101  2np3bcnp1  42157  2ap1caineq  42158  aks6d1c7lem1  42193  aks6d1c7lem2  42194  aks6d1c7  42197  aks5lem6  42205  aks5lem8  42214  2xp3dxp2ge1d  42254  acos1half  42401  sn-0ne2  42449  3cubeslem2  42708  3cubeslem4  42712  jm2.23  43020  jm2.20nn  43021  lt4addmuld  45335  stoweidlem11  46040  stoweidlem13  46042  stoweidlem26  46055  stoweidlem34  46063  stoweidlem42  46071  stoweidlem59  46088  stoweidlem62  46091  stoweid  46092  wallispilem4  46097  fourierdlem87  46222  smfmullem4  46823  fmtnoge3  47544  fmtnoprmfac2lem1  47580  31prm  47611  9fppr8  47751  fpprel2  47755  nfermltl8rev  47756  nfermltl2rev  47757  gbegt5  47775  gboge9  47778  sbgoldbwt  47791  sbgoldbst  47792  sbgoldbalt  47795  sbgoldbo  47801  nnsum3primes4  47802  nnsum4primes4  47803  nnsum4primesprm  47805  nnsum3primesgbe  47806  nnsum4primesgbe  47807  nnsum3primesle9  47808  nnsum4primesle9  47809  evengpop3  47812  evengpoap3  47813  nnsum4primeseven  47814  nnsum4primesevenALTV  47815  wtgoldbnnsum4prm  47816  bgoldbnnsum3prm  47818  cycl3grtri  47959  usgrexmpl1lem  48025  usgrexmpl2lem  48030  usgrexmpl2nb3  48038  usgrexmpl2nb4  48039  usgrexmpl2nb5  48040  usgrexmpl2trifr  48041  gpgusgralem  48060  gpg3nbgrvtx0  48078  gpg3kgrtriexlem1  48085  gpg3kgrtriexlem3  48087  gpg3kgrtriexlem4  48088  gpg3kgrtriexlem6  48090  pgrpgt2nabl  48341  ackval42  48676  sepfsepc  48902