Theorem 6re 12358

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 12334	. 2 ⊢ 6 = (5 + 1)
2		5re 12355	. . 3 ⊢ 5 ∈ ℝ
3		1re 11235	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11251	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2856	1 ⊢ 6 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7414  ℝcr 11126  1c1 11128   + caddc 11130  5c5 12325  6c6 12326

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 2732  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rrecex 11199  ax-cnre 11200

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 6489  df-fv 6541  df-ov 7417  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334

This theorem is used by:  7re  12361  4lt6  12452  3lt6  12453  2lt6  12454  1lt6  12455  6lt7  12456  5lt7  12457  6lt8  12463  5lt8  12464  6lt9  12471  5lt9  12472  8th4div3  12491  halfpm6th  12493  div4p1lem1div2  12526  6lt10  12879  5recm6rec  12889  bpoly2  16146  bpoly3  16147  efi4p  16228  resin4p  16229  recos4p  16230  ef01bndlem  16275  sin01bnd  16276  cos01bnd  16277  slotsdifipndx  17423  slotstnscsi  17448  plendxnvscandx  17462  slotsdnscsi  17480  lt6abl  20025  sincos6thpi  26756  pigt3  26758  basellem5  27324  basellem8  27327  basellem9  27328  ppiublem1  27441  ppiublem2  27442  ppiub  27443  chtub  27451  bposlem6  27528  bposlem8  27530  slotsinbpsd  28785  slotslnbpsd  28786  ex-res  30924  hgt750lemd  35159  hgt750lem2  35163  hgt750leme  35169  problem4  36250  problem5  36251  6rp  43179  asin1half  43235  nprmdvdsfacm1lem2  48527  nprmdvdsfacm1lem4  48529  nprmdvdsfacm1  48530  ppivalnnnprmge6  48532  gbegt5  48680  gbowgt5  48681  gbowge7  48682  gboge9  48683  sbgoldbwt  48696  sgoldbeven3prm  48702  mogoldbb  48704  sbgoldbo  48706  nnsum3primesle9  48713  nnsum4primesodd  48715  wtgoldbnnsum4prm  48721  bgoldbnnsum3prm  48723  pgrple2abl  49298  veronesev1lem  50809  veronesev2lem  50810  veronesev3lem  50811  veronesev4lem  50812  veronesev5lem  50813  veronesev6lem  50814  veronesevrowd  50815  veronesematrowd  50817  veroquadgsumlem  50819  veroquadmodzerod  50820  veroquadnolindfd  50821