Theorem 6re 12252

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 12229	. 2 ⊢ 6 = (5 + 1)
2		5re 12249	. . 3 ⊢ 5 ∈ ℝ
3		1re 11164	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11179	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2828	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2106  (class class class)co 7362  ℝcr 11059  1c1 11061   + caddc 11063  5c5 12220  6c6 12221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-i2m1 11128  ax-1ne0 11129  ax-rrecex 11132  ax-cnre 11133

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-iota 6453  df-fv 6509  df-ov 7365  df-2 12225  df-3 12226  df-4 12227  df-5 12228  df-6 12229

This theorem is referenced by:  7re  12255  7pos  12273  4lt6  12344  3lt6  12345  2lt6  12346  1lt6  12347  6lt7  12348  5lt7  12349  6lt8  12355  5lt8  12356  6lt9  12363  5lt9  12364  8th4div3  12382  halfpm6th  12383  div4p1lem1div2  12417  6lt10  12761  5lt10  12762  5recm6rec  12771  bpoly2  15951  bpoly3  15952  efi4p  16030  resin4p  16031  recos4p  16032  ef01bndlem  16077  sin01bnd  16078  cos01bnd  16079  slotsdifipndx  17230  slotstnscsi  17255  plendxnvscandx  17269  slotsdnscsi  17287  lt6abl  19686  sralemOLD  20698  sravscaOLD  20708  zlmlemOLD  20955  sincos6thpi  25909  pigt3  25911  basellem5  26471  basellem8  26474  basellem9  26475  ppiublem1  26587  ppiublem2  26588  ppiub  26589  chtub  26597  bposlem6  26674  bposlem8  26676  slotsinbpsd  27446  slotslnbpsd  27447  ex-res  29448  zlmdsOLD  32633  zlmtsetOLD  32635  hgt750lemd  33350  hgt750lem2  33354  hgt750leme  33360  problem4  34343  problem5  34344  gbegt5  46073  gbowgt5  46074  gbowge7  46075  gboge9  46076  sbgoldbwt  46089  sgoldbeven3prm  46095  mogoldbb  46097  sbgoldbo  46099  nnsum3primesle9  46106  nnsum4primesodd  46108  wtgoldbnnsum4prm  46114  bgoldbnnsum3prm  46116  pgrple2abl  46561