Theorem 6re 12354

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 12331	. 2 ⊢ 6 = (5 + 1)
2		5re 12351	. . 3 ⊢ 5 ∈ ℝ
3		1re 11259	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11274	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2835	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2106  (class class class)co 7431  ℝcr 11152  1c1 11154   + caddc 11156  5c5 12322  6c6 12323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-i2m1 11221  ax-1ne0 11222  ax-rrecex 11225  ax-cnre 11226

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-iota 6516  df-fv 6571  df-ov 7434  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331

This theorem is referenced by:  7re  12357  7pos  12375  4lt6  12446  3lt6  12447  2lt6  12448  1lt6  12449  6lt7  12450  5lt7  12451  6lt8  12457  5lt8  12458  6lt9  12465  5lt9  12466  8th4div3  12484  halfpm6th  12485  div4p1lem1div2  12519  6lt10  12865  5lt10  12866  5recm6rec  12875  bpoly2  16090  bpoly3  16091  efi4p  16170  resin4p  16171  recos4p  16172  ef01bndlem  16217  sin01bnd  16218  cos01bnd  16219  slotsdifipndx  17381  slotstnscsi  17406  plendxnvscandx  17420  slotsdnscsi  17438  lt6abl  19928  sralemOLD  21194  sravscaOLD  21204  zlmlemOLD  21546  sincos6thpi  26573  pigt3  26575  basellem5  27143  basellem8  27146  basellem9  27147  ppiublem1  27261  ppiublem2  27262  ppiub  27263  chtub  27271  bposlem6  27348  bposlem8  27350  slotsinbpsd  28464  slotslnbpsd  28465  ex-res  30470  zlmdsOLD  33924  zlmtsetOLD  33926  hgt750lemd  34642  hgt750lem2  34646  hgt750leme  34652  problem4  35653  problem5  35654  6rp  42314  asin1half  42366  gbegt5  47686  gbowgt5  47687  gbowge7  47688  gboge9  47689  sbgoldbwt  47702  sgoldbeven3prm  47708  mogoldbb  47710  sbgoldbo  47712  nnsum3primesle9  47719  nnsum4primesodd  47721  wtgoldbnnsum4prm  47727  bgoldbnnsum3prm  47729  pgrple2abl  48210