Theorem 6re 12262

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 12239	. 2 ⊢ 6 = (5 + 1)
2		5re 12259	. . 3 ⊢ 5 ∈ ℝ
3		1re 11135	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11151	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2835	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2119  (class class class)co 7356  ℝcr 11028  1c1 11030   + caddc 11032  5c5 12230  6c6 12231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rrecex 11101  ax-cnre 11102

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-iota 6441  df-fv 6493  df-ov 7359  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239

This theorem is referenced by:  7re  12265  7pos  12283  4lt6  12349  3lt6  12350  2lt6  12351  1lt6  12352  6lt7  12353  5lt7  12354  6lt8  12360  5lt8  12361  6lt9  12368  5lt9  12369  8th4div3  12388  halfpm6th  12390  div4p1lem1div2  12423  6lt10  12769  5lt10  12770  5recm6rec  12778  bpoly2  16013  bpoly3  16014  efi4p  16095  resin4p  16096  recos4p  16097  ef01bndlem  16142  sin01bnd  16143  cos01bnd  16144  slotsdifipndx  17289  slotstnscsi  17314  plendxnvscandx  17328  slotsdnscsi  17346  lt6abl  19861  sincos6thpi  26498  pigt3  26500  basellem5  27066  basellem8  27069  basellem9  27070  ppiublem1  27183  ppiublem2  27184  ppiub  27185  chtub  27193  bposlem6  27270  bposlem8  27272  slotsinbpsd  28527  slotslnbpsd  28528  ex-res  30529  hgt750lemd  34832  hgt750lem2  34836  hgt750leme  34842  problem4  35896  problem5  35897  6rp  42778  asin1half  42834  nprmdvdsfacm1lem2  48099  nprmdvdsfacm1lem4  48101  nprmdvdsfacm1  48102  ppivalnnnprmge6  48104  gbegt5  48252  gbowgt5  48253  gbowge7  48254  gboge9  48255  sbgoldbwt  48268  sgoldbeven3prm  48274  mogoldbb  48276  sbgoldbo  48278  nnsum3primesle9  48285  nnsum4primesodd  48287  wtgoldbnnsum4prm  48293  bgoldbnnsum3prm  48295  pgrple2abl  48856