Theorem 6re 11139

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 11121	. 2 ⊢ 6 = (5 + 1)
2		5re 11137	. . 3 ⊢ 5 ∈ ℝ
3		1re 10077	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10091	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2726	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2030  (class class class)co 6690  ℝcr 9973  1c1 9975   + caddc 9977  5c5 11111  6c6 11112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rrecex 10046  ax-cnre 10047

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121

This theorem is referenced by:  6cn  11140  7re  11141  7pos  11158  4lt6  11243  3lt6  11244  2lt6  11245  1lt6  11246  6lt7  11247  5lt7  11248  6lt8  11254  5lt8  11255  6lt9  11262  5lt9  11263  6lt10OLD  11271  5lt10OLD  11272  8th4div3  11290  halfpm6th  11291  div4p1lem1div2  11325  6lt10  11714  5lt10  11715  5recm6rec  11724  bpoly2  14832  bpoly3  14833  efi4p  14911  resin4p  14912  recos4p  14913  ef01bndlem  14958  sin01bnd  14959  cos01bnd  14960  lt6abl  18342  sralem  19225  sravsca  19230  zlmlem  19913  sincos6thpi  24312  basellem5  24856  basellem8  24859  basellem9  24860  ppiublem1  24972  ppiublem2  24973  ppiub  24974  chtub  24982  bposlem6  25059  bposlem8  25061  ex-res  27428  zlmds  30136  zlmtset  30137  hgt750lemd  30854  hgt750lem2  30858  hgt750leme  30864  problem4  31688  problem5  31689  pigt3  33532  gbegt5  41974  gbowgt5  41975  gbowge7  41976  gboge9  41977  sbgoldbwt  41990  sgoldbeven3prm  41996  mogoldbb  41998  sbgoldbo  42000  nnsum3primesle9  42007  nnsum4primesodd  42009  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  pgrple2abl  42471