Theorem 6re 12247

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 12224	. 2 ⊢ 6 = (5 + 1)
2		5re 12244	. . 3 ⊢ 5 ∈ ℝ
3		1re 11144	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11159	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2833	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7368  ℝcr 11037  1c1 11039   + caddc 11041  5c5 12215  6c6 12216

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 2709  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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-2 12220  df-3 12221  df-4 12222  df-5 12223  df-6 12224

This theorem is referenced by:  7re  12250  7pos  12268  4lt6  12334  3lt6  12335  2lt6  12336  1lt6  12337  6lt7  12338  5lt7  12339  6lt8  12345  5lt8  12346  6lt9  12353  5lt9  12354  8th4div3  12373  halfpm6th  12375  div4p1lem1div2  12408  6lt10  12753  5lt10  12754  5recm6rec  12762  bpoly2  15992  bpoly3  15993  efi4p  16074  resin4p  16075  recos4p  16076  ef01bndlem  16121  sin01bnd  16122  cos01bnd  16123  slotsdifipndx  17267  slotstnscsi  17292  plendxnvscandx  17306  slotsdnscsi  17324  lt6abl  19839  sincos6thpi  26496  pigt3  26498  basellem5  27066  basellem8  27069  basellem9  27070  ppiublem1  27184  ppiublem2  27185  ppiub  27186  chtub  27194  bposlem6  27271  bposlem8  27273  slotsinbpsd  28528  slotslnbpsd  28529  ex-res  30532  hgt750lemd  34830  hgt750lem2  34834  hgt750leme  34840  problem4  35888  problem5  35889  6rp  42675  asin1half  42731  gbegt5  48125  gbowgt5  48126  gbowge7  48127  gboge9  48128  sbgoldbwt  48141  sgoldbeven3prm  48147  mogoldbb  48149  sbgoldbo  48151  nnsum3primesle9  48158  nnsum4primesodd  48160  wtgoldbnnsum4prm  48166  bgoldbnnsum3prm  48168  pgrple2abl  48729