Theorem 6re 12218

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 12195	. 2 ⊢ 6 = (5 + 1)
2		5re 12215	. . 3 ⊢ 5 ∈ ℝ
3		1re 11115	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11130	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  ℝcr 11008  1c1 11010   + caddc 11012  5c5 12186  6c6 12187

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 2701  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-i2m1 11077  ax-1ne0 11078  ax-rrecex 11081  ax-cnre 11082

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-2 12191  df-3 12192  df-4 12193  df-5 12194  df-6 12195

This theorem is referenced by:  7re  12221  7pos  12239  4lt6  12305  3lt6  12306  2lt6  12307  1lt6  12308  6lt7  12309  5lt7  12310  6lt8  12316  5lt8  12317  6lt9  12324  5lt9  12325  8th4div3  12344  halfpm6th  12346  div4p1lem1div2  12379  6lt10  12725  5lt10  12726  5recm6rec  12734  bpoly2  15964  bpoly3  15965  efi4p  16046  resin4p  16047  recos4p  16048  ef01bndlem  16093  sin01bnd  16094  cos01bnd  16095  slotsdifipndx  17239  slotstnscsi  17264  plendxnvscandx  17278  slotsdnscsi  17296  lt6abl  19774  sincos6thpi  26423  pigt3  26425  basellem5  26993  basellem8  26996  basellem9  26997  ppiublem1  27111  ppiublem2  27112  ppiub  27113  chtub  27121  bposlem6  27198  bposlem8  27200  slotsinbpsd  28386  slotslnbpsd  28387  ex-res  30385  hgt750lemd  34622  hgt750lem2  34626  hgt750leme  34632  problem4  35651  problem5  35652  6rp  42284  asin1half  42340  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  48359