Theorem 7re 12279

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 12254	. 2 ⊢ 7 = (6 + 1)
2		6re 12276	. . 3 ⊢ 6 ∈ ℝ
3		1re 11174	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11189	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7387  ℝcr 11067  1c1 11069   + caddc 11071  6c6 12245  7c7 12246

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rrecex 11140  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-2 12249  df-3 12250  df-4 12251  df-5 12252  df-6 12253  df-7 12254

This theorem is referenced by:  8re  12282  8pos  12298  5lt7  12368  4lt7  12369  3lt7  12370  2lt7  12371  1lt7  12372  7lt8  12373  6lt8  12374  7lt9  12381  6lt9  12382  7lt10  12782  6lt10  12783  bposlem8  27202  lgsdir2lem1  27236  hgt750lem2  34643  hgt750leme  34649  problem4  35655  60gcd7e1  41993  lcmineqlem  42040  3lexlogpow5ineq1  42042  3lexlogpow5ineq2  42043  3lexlogpow5ineq4  42044  3lexlogpow5ineq3  42045  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p7  42062  aks4d1p2  42065  aks4d1p3  42066  7rp  42290  mod42tp1mod8  47603  stgoldbwt  47777  sbgoldbwt  47778  nnsum3primesle9  47795  nnsum4primesoddALTV  47798  evengpoap3  47800  bgoldbtbndlem1  47806  bgoldbtbnd  47810