Theorem 6re 12221

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 12198	. 2 ⊢ 6 = (5 + 1)
2		5re 12218	. . 3 ⊢ 5 ∈ ℝ
3		1re 11118	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11133	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2827	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2111  (class class class)co 7352  ℝcr 11011  1c1 11013   + caddc 11015  5c5 12189  6c6 12190

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11070  ax-icn 11071  ax-addcl 11072  ax-addrcl 11073  ax-mulcl 11074  ax-mulrcl 11075  ax-i2m1 11080  ax-1ne0 11081  ax-rrecex 11084  ax-cnre 11085

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6443  df-fv 6495  df-ov 7355  df-2 12194  df-3 12195  df-4 12196  df-5 12197  df-6 12198

This theorem is referenced by:  7re  12224  7pos  12242  4lt6  12308  3lt6  12309  2lt6  12310  1lt6  12311  6lt7  12312  5lt7  12313  6lt8  12319  5lt8  12320  6lt9  12327  5lt9  12328  8th4div3  12347  halfpm6th  12349  div4p1lem1div2  12382  6lt10  12728  5lt10  12729  5recm6rec  12737  bpoly2  15970  bpoly3  15971  efi4p  16052  resin4p  16053  recos4p  16054  ef01bndlem  16099  sin01bnd  16100  cos01bnd  16101  slotsdifipndx  17245  slotstnscsi  17270  plendxnvscandx  17284  slotsdnscsi  17302  lt6abl  19813  sincos6thpi  26458  pigt3  26460  basellem5  27028  basellem8  27031  basellem9  27032  ppiublem1  27146  ppiublem2  27147  ppiub  27148  chtub  27156  bposlem6  27233  bposlem8  27235  slotsinbpsd  28425  slotslnbpsd  28426  ex-res  30428  hgt750lemd  34668  hgt750lem2  34672  hgt750leme  34678  problem4  35719  problem5  35720  6rp  42400  asin1half  42456  gbegt5  47866  gbowgt5  47867  gbowge7  47868  gboge9  47869  sbgoldbwt  47882  sgoldbeven3prm  47888  mogoldbb  47890  sbgoldbo  47892  nnsum3primesle9  47899  nnsum4primesodd  47901  wtgoldbnnsum4prm  47907  bgoldbnnsum3prm  47909  pgrple2abl  48470