Theorem 6re 12433

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 12409	. 2 ⊢ 6 = (5 + 1)
2		5re 12430	. . 3 ⊢ 5 ∈ ℝ
3		1re 11308	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11324	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2857	1 ⊢ 6 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℝcr 11199  1c1 11201   + caddc 11203  5c5 12400  6c6 12401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-i2m1 11268  ax-1ne0 11269  ax-rrecex 11272  ax-cnre 11273

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546  df-ov 7423  df-2 12405  df-3 12406  df-4 12407  df-5 12408  df-6 12409

This theorem is used by:  7re  12436  4lt6  12527  3lt6  12528  2lt6  12529  1lt6  12530  6lt7  12531  5lt7  12532  6lt8  12538  5lt8  12539  6lt9  12546  5lt9  12547  8th4div3  12566  halfpm6th  12568  div4p1lem1div2  12601  6lt10  12954  5recm6rec  12964  bpoly2  16223  bpoly3  16224  efi4p  16305  resin4p  16306  recos4p  16307  ef01bndlem  16352  sin01bnd  16353  cos01bnd  16354  slotsdifipndx  17506  slotstnscsi  17531  plendxnvscandx  17545  slotsdnscsi  17563  lt6abl  20109  sincos6thpi  26844  pigt3  26846  basellem5  27412  basellem8  27415  basellem9  27416  ppiublem1  27529  ppiublem2  27530  ppiub  27531  chtub  27539  bposlem6  27616  bposlem8  27618  slotsinbpsd  28903  slotslnbpsd  28904  ex-res  31042  hgt750lemd  35277  hgt750lem2  35281  hgt750leme  35287  problem4  36433  problem5  36434  6rp  43358  asin1half  43408  nprmdvdsfacm1lem2  48705  nprmdvdsfacm1lem4  48707  nprmdvdsfacm1  48708  ppivalnnnprmge6  48710  gbegt5  48858  gbowgt5  48859  gbowge7  48860  gboge9  48861  sbgoldbwt  48874  sgoldbeven3prm  48880  mogoldbb  48882  sbgoldbo  48884  nnsum3primesle9  48891  nnsum4primesodd  48893  wtgoldbnnsum4prm  48899  bgoldbnnsum3prm  48901  pgrple2abl  49476  veronesev1lem  50972  veronesev2lem  50973  veronesev3lem  50974  veronesev4lem  50975  veronesev5lem  50976  veronesev6lem  50977  veronesevrowd  50978  veronesematrowd  50980  veroquadgsumlem  50982  veroquadmodzerod  50983  veroquadnolindfd  50984