Theorem 6re 12348

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 12324	. 2 ⊢ 6 = (5 + 1)
2		5re 12345	. . 3 ⊢ 5 ∈ ℝ
3		1re 11225	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11241	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2861	1 ⊢ 6 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7419  ℝcr 11116  1c1 11118   + caddc 11120  5c5 12315  6c6 12316

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-1cn 11175  ax-icn 11176  ax-addcl 11177  ax-addrcl 11178  ax-mulcl 11179  ax-mulrcl 11180  ax-i2m1 11185  ax-1ne0 11186  ax-rrecex 11189  ax-cnre 11190

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-2 12320  df-3 12321  df-4 12322  df-5 12323  df-6 12324

This theorem is used by:  7re  12351  4lt6  12442  3lt6  12443  2lt6  12444  1lt6  12445  6lt7  12446  5lt7  12447  6lt8  12453  5lt8  12454  6lt9  12461  5lt9  12462  8th4div3  12481  halfpm6th  12483  div4p1lem1div2  12516  6lt10  12869  5recm6rec  12879  bpoly2  16135  bpoly3  16136  efi4p  16217  resin4p  16218  recos4p  16219  ef01bndlem  16264  sin01bnd  16265  cos01bnd  16266  slotsdifipndx  17412  slotstnscsi  17437  plendxnvscandx  17451  slotsdnscsi  17469  lt6abl  20011  sincos6thpi  26734  pigt3  26736  basellem5  27302  basellem8  27305  basellem9  27306  ppiublem1  27419  ppiublem2  27420  ppiub  27421  chtub  27429  bposlem6  27506  bposlem8  27508  slotsinbpsd  28763  slotslnbpsd  28764  ex-res  30865  hgt750lemd  35102  hgt750lem2  35106  hgt750leme  35112  problem4  36199  problem5  36200  6rp  43122  asin1half  43178  nprmdvdsfacm1lem2  48433  nprmdvdsfacm1lem4  48435  nprmdvdsfacm1  48436  ppivalnnnprmge6  48438  gbegt5  48586  gbowgt5  48587  gbowge7  48588  gboge9  48589  sbgoldbwt  48602  sgoldbeven3prm  48608  mogoldbb  48610  sbgoldbo  48612  nnsum3primesle9  48619  nnsum4primesodd  48621  wtgoldbnnsum4prm  48627  bgoldbnnsum3prm  48629  pgrple2abl  49204