Theorem 6re 12443

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 12419	. 2 ⊢ 6 = (5 + 1)
2		5re 12440	. . 3 ⊢ 5 ∈ ℝ
3		1re 11318	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11334	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2859	1 ⊢ 6 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7427  ℝcr 11209  1c1 11211   + caddc 11213  5c5 12410  6c6 12411

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-addrcl 11271  ax-mulcl 11272  ax-mulrcl 11273  ax-i2m1 11278  ax-1ne0 11279  ax-rrecex 11282  ax-cnre 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-iota 6500  df-fv 6554  df-ov 7430  df-2 12415  df-3 12416  df-4 12417  df-5 12418  df-6 12419

This theorem is used by:  7re  12446  4lt6  12537  3lt6  12538  2lt6  12539  1lt6  12540  6lt7  12541  5lt7  12542  6lt8  12548  5lt8  12549  6lt9  12556  5lt9  12557  8th4div3  12576  halfpm6th  12578  div4p1lem1div2  12611  6lt10  12964  5recm6rec  12974  bpoly2  16235  bpoly3  16236  efi4p  16317  resin4p  16318  recos4p  16319  ef01bndlem  16364  sin01bnd  16365  cos01bnd  16366  slotsdifipndx  17518  slotstnscsi  17543  plendxnvscandx  17557  slotsdnscsi  17575  lt6abl  20121  sincos6thpi  26856  pigt3  26858  basellem5  27424  basellem8  27427  basellem9  27428  ppiublem1  27541  ppiublem2  27542  ppiub  27543  chtub  27551  bposlem6  27628  bposlem8  27630  slotsinbpsd  28915  slotslnbpsd  28916  ex-res  31054  hgt750lemd  35330  hgt750lem2  35334  hgt750leme  35340  problem4  36554  problem5  36555  6rp  43498  asin1half  43548  nprmdvdsfacm1lem2  48845  nprmdvdsfacm1lem4  48847  nprmdvdsfacm1  48848  ppivalnnnprmge6  48850  gbegt5  48998  gbowgt5  48999  gbowge7  49000  gboge9  49001  sbgoldbwt  49014  sgoldbeven3prm  49020  mogoldbb  49022  sbgoldbo  49024  nnsum3primesle9  49031  nnsum4primesodd  49033  wtgoldbnnsum4prm  49039  bgoldbnnsum3prm  49041  pgrple2abl  49616  veronesev1lem  51187  veronesev2lem  51188  veronesev3lem  51189  veronesev4lem  51190  veronesev5lem  51191  veronesev6lem  51192  veronesevrowd  51193  veronesematrowd  51195  veroquadgsumlem  51197  veroquadmodzerod  51198  veroquadnolindfd  51199