Theorem 6re 12335

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 12312	. 2 ⊢ 6 = (5 + 1)
2		5re 12332	. . 3 ⊢ 5 ∈ ℝ
3		1re 11240	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11255	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2831	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7410  ℝcr 11133  1c1 11135   + caddc 11137  5c5 12303  6c6 12304

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-i2m1 11202  ax-1ne0 11203  ax-rrecex 11206  ax-cnre 11207

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312

This theorem is referenced by:  7re  12338  7pos  12356  4lt6  12427  3lt6  12428  2lt6  12429  1lt6  12430  6lt7  12431  5lt7  12432  6lt8  12438  5lt8  12439  6lt9  12446  5lt9  12447  8th4div3  12466  halfpm6th  12468  div4p1lem1div2  12501  6lt10  12847  5lt10  12848  5recm6rec  12856  bpoly2  16078  bpoly3  16079  efi4p  16160  resin4p  16161  recos4p  16162  ef01bndlem  16207  sin01bnd  16208  cos01bnd  16209  slotsdifipndx  17354  slotstnscsi  17379  plendxnvscandx  17393  slotsdnscsi  17411  lt6abl  19881  sincos6thpi  26482  pigt3  26484  basellem5  27052  basellem8  27055  basellem9  27056  ppiublem1  27170  ppiublem2  27171  ppiub  27172  chtub  27180  bposlem6  27257  bposlem8  27259  slotsinbpsd  28425  slotslnbpsd  28426  ex-res  30427  hgt750lemd  34685  hgt750lem2  34689  hgt750leme  34695  problem4  35695  problem5  35696  6rp  42319  asin1half  42375  gbegt5  47755  gbowgt5  47756  gbowge7  47757  gboge9  47758  sbgoldbwt  47771  sgoldbeven3prm  47777  mogoldbb  47779  sbgoldbo  47781  nnsum3primesle9  47788  nnsum4primesodd  47790  wtgoldbnnsum4prm  47796  bgoldbnnsum3prm  47798  pgrple2abl  48320