Theorem 6re 12308

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 12284	. 2 ⊢ 6 = (5 + 1)
2		5re 12305	. . 3 ⊢ 5 ∈ ℝ
3		1re 11181	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11197	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2858	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2142  (class class class)co 7396  ℝcr 11072  1c1 11074   + caddc 11076  5c5 12275  6c6 12276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-i2m1 11141  ax-1ne0 11142  ax-rrecex 11145  ax-cnre 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284

This theorem is referenced by:  7re  12311  4lt6  12402  3lt6  12403  2lt6  12404  1lt6  12405  6lt7  12406  5lt7  12407  6lt8  12413  5lt8  12414  6lt9  12421  5lt9  12422  8th4div3  12441  halfpm6th  12443  div4p1lem1div2  12476  6lt10  12828  5recm6rec  12838  bpoly2  16087  bpoly3  16088  efi4p  16169  resin4p  16170  recos4p  16171  ef01bndlem  16216  sin01bnd  16217  cos01bnd  16218  slotsdifipndx  17364  slotstnscsi  17389  plendxnvscandx  17403  slotsdnscsi  17421  lt6abl  19935  sincos6thpi  26581  pigt3  26583  basellem5  27149  basellem8  27152  basellem9  27153  ppiublem1  27266  ppiublem2  27267  ppiub  27268  chtub  27276  bposlem6  27353  bposlem8  27355  slotsinbpsd  28610  slotslnbpsd  28611  ex-res  30643  hgt750lemd  34942  hgt750lem2  34946  hgt750leme  34952  problem4  36018  problem5  36019  6rp  42910  asin1half  42966  nprmdvdsfacm1lem2  48230  nprmdvdsfacm1lem4  48232  nprmdvdsfacm1  48233  ppivalnnnprmge6  48235  gbegt5  48383  gbowgt5  48384  gbowge7  48385  gboge9  48386  sbgoldbwt  48399  sgoldbeven3prm  48405  mogoldbb  48407  sbgoldbo  48409  nnsum3primesle9  48416  nnsum4primesodd  48418  wtgoldbnnsum4prm  48424  bgoldbnnsum3prm  48426  pgrple2abl  48987