Theorem 7re 12301

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 12276	. 2 ⊢ 7 = (6 + 1)
2		6re 12298	. . 3 ⊢ 6 ∈ ℝ
3		1re 11210	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11225	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2829	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2106  (class class class)co 7405  ℝcr 11105  1c1 11107   + caddc 11109  6c6 12267  7c7 12268

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-i2m1 11174  ax-1ne0 11175  ax-rrecex 11178  ax-cnre 11179

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276

This theorem is referenced by:  8re  12304  8pos  12320  5lt7  12395  4lt7  12396  3lt7  12397  2lt7  12398  1lt7  12399  7lt8  12400  6lt8  12401  7lt9  12408  6lt9  12409  7lt10  12806  6lt10  12807  bposlem8  26783  lgsdir2lem1  26817  hgt750lem2  33652  hgt750leme  33658  problem4  34641  60gcd7e1  40858  lcmineqlem  40905  3lexlogpow5ineq1  40907  3lexlogpow5ineq2  40908  3lexlogpow5ineq4  40909  3lexlogpow5ineq3  40910  aks4d1p1p3  40922  aks4d1p1p2  40923  aks4d1p1p4  40924  aks4d1p1p7  40927  aks4d1p2  40930  aks4d1p3  40931  mod42tp1mod8  46256  stgoldbwt  46430  sbgoldbwt  46431  nnsum3primesle9  46448  nnsum4primesoddALTV  46451  evengpoap3  46453  bgoldbtbndlem1  46459  bgoldbtbnd  46463