Theorem 6re 12235

Description: The number 6 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
6re	⊢ 6 ∈ ℝ

Proof of Theorem 6re

Step	Hyp	Ref	Expression
1		df-6 12212	. 2 ⊢ 6 = (5 + 1)
2		5re 12232	. . 3 ⊢ 5 ∈ ℝ
3		1re 11132	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11147	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2832	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℝcr 11025  1c1 11027   + caddc 11029  5c5 12203  6c6 12204

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  df-4 12210  df-5 12211  df-6 12212

This theorem is referenced by:  7re  12238  7pos  12256  4lt6  12322  3lt6  12323  2lt6  12324  1lt6  12325  6lt7  12326  5lt7  12327  6lt8  12333  5lt8  12334  6lt9  12341  5lt9  12342  8th4div3  12361  halfpm6th  12363  div4p1lem1div2  12396  6lt10  12741  5lt10  12742  5recm6rec  12750  bpoly2  15980  bpoly3  15981  efi4p  16062  resin4p  16063  recos4p  16064  ef01bndlem  16109  sin01bnd  16110  cos01bnd  16111  slotsdifipndx  17255  slotstnscsi  17280  plendxnvscandx  17294  slotsdnscsi  17312  lt6abl  19824  sincos6thpi  26481  pigt3  26483  basellem5  27051  basellem8  27054  basellem9  27055  ppiublem1  27169  ppiublem2  27170  ppiub  27171  chtub  27179  bposlem6  27256  bposlem8  27258  slotsinbpsd  28513  slotslnbpsd  28514  ex-res  30516  hgt750lemd  34805  hgt750lem2  34809  hgt750leme  34815  problem4  35862  problem5  35863  6rp  42566  asin1half  42622  gbegt5  48017  gbowgt5  48018  gbowge7  48019  gboge9  48020  sbgoldbwt  48033  sgoldbeven3prm  48039  mogoldbb  48041  sbgoldbo  48043  nnsum3primesle9  48050  nnsum4primesodd  48052  wtgoldbnnsum4prm  48058  bgoldbnnsum3prm  48060  pgrple2abl  48621