Theorem 6re 12265

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 12242	. 2 ⊢ 6 = (5 + 1)
2		5re 12262	. . 3 ⊢ 5 ∈ ℝ
3		1re 11138	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11154	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2833	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℝcr 11031  1c1 11033   + caddc 11035  5c5 12233  6c6 12234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-i2m1 11100  ax-1ne0 11101  ax-rrecex 11104  ax-cnre 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-2 12238  df-3 12239  df-4 12240  df-5 12241  df-6 12242

This theorem is referenced by:  7re  12268  7pos  12286  4lt6  12352  3lt6  12353  2lt6  12354  1lt6  12355  6lt7  12356  5lt7  12357  6lt8  12363  5lt8  12364  6lt9  12371  5lt9  12372  8th4div3  12391  halfpm6th  12393  div4p1lem1div2  12426  6lt10  12772  5lt10  12773  5recm6rec  12781  bpoly2  16016  bpoly3  16017  efi4p  16098  resin4p  16099  recos4p  16100  ef01bndlem  16145  sin01bnd  16146  cos01bnd  16147  slotsdifipndx  17292  slotstnscsi  17317  plendxnvscandx  17331  slotsdnscsi  17349  lt6abl  19864  sincos6thpi  26496  pigt3  26498  basellem5  27065  basellem8  27068  basellem9  27069  ppiublem1  27182  ppiublem2  27183  ppiub  27184  chtub  27192  bposlem6  27269  bposlem8  27271  slotsinbpsd  28526  slotslnbpsd  28527  ex-res  30529  hgt750lemd  34811  hgt750lem2  34815  hgt750leme  34821  problem4  35869  problem5  35870  6rp  42750  asin1half  42806  nprmdvdsfacm1lem2  48099  nprmdvdsfacm1lem4  48101  nprmdvdsfacm1  48102  ppivalnnnprmge6  48104  gbegt5  48252  gbowgt5  48253  gbowge7  48254  gboge9  48255  sbgoldbwt  48268  sgoldbeven3prm  48274  mogoldbb  48276  sbgoldbo  48278  nnsum3primesle9  48285  nnsum4primesodd  48287  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  pgrple2abl  48856