Theorem 6re 12302

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 12279	. 2 ⊢ 6 = (5 + 1)
2		5re 12299	. . 3 ⊢ 5 ∈ ℝ
3		1re 11214	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11229	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2830	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2107  (class class class)co 7409  ℝcr 11109  1c1 11111   + caddc 11113  5c5 12270  6c6 12271

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-i2m1 11178  ax-1ne0 11179  ax-rrecex 11182  ax-cnre 11183

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-iota 6496  df-fv 6552  df-ov 7412  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279

This theorem is referenced by:  7re  12305  7pos  12323  4lt6  12394  3lt6  12395  2lt6  12396  1lt6  12397  6lt7  12398  5lt7  12399  6lt8  12405  5lt8  12406  6lt9  12413  5lt9  12414  8th4div3  12432  halfpm6th  12433  div4p1lem1div2  12467  6lt10  12811  5lt10  12812  5recm6rec  12821  bpoly2  16001  bpoly3  16002  efi4p  16080  resin4p  16081  recos4p  16082  ef01bndlem  16127  sin01bnd  16128  cos01bnd  16129  slotsdifipndx  17280  slotstnscsi  17305  plendxnvscandx  17319  slotsdnscsi  17337  lt6abl  19763  sralemOLD  20791  sravscaOLD  20801  zlmlemOLD  21067  sincos6thpi  26025  pigt3  26027  basellem5  26589  basellem8  26592  basellem9  26593  ppiublem1  26705  ppiublem2  26706  ppiub  26707  chtub  26715  bposlem6  26792  bposlem8  26794  slotsinbpsd  27692  slotslnbpsd  27693  ex-res  29694  zlmdsOLD  32943  zlmtsetOLD  32945  hgt750lemd  33660  hgt750lem2  33664  hgt750leme  33670  problem4  34653  problem5  34654  gbegt5  46429  gbowgt5  46430  gbowge7  46431  gboge9  46432  sbgoldbwt  46445  sgoldbeven3prm  46451  mogoldbb  46453  sbgoldbo  46455  nnsum3primesle9  46462  nnsum4primesodd  46464  wtgoldbnnsum4prm  46470  bgoldbnnsum3prm  46472  pgrple2abl  47041