Theorem 7re 12268

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 12243	. 2 ⊢ 7 = (6 + 1)
2		6re 12265	. . 3 ⊢ 6 ∈ ℝ
3		1re 11138	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11154	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2833	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7361  ℝcr 11031  1c1 11033   + caddc 11035  6c6 12234  7c7 12235

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-i2m1 11100  ax-1ne0 11101  ax-rrecex 11104  ax-cnre 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6449  df-fv 6501  df-ov 7364  df-2 12238  df-3 12239  df-4 12240  df-5 12241  df-6 12242  df-7 12243

This theorem is referenced by:  8re  12271  8pos  12287  5lt7  12357  4lt7  12358  3lt7  12359  2lt7  12360  1lt7  12361  7lt8  12362  6lt8  12363  7lt9  12370  6lt9  12371  7lt10  12771  6lt10  12772  bposlem8  27271  lgsdir2lem1  27305  hgt750lem2  34815  hgt750leme  34821  problem4  35869  60gcd7e1  42461  lcmineqlem  42508  3lexlogpow5ineq1  42510  3lexlogpow5ineq2  42511  3lexlogpow5ineq4  42512  3lexlogpow5ineq3  42513  aks4d1p1p3  42525  aks4d1p1p2  42526  aks4d1p1p4  42527  aks4d1p1p7  42530  aks4d1p2  42533  aks4d1p3  42534  7rp  42751  mod42tp1mod8  48080  stgoldbwt  48267  sbgoldbwt  48268  nnsum3primesle9  48285  nnsum4primesoddALTV  48288  evengpoap3  48290  bgoldbtbndlem1  48296  bgoldbtbnd  48300