Theorem 6re 12271

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 12248	. 2 ⊢ 6 = (5 + 1)
2		5re 12268	. . 3 ⊢ 5 ∈ ℝ
3		1re 11144	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11160	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2832	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℝcr 11037  1c1 11039   + caddc 11041  5c5 12239  6c6 12240

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 2708  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248

This theorem is referenced by:  7re  12274  7pos  12292  4lt6  12358  3lt6  12359  2lt6  12360  1lt6  12361  6lt7  12362  5lt7  12363  6lt8  12369  5lt8  12370  6lt9  12377  5lt9  12378  8th4div3  12397  halfpm6th  12399  div4p1lem1div2  12432  6lt10  12778  5lt10  12779  5recm6rec  12787  bpoly2  16022  bpoly3  16023  efi4p  16104  resin4p  16105  recos4p  16106  ef01bndlem  16151  sin01bnd  16152  cos01bnd  16153  slotsdifipndx  17298  slotstnscsi  17323  plendxnvscandx  17337  slotsdnscsi  17355  lt6abl  19870  sincos6thpi  26480  pigt3  26482  basellem5  27048  basellem8  27051  basellem9  27052  ppiublem1  27165  ppiublem2  27166  ppiub  27167  chtub  27175  bposlem6  27252  bposlem8  27254  slotsinbpsd  28509  slotslnbpsd  28510  ex-res  30511  hgt750lemd  34792  hgt750lem2  34796  hgt750leme  34802  problem4  35850  problem5  35851  6rp  42733  asin1half  42789  nprmdvdsfacm1lem2  48084  nprmdvdsfacm1lem4  48086  nprmdvdsfacm1  48087  ppivalnnnprmge6  48089  gbegt5  48237  gbowgt5  48238  gbowge7  48239  gboge9  48240  sbgoldbwt  48253  sgoldbeven3prm  48259  mogoldbb  48261  sbgoldbo  48263  nnsum3primesle9  48270  nnsum4primesodd  48272  wtgoldbnnsum4prm  48278  bgoldbnnsum3prm  48280  pgrple2abl  48841