Theorem 6re 12383

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 12360	. 2 ⊢ 6 = (5 + 1)
2		5re 12380	. . 3 ⊢ 5 ∈ ℝ
3		1re 11290	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11305	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2840	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℝcr 11183  1c1 11185   + caddc 11187  5c5 12351  6c6 12352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360

This theorem is referenced by:  7re  12386  7pos  12404  4lt6  12475  3lt6  12476  2lt6  12477  1lt6  12478  6lt7  12479  5lt7  12480  6lt8  12486  5lt8  12487  6lt9  12494  5lt9  12495  8th4div3  12513  halfpm6th  12514  div4p1lem1div2  12548  6lt10  12892  5lt10  12893  5recm6rec  12902  bpoly2  16105  bpoly3  16106  efi4p  16185  resin4p  16186  recos4p  16187  ef01bndlem  16232  sin01bnd  16233  cos01bnd  16234  slotsdifipndx  17394  slotstnscsi  17419  plendxnvscandx  17433  slotsdnscsi  17451  lt6abl  19937  sralemOLD  21199  sravscaOLD  21209  zlmlemOLD  21551  sincos6thpi  26576  pigt3  26578  basellem5  27146  basellem8  27149  basellem9  27150  ppiublem1  27264  ppiublem2  27265  ppiub  27266  chtub  27274  bposlem6  27351  bposlem8  27353  slotsinbpsd  28467  slotslnbpsd  28468  ex-res  30473  zlmdsOLD  33909  zlmtsetOLD  33911  hgt750lemd  34625  hgt750lem2  34629  hgt750leme  34635  problem4  35636  problem5  35637  6rp  42289  asin1half  42339  gbegt5  47635  gbowgt5  47636  gbowge7  47637  gboge9  47638  sbgoldbwt  47651  sgoldbeven3prm  47657  mogoldbb  47659  sbgoldbo  47661  nnsum3primesle9  47668  nnsum4primesodd  47670  wtgoldbnnsum4prm  47676  bgoldbnnsum3prm  47678  pgrple2abl  48090