Theorem 6re 11885

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 11862	. 2 ⊢ 6 = (5 + 1)
2		5re 11882	. . 3 ⊢ 5 ∈ ℝ
3		1re 10798	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10813	. 2 ⊢ (5 + 1) ∈ ℝ
5	1, 4	eqeltri 2827	1 ⊢ 6 ∈ ℝ

Syntax hints:   ∈ wcel 2112  (class class class)co 7191  ℝcr 10693  1c1 10695   + caddc 10697  5c5 11853  6c6 11854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-i2m1 10762  ax-1ne0 10763  ax-rrecex 10766  ax-cnre 10767

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-iota 6316  df-fv 6366  df-ov 7194  df-2 11858  df-3 11859  df-4 11860  df-5 11861  df-6 11862

This theorem is referenced by:  7re  11888  7pos  11906  4lt6  11977  3lt6  11978  2lt6  11979  1lt6  11980  6lt7  11981  5lt7  11982  6lt8  11988  5lt8  11989  6lt9  11996  5lt9  11997  8th4div3  12015  halfpm6th  12016  div4p1lem1div2  12050  6lt10  12392  5lt10  12393  5recm6rec  12402  bpoly2  15582  bpoly3  15583  efi4p  15661  resin4p  15662  recos4p  15663  ef01bndlem  15708  sin01bnd  15709  cos01bnd  15710  lt6abl  19234  sralem  20168  sravsca  20173  zlmlem  20437  sincos6thpi  25359  pigt3  25361  basellem5  25921  basellem8  25924  basellem9  25925  ppiublem1  26037  ppiublem2  26038  ppiub  26039  chtub  26047  bposlem6  26124  bposlem8  26126  ex-res  28478  zlmds  31580  zlmtset  31581  hgt750lemd  32294  hgt750lem2  32298  hgt750leme  32304  problem4  33293  problem5  33294  gbegt5  44829  gbowgt5  44830  gbowge7  44831  gboge9  44832  sbgoldbwt  44845  sgoldbeven3prm  44851  mogoldbb  44853  sbgoldbo  44855  nnsum3primesle9  44862  nnsum4primesodd  44864  wtgoldbnnsum4prm  44870  bgoldbnnsum3prm  44872  pgrple2abl  45317