Theorem 3re 12373

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 12357	. 2 ⊢ 3 = (2 + 1)
2		2re 12367	. . 3 ⊢ 2 ∈ ℝ
3		1re 11290	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11305	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2840	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℝcr 11183  1c1 11185   + caddc 11187  2c2 12348  3c3 12349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-2 12356  df-3 12357

This theorem is referenced by:  4re  12377  3ne0  12399  4pos  12400  1lt3  12466  3lt4  12467  2lt4  12468  3lt5  12471  3lt6  12476  2lt6  12477  3lt7  12482  2lt7  12483  3lt8  12489  2lt8  12490  3lt9  12497  2lt9  12498  1le3  12505  3halfnz  12722  3lt10  12895  2lt10  12896  uzuzle23  12954  uz3m2nn  12956  nn01to3  13006  3rp  13063  fz0to4untppr  13687  fz0to5un2tp  13688  expnass  14257  hashtpg  14534  hash3tpde  14542  01sqrexlem7  15297  sqrt9  15322  caucvgrlem  15721  bpoly4  16107  ef01bndlem  16232  sin01bnd  16233  cos2bnd  16236  sin01gt0  16238  cos01gt0  16239  egt2lt3  16254  rpnnen2lem3  16264  rpnnen2lem4  16265  rpnnen2lem9  16270  flodddiv4  16461  ge2nprmge4  16748  starvndxnmulrndx  17365  scandxnmulrndx  17377  vscandxnmulrndx  17382  ipndxnmulrndx  17393  tsetndxnmulrndx  17417  plendxnmulrndx  17431  dsndxnmulrndx  17450  slotsdifunifndx  17460  cnfldfunALTOLDOLD  21416  matscaOLD  22441  matvscaOLD  22443  vitalilem4  25665  dveflem  26037  sincosq3sgn  26560  sincosq4sgn  26561  tangtx  26565  sincos6thpi  26576  pigt3  26578  pige3  26579  pige3ALT  26580  ang180lem2  26871  1cubrlem  26902  log2cnv  27005  log2tlbnd  27006  log2ub  27010  cxploglim2  27040  basellem5  27146  basellem9  27150  ppiublem1  27264  ppiub  27266  chtub  27274  bposlem2  27347  bposlem3  27348  bposlem4  27349  bposlem5  27350  bposlem6  27351  bposlem8  27353  bposlem9  27354  lgsdir2lem1  27387  2lgslem3  27466  chebbnd1lem2  27532  chebbnd1lem3  27533  chebbnd1  27534  chto1ub  27538  dchrvmasumlem2  27560  dchrvmasumlema  27562  dchrvmasumiflem1  27563  mulog2sumlem2  27597  pntibndlem1  27651  pntibndlem2  27653  pntlemb  27659  pntlemk  27668  pntlemo  27669  istrkg3ld  28487  tgcgr4  28557  axlowdimlem16  28990  axlowdimlem17  28991  axlowdim  28994  usgrexmplef  29294  upgr4cycl4dv4e  30217  konigsbergiedgw  30280  konigsberglem1  30284  konigsberglem2  30285  konigsberglem3  30286  konigsberglem4  30287  frgrogt3nreg  30429  friendshipgt3  30430  friendship  30431  ex-dif  30455  ex-in  30457  ex-fl  30479  ex-ceil  30480  ex-gcd  30489  threehalves  32879  resvmulrOLD  33331  2sqr3minply  33738  prodfzo03  34580  hgt750lem  34628  hgt750lem2  34629  hgt750leme  34635  cusgracyclt3v  35124  problem3  35635  problem5  35637  poimirlem9  37589  itg2addnclem2  37632  heiborlem5  37775  heiborlem6  37776  heiborlem7  37777  heiborlem8  37778  3lexlogpow5ineq2  42012  3lexlogpow5ineq4  42013  3lexlogpow5ineq3  42014  3lexlogpow2ineq1  42015  3lexlogpow2ineq2  42016  3lexlogpow5ineq5  42017  aks4d1lem1  42019  aks4d1p1p3  42026  aks4d1p1p2  42027  aks4d1p1p4  42028  aks4d1p1p6  42030  aks4d1p1p5  42032  aks4d1p1  42033  aks4d1p2  42034  aks4d1p3  42035  aks4d1p5  42037  aks4d1p6  42038  aks4d1p7d1  42039  aks4d1p7  42040  aks4d1p8  42044  aks4d1p9  42045  2np3bcnp1  42101  2ap1caineq  42102  aks6d1c7lem1  42137  aks6d1c7lem2  42138  aks6d1c7  42141  aks5lem6  42149  aks5lem8  42158  2xp3dxp2ge1d  42198  acos1half  42340  sn-0ne2  42382  3cubeslem2  42641  3cubeslem4  42645  jm2.23  42953  jm2.20nn  42954  mnringscadOLD  44192  mnringvscadOLD  44194  lt4addmuld  45221  stoweidlem11  45932  stoweidlem13  45934  stoweidlem26  45947  stoweidlem34  45955  stoweidlem42  45963  stoweidlem59  45980  stoweidlem62  45983  stoweid  45984  wallispilem4  45989  fourierdlem87  46114  smfmullem4  46715  fmtnoge3  47404  fmtnoprmfac2lem1  47440  31prm  47471  9fppr8  47611  fpprel2  47615  nfermltl8rev  47616  nfermltl2rev  47617  gbegt5  47635  gboge9  47638  sbgoldbwt  47651  sbgoldbst  47652  sbgoldbalt  47655  sbgoldbo  47661  nnsum3primes4  47662  nnsum4primes4  47663  nnsum4primesprm  47665  nnsum3primesgbe  47666  nnsum4primesgbe  47667  nnsum3primesle9  47668  nnsum4primesle9  47669  evengpop3  47672  evengpoap3  47673  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  usgrexmpl1lem  47836  usgrexmpl2lem  47841  usgrexmpl2nb3  47849  usgrexmpl2nb4  47850  usgrexmpl2nb5  47851  usgrexmpl2trifr  47852  pgrpgt2nabl  48091  ackval42  48430  sepfsepc  48607