Theorem 7re 11410

Description: The number 7 is real. (Contributed by NM, 27-May-1999.)

Assertion

Ref	Expression
7re	⊢ 7 ∈ ℝ

Proof of Theorem 7re

Step	Hyp	Ref	Expression
1		df-7 11381	. 2 ⊢ 7 = (6 + 1)
2		6re 11406	. . 3 ⊢ 6 ∈ ℝ
3		1re 10328	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10344	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2874	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2157  (class class class)co 6878  ℝcr 10223  1c1 10225   + caddc 10227  6c6 11372  7c7 11373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-1cn 10282  ax-icn 10283  ax-addcl 10284  ax-addrcl 10285  ax-mulcl 10286  ax-mulrcl 10287  ax-i2m1 10292  ax-1ne0 10293  ax-rrecex 10296  ax-cnre 10297

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ne 2972  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-iota 6064  df-fv 6109  df-ov 6881  df-2 11376  df-3 11377  df-4 11378  df-5 11379  df-6 11380  df-7 11381

This theorem is referenced by:  7cnOLD  11412  8re  11414  8pos  11432  5lt7  11507  4lt7  11508  3lt7  11509  2lt7  11510  1lt7  11511  7lt8  11512  6lt8  11513  7lt9  11520  6lt9  11521  7lt10  11918  6lt10  11919  bposlem8  25368  lgsdir2lem1  25402  hgt750lem2  31250  hgt750leme  31256  problem4  32077  mod42tp1mod8  42301  stgoldbwt  42446  sbgoldbwt  42447  nnsum3primesle9  42464  nnsum4primesoddALTV  42467  evengpoap3  42469  bgoldbtbndlem1  42475  bgoldbtbnd  42479