Theorem 3re 12223

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 12207	. 2 ⊢ 3 = (2 + 1)
2		2re 12217	. . 3 ⊢ 2 ∈ ℝ
3		1re 11130	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11145	. 2 ⊢ (2 + 1) ∈ ℝ
5	1, 4	eqeltri 2830	1 ⊢ 3 ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7356  ℝcr 11023  1c1 11025   + caddc 11027  2c2 12198  3c3 12199

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 2706  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-i2m1 11092  ax-1ne0 11093  ax-rrecex 11096  ax-cnre 11097

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 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-2 12206  df-3 12207

This theorem is referenced by:  4re  12227  4pos  12250  1lt3  12311  3lt4  12312  2lt4  12313  3lt5  12316  3lt6  12321  2lt6  12322  3lt7  12327  2lt7  12328  3lt8  12334  2lt8  12335  3lt9  12342  2lt9  12343  1le3  12350  3halfnz  12569  3lt10  12742  2lt10  12743  5eluz3  12794  uzuzle23  12795  uzuzle34  12797  uz3m2nn  12805  nn01to3  12852  3rp  12909  fz0to4untppr  13544  fz0to5un2tp  13545  expnass  14129  hashtpg  14406  hash3tpde  14414  01sqrexlem7  15169  sqrt9  15194  caucvgrlem  15594  bpoly4  15980  ef01bndlem  16107  sin01bnd  16108  cos2bnd  16111  sin01gt0  16113  cos01gt0  16114  egt2lt3  16129  rpnnen2lem3  16139  rpnnen2lem4  16140  rpnnen2lem9  16145  flodddiv4  16340  ge2nprmge4  16626  starvndxnmulrndx  17224  scandxnmulrndx  17236  vscandxnmulrndx  17241  ipndxnmulrndx  17252  tsetndxnmulrndx  17276  plendxnmulrndx  17290  dsndxnmulrndx  17309  slotsdifunifndx  17319  vitalilem4  25566  dveflem  25937  sincosq3sgn  26463  sincosq4sgn  26464  tangtx  26468  sincos6thpi  26479  pigt3  26481  pige3  26482  pige3ALT  26483  ang180lem2  26774  1cubrlem  26805  log2cnv  26908  log2tlbnd  26909  log2ub  26913  cxploglim2  26943  basellem5  27049  basellem9  27053  ppiublem1  27167  ppiub  27169  chtub  27177  bposlem2  27250  bposlem3  27251  bposlem4  27252  bposlem5  27253  bposlem6  27254  bposlem8  27256  bposlem9  27257  lgsdir2lem1  27290  2lgslem3  27369  chebbnd1lem2  27435  chebbnd1lem3  27436  chebbnd1  27437  chto1ub  27441  dchrvmasumlem2  27463  dchrvmasumlema  27465  dchrvmasumiflem1  27466  mulog2sumlem2  27500  pntibndlem1  27554  pntibndlem2  27556  pntlemb  27562  pntlemk  27571  pntlemo  27572  istrkg3ld  28482  tgcgr4  28552  axlowdimlem16  28979  axlowdimlem17  28980  axlowdim  28983  usgrexmplef  29281  upgr4cycl4dv4e  30209  konigsbergiedgw  30272  konigsberglem1  30276  konigsberglem2  30277  konigsberglem3  30278  konigsberglem4  30279  frgrogt3nreg  30421  friendshipgt3  30422  friendship  30423  ex-dif  30447  ex-in  30449  ex-fl  30471  ex-ceil  30472  ex-gcd  30481  threehalves  32945  iconstr  33872  2sqr3minply  33886  cos9thpiminplylem3  33890  cos9thpinconstrlem1  33895  prodfzo03  34709  hgt750lem  34757  hgt750lem2  34758  hgt750leme  34764  cusgracyclt3v  35299  problem3  35810  problem5  35812  poimirlem9  37769  itg2addnclem2  37812  heiborlem5  37955  heiborlem6  37956  heiborlem7  37957  heiborlem8  37958  3lexlogpow5ineq2  42248  3lexlogpow5ineq4  42249  3lexlogpow5ineq3  42250  3lexlogpow2ineq1  42251  3lexlogpow2ineq2  42252  3lexlogpow5ineq5  42253  aks4d1lem1  42255  aks4d1p1p3  42262  aks4d1p1p2  42263  aks4d1p1p4  42264  aks4d1p1p6  42266  aks4d1p1p5  42268  aks4d1p1  42269  aks4d1p2  42270  aks4d1p3  42271  aks4d1p5  42273  aks4d1p6  42274  aks4d1p7d1  42275  aks4d1p7  42276  aks4d1p8  42280  aks4d1p9  42281  2np3bcnp1  42337  2ap1caineq  42338  aks6d1c7lem1  42373  aks6d1c7lem2  42374  aks6d1c7  42377  aks5lem6  42385  aks5lem8  42394  acos1half  42555  sn-0ne2  42603  3cubeslem2  42869  3cubeslem4  42873  jm2.23  43180  jm2.20nn  43181  lt4addmuld  45496  stoweidlem11  46197  stoweidlem13  46199  stoweidlem26  46212  stoweidlem34  46220  stoweidlem42  46228  stoweidlem59  46245  stoweidlem62  46248  stoweid  46249  wallispilem4  46254  fourierdlem87  46379  smfmullem4  46980  modm2nep1  47554  modm1nep2  47556  fmtnoge3  47718  fmtnoprmfac2lem1  47754  31prm  47785  9fppr8  47925  fpprel2  47929  nfermltl8rev  47930  nfermltl2rev  47931  gbegt5  47949  gboge9  47952  sbgoldbwt  47965  sbgoldbst  47966  sbgoldbalt  47969  sbgoldbo  47975  nnsum3primes4  47976  nnsum4primes4  47977  nnsum4primesprm  47979  nnsum3primesgbe  47980  nnsum4primesgbe  47981  nnsum3primesle9  47982  nnsum4primesle9  47983  evengpop3  47986  evengpoap3  47987  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  wtgoldbnnsum4prm  47990  bgoldbnnsum3prm  47992  cycl3grtri  48135  usgrexmpl1lem  48209  usgrexmpl2lem  48214  usgrexmpl2nb3  48222  usgrexmpl2nb4  48223  usgrexmpl2nb5  48224  usgrexmpl2trifr  48225  gpgusgralem  48244  gpg3nbgrvtx0  48264  gpg3kgrtriexlem1  48271  gpg3kgrtriexlem3  48273  gpg3kgrtriexlem4  48274  gpg3kgrtriexlem6  48276  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  pgrpgt2nabl  48554  ackval42  48884  sepfsepc  49115