Theorem 6re 12276

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 12253	. 2 ⊢ 6 = (5 + 1)
2		5re 12273	. . 3 ⊢ 5 ∈ ℝ
3		1re 11174	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11189	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℝcr 11067  1c1 11069   + caddc 11071  5c5 12244  6c6 12245

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 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

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 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253

This theorem is referenced by:  7re  12279  7pos  12297  4lt6  12363  3lt6  12364  2lt6  12365  1lt6  12366  6lt7  12367  5lt7  12368  6lt8  12374  5lt8  12375  6lt9  12382  5lt9  12383  8th4div3  12402  halfpm6th  12404  div4p1lem1div2  12437  6lt10  12783  5lt10  12784  5recm6rec  12792  bpoly2  16023  bpoly3  16024  efi4p  16105  resin4p  16106  recos4p  16107  ef01bndlem  16152  sin01bnd  16153  cos01bnd  16154  slotsdifipndx  17298  slotstnscsi  17323  plendxnvscandx  17337  slotsdnscsi  17355  lt6abl  19825  sincos6thpi  26425  pigt3  26427  basellem5  26995  basellem8  26998  basellem9  26999  ppiublem1  27113  ppiublem2  27114  ppiub  27115  chtub  27123  bposlem6  27200  bposlem8  27202  slotsinbpsd  28368  slotslnbpsd  28369  ex-res  30370  hgt750lemd  34639  hgt750lem2  34643  hgt750leme  34649  problem4  35655  problem5  35656  6rp  42289  asin1half  42345  gbegt5  47762  gbowgt5  47763  gbowge7  47764  gboge9  47765  sbgoldbwt  47778  sgoldbeven3prm  47784  mogoldbb  47786  sbgoldbo  47788  nnsum3primesle9  47795  nnsum4primesodd  47797  wtgoldbnnsum4prm  47803  bgoldbnnsum3prm  47805  pgrple2abl  48353