Theorem 7re 11583

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 11558	. 2 ⊢ 7 = (6 + 1)
2		6re 11580	. . 3 ⊢ 6 ∈ ℝ
3		1re 10492	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10507	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2879	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2081  (class class class)co 7021  ℝcr 10387  1c1 10389   + caddc 10391  6c6 11549  7c7 11550

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769  ax-1cn 10446  ax-icn 10447  ax-addcl 10448  ax-addrcl 10449  ax-mulcl 10450  ax-mulrcl 10451  ax-i2m1 10456  ax-1ne0 10457  ax-rrecex 10460  ax-cnre 10461

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-iota 6194  df-fv 6238  df-ov 7024  df-2 11553  df-3 11554  df-4 11555  df-5 11556  df-6 11557  df-7 11558

This theorem is referenced by:  8re  11586  8pos  11602  5lt7  11677  4lt7  11678  3lt7  11679  2lt7  11680  1lt7  11681  7lt8  11682  6lt8  11683  7lt9  11690  6lt9  11691  7lt10  12086  6lt10  12087  bposlem8  25554  lgsdir2lem1  25588  hgt750lem2  31545  hgt750leme  31551  problem4  32525  mod42tp1mod8  43275  stgoldbwt  43449  sbgoldbwt  43450  nnsum3primesle9  43467  nnsum4primesoddALTV  43470  evengpoap3  43472  bgoldbtbndlem1  43478  bgoldbtbnd  43482