Theorem 6re 11581

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 11558	. 2 ⊢ 6 = (5 + 1)
2		5re 11578	. . 3 ⊢ 5 ∈ ℝ
3		1re 10494	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10509	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2881	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2083  (class class class)co 7023  ℝcr 10389  1c1 10391   + caddc 10393  5c5 11549  6c6 11550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771  ax-1cn 10448  ax-icn 10449  ax-addcl 10450  ax-addrcl 10451  ax-mulcl 10452  ax-mulrcl 10453  ax-i2m1 10458  ax-1ne0 10459  ax-rrecex 10462  ax-cnre 10463

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-br 4969  df-iota 6196  df-fv 6240  df-ov 7026  df-2 11554  df-3 11555  df-4 11556  df-5 11557  df-6 11558

This theorem is referenced by:  7re  11584  7pos  11602  4lt6  11673  3lt6  11674  2lt6  11675  1lt6  11676  6lt7  11677  5lt7  11678  6lt8  11684  5lt8  11685  6lt9  11692  5lt9  11693  8th4div3  11711  halfpm6th  11712  div4p1lem1div2  11746  6lt10  12086  5lt10  12087  5recm6rec  12096  bpoly2  15248  bpoly3  15249  efi4p  15327  resin4p  15328  recos4p  15329  ef01bndlem  15374  sin01bnd  15375  cos01bnd  15376  lt6abl  18740  sralem  19643  sravsca  19648  zlmlem  20350  sincos6thpi  24788  pigt3  24790  basellem5  25348  basellem8  25351  basellem9  25352  ppiublem1  25464  ppiublem2  25465  ppiub  25466  chtub  25474  bposlem6  25551  bposlem8  25553  ex-res  27908  zlmds  30818  zlmtset  30819  hgt750lemd  31532  hgt750lem2  31536  hgt750leme  31542  problem4  32521  problem5  32522  gbegt5  43430  gbowgt5  43431  gbowge7  43432  gboge9  43433  sbgoldbwt  43446  sgoldbeven3prm  43452  mogoldbb  43454  sbgoldbo  43456  nnsum3primesle9  43463  nnsum4primesodd  43465  wtgoldbnnsum4prm  43471  bgoldbnnsum3prm  43473  pgrple2abl  43915