Theorem 6re 12326

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 12302	. 2 ⊢ 6 = (5 + 1)
2		5re 12323	. . 3 ⊢ 5 ∈ ℝ
3		1re 11203	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11219	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2859	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℝcr 11094  1c1 11096   + caddc 11098  5c5 12293  6c6 12294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-i2m1 11163  ax-1ne0 11164  ax-rrecex 11167  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-2 12298  df-3 12299  df-4 12300  df-5 12301  df-6 12302

This theorem is referenced by:  7re  12329  4lt6  12420  3lt6  12421  2lt6  12422  1lt6  12423  6lt7  12424  5lt7  12425  6lt8  12431  5lt8  12432  6lt9  12439  5lt9  12440  8th4div3  12459  halfpm6th  12461  div4p1lem1div2  12494  6lt10  12846  5recm6rec  12856  bpoly2  16106  bpoly3  16107  efi4p  16188  resin4p  16189  recos4p  16190  ef01bndlem  16235  sin01bnd  16236  cos01bnd  16237  slotsdifipndx  17383  slotstnscsi  17408  plendxnvscandx  17422  slotsdnscsi  17440  lt6abl  19960  sincos6thpi  26681  pigt3  26683  basellem5  27249  basellem8  27252  basellem9  27253  ppiublem1  27366  ppiublem2  27367  ppiub  27368  chtub  27376  bposlem6  27453  bposlem8  27455  slotsinbpsd  28710  slotslnbpsd  28711  ex-res  30792  hgt750lemd  35035  hgt750lem2  35039  hgt750leme  35045  problem4  36160  problem5  36161  6rp  43082  asin1half  43138  nprmdvdsfacm1lem2  48393  nprmdvdsfacm1lem4  48395  nprmdvdsfacm1  48396  ppivalnnnprmge6  48398  gbegt5  48546  gbowgt5  48547  gbowge7  48548  gboge9  48549  sbgoldbwt  48562  sgoldbeven3prm  48568  mogoldbb  48570  sbgoldbo  48572  nnsum3primesle9  48579  nnsum4primesodd  48581  wtgoldbnnsum4prm  48587  bgoldbnnsum3prm  48589  pgrple2abl  49165