Theorem 6re 12357

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 12334	. 2 ⊢ 6 = (5 + 1)
2		5re 12354	. . 3 ⊢ 5 ∈ ℝ
3		1re 11262	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11277	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2836	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2107  (class class class)co 7432  ℝcr 11155  1c1 11157   + caddc 11159  5c5 12325  6c6 12326

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-i2m1 11224  ax-1ne0 11225  ax-rrecex 11228  ax-cnre 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568  df-ov 7435  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334

This theorem is referenced by:  7re  12360  7pos  12378  4lt6  12449  3lt6  12450  2lt6  12451  1lt6  12452  6lt7  12453  5lt7  12454  6lt8  12460  5lt8  12461  6lt9  12468  5lt9  12469  8th4div3  12488  halfpm6th  12490  div4p1lem1div2  12523  6lt10  12869  5lt10  12870  5recm6rec  12878  bpoly2  16094  bpoly3  16095  efi4p  16174  resin4p  16175  recos4p  16176  ef01bndlem  16221  sin01bnd  16222  cos01bnd  16223  slotsdifipndx  17380  slotstnscsi  17405  plendxnvscandx  17419  slotsdnscsi  17437  lt6abl  19914  sralemOLD  21177  sravscaOLD  21187  zlmlemOLD  21529  sincos6thpi  26559  pigt3  26561  basellem5  27129  basellem8  27132  basellem9  27133  ppiublem1  27247  ppiublem2  27248  ppiub  27249  chtub  27257  bposlem6  27334  bposlem8  27336  slotsinbpsd  28450  slotslnbpsd  28451  ex-res  30461  zlmdsOLD  33963  zlmtsetOLD  33965  hgt750lemd  34664  hgt750lem2  34668  hgt750leme  34674  problem4  35674  problem5  35675  6rp  42340  asin1half  42392  gbegt5  47753  gbowgt5  47754  gbowge7  47755  gboge9  47756  sbgoldbwt  47769  sgoldbeven3prm  47775  mogoldbb  47777  sbgoldbo  47779  nnsum3primesle9  47786  nnsum4primesodd  47788  wtgoldbnnsum4prm  47794  bgoldbnnsum3prm  47796  pgrple2abl  48286