Theorem 7re 11996

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 11971	. 2 ⊢ 7 = (6 + 1)
2		6re 11993	. . 3 ⊢ 6 ∈ ℝ
3		1re 10906	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10921	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2835	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7255  ℝcr 10801  1c1 10803   + caddc 10805  6c6 11962  7c7 11963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-i2m1 10870  ax-1ne0 10871  ax-rrecex 10874  ax-cnre 10875

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-2 11966  df-3 11967  df-4 11968  df-5 11969  df-6 11970  df-7 11971

This theorem is referenced by:  8re  11999  8pos  12015  5lt7  12090  4lt7  12091  3lt7  12092  2lt7  12093  1lt7  12094  7lt8  12095  6lt8  12096  7lt9  12103  6lt9  12104  7lt10  12499  6lt10  12500  bposlem8  26344  lgsdir2lem1  26378  hgt750lem2  32532  hgt750leme  32538  problem4  33526  60gcd7e1  39941  lcmineqlem  39988  3lexlogpow5ineq1  39990  3lexlogpow5ineq2  39991  3lexlogpow5ineq4  39992  3lexlogpow5ineq3  39993  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1p7  40010  aks4d1p2  40013  aks4d1p3  40014  mod42tp1mod8  44942  stgoldbwt  45116  sbgoldbwt  45117  nnsum3primesle9  45134  nnsum4primesoddALTV  45137  evengpoap3  45139  bgoldbtbndlem1  45145  bgoldbtbnd  45149