Theorem 3re 12225

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 12209	. 2 ⊢ 3 = (2 + 1)
2		2re 12219	. . 3 ⊢ 2 ∈ ℝ
3		1re 11132	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11147	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2832	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℝcr 11025  1c1 11027   + caddc 11029  2c2 12200  3c3 12201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rrecex 11098  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-2 12208  df-3 12209

This theorem is referenced by:  4re  12229  4pos  12252  1lt3  12313  3lt4  12314  2lt4  12315  3lt5  12318  3lt6  12323  2lt6  12324  3lt7  12329  2lt7  12330  3lt8  12336  2lt8  12337  3lt9  12344  2lt9  12345  1le3  12352  3halfnz  12571  3lt10  12744  2lt10  12745  5eluz3  12796  uzuzle23  12797  uzuzle34  12799  uz3m2nn  12807  nn01to3  12854  3rp  12911  fz0to4untppr  13546  fz0to5un2tp  13547  expnass  14131  hashtpg  14408  hash3tpde  14416  01sqrexlem7  15171  sqrt9  15196  caucvgrlem  15596  bpoly4  15982  ef01bndlem  16109  sin01bnd  16110  cos2bnd  16113  sin01gt0  16115  cos01gt0  16116  egt2lt3  16131  rpnnen2lem3  16141  rpnnen2lem4  16142  rpnnen2lem9  16147  flodddiv4  16342  ge2nprmge4  16628  starvndxnmulrndx  17226  scandxnmulrndx  17238  vscandxnmulrndx  17243  ipndxnmulrndx  17254  tsetndxnmulrndx  17278  plendxnmulrndx  17292  dsndxnmulrndx  17311  slotsdifunifndx  17321  vitalilem4  25568  dveflem  25939  sincosq3sgn  26465  sincosq4sgn  26466  tangtx  26470  sincos6thpi  26481  pigt3  26483  pige3  26484  pige3ALT  26485  ang180lem2  26776  1cubrlem  26807  log2cnv  26910  log2tlbnd  26911  log2ub  26915  cxploglim2  26945  basellem5  27051  basellem9  27055  ppiublem1  27169  ppiub  27171  chtub  27179  bposlem2  27252  bposlem3  27253  bposlem4  27254  bposlem5  27255  bposlem6  27256  bposlem8  27258  bposlem9  27259  lgsdir2lem1  27292  2lgslem3  27371  chebbnd1lem2  27437  chebbnd1lem3  27438  chebbnd1  27439  chto1ub  27443  dchrvmasumlem2  27465  dchrvmasumlema  27467  dchrvmasumiflem1  27468  mulog2sumlem2  27502  pntibndlem1  27556  pntibndlem2  27558  pntlemb  27564  pntlemk  27573  pntlemo  27574  istrkg3ld  28533  tgcgr4  28603  axlowdimlem16  29030  axlowdimlem17  29031  axlowdim  29034  usgrexmplef  29332  upgr4cycl4dv4e  30260  konigsbergiedgw  30323  konigsberglem1  30327  konigsberglem2  30328  konigsberglem3  30329  konigsberglem4  30330  frgrogt3nreg  30472  friendshipgt3  30473  friendship  30474  ex-dif  30498  ex-in  30500  ex-fl  30522  ex-ceil  30523  ex-gcd  30532  threehalves  32996  iconstr  33923  2sqr3minply  33937  cos9thpiminplylem3  33941  cos9thpinconstrlem1  33946  prodfzo03  34760  hgt750lem  34808  hgt750lem2  34809  hgt750leme  34815  cusgracyclt3v  35350  problem3  35861  problem5  35863  poimirlem9  37830  itg2addnclem2  37873  heiborlem5  38016  heiborlem6  38017  heiborlem7  38018  heiborlem8  38019  3lexlogpow5ineq2  42319  3lexlogpow5ineq4  42320  3lexlogpow5ineq3  42321  3lexlogpow2ineq1  42322  3lexlogpow2ineq2  42323  3lexlogpow5ineq5  42324  aks4d1lem1  42326  aks4d1p1p3  42333  aks4d1p1p2  42334  aks4d1p1p4  42335  aks4d1p1p6  42337  aks4d1p1p5  42339  aks4d1p1  42340  aks4d1p2  42341  aks4d1p3  42342  aks4d1p5  42344  aks4d1p6  42345  aks4d1p7d1  42346  aks4d1p7  42347  aks4d1p8  42351  aks4d1p9  42352  2np3bcnp1  42408  2ap1caineq  42409  aks6d1c7lem1  42444  aks6d1c7lem2  42445  aks6d1c7  42448  aks5lem6  42456  aks5lem8  42465  acos1half  42623  sn-0ne2  42671  3cubeslem2  42937  3cubeslem4  42941  jm2.23  43248  jm2.20nn  43249  lt4addmuld  45564  stoweidlem11  46265  stoweidlem13  46267  stoweidlem26  46280  stoweidlem34  46288  stoweidlem42  46296  stoweidlem59  46313  stoweidlem62  46316  stoweid  46317  wallispilem4  46322  fourierdlem87  46447  smfmullem4  47048  modm2nep1  47622  modm1nep2  47624  fmtnoge3  47786  fmtnoprmfac2lem1  47822  31prm  47853  9fppr8  47993  fpprel2  47997  nfermltl8rev  47998  nfermltl2rev  47999  gbegt5  48017  gboge9  48020  sbgoldbwt  48033  sbgoldbst  48034  sbgoldbalt  48037  sbgoldbo  48043  nnsum3primes4  48044  nnsum4primes4  48045  nnsum4primesprm  48047  nnsum3primesgbe  48048  nnsum4primesgbe  48049  nnsum3primesle9  48050  nnsum4primesle9  48051  evengpop3  48054  evengpoap3  48055  nnsum4primeseven  48056  nnsum4primesevenALTV  48057  wtgoldbnnsum4prm  48058  bgoldbnnsum3prm  48060  cycl3grtri  48203  usgrexmpl1lem  48277  usgrexmpl2lem  48282  usgrexmpl2nb3  48290  usgrexmpl2nb4  48291  usgrexmpl2nb5  48292  usgrexmpl2trifr  48293  gpgusgralem  48312  gpg3nbgrvtx0  48332  gpg3kgrtriexlem1  48339  gpg3kgrtriexlem3  48341  gpg3kgrtriexlem4  48342  gpg3kgrtriexlem6  48344  pgnbgreunbgrlem2lem1  48370  pgnbgreunbgrlem2lem2  48371  pgrpgt2nabl  48622  ackval42  48952  sepfsepc  49183