Theorem 7re 12360

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 12335	. 2 ⊢ 7 = (6 + 1)
2		6re 12357	. . 3 ⊢ 6 ∈ ℝ
3		1re 11262	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11277	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2836	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2107  (class class class)co 7432  ℝcr 11155  1c1 11157   + caddc 11159  6c6 12326  7c7 12327

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-i2m1 11224  ax-1ne0 11225  ax-rrecex 11228  ax-cnre 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-iota 6513  df-fv 6568  df-ov 7435  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335

This theorem is referenced by:  8re  12363  8pos  12379  5lt7  12454  4lt7  12455  3lt7  12456  2lt7  12457  1lt7  12458  7lt8  12459  6lt8  12460  7lt9  12467  6lt9  12468  7lt10  12868  6lt10  12869  bposlem8  27336  lgsdir2lem1  27370  hgt750lem2  34668  hgt750leme  34674  problem4  35674  60gcd7e1  42007  lcmineqlem  42054  3lexlogpow5ineq1  42056  3lexlogpow5ineq2  42057  3lexlogpow5ineq4  42058  3lexlogpow5ineq3  42059  aks4d1p1p3  42071  aks4d1p1p2  42072  aks4d1p1p4  42073  aks4d1p1p7  42076  aks4d1p2  42079  aks4d1p3  42080  7rp  42341  mod42tp1mod8  47594  stgoldbwt  47768  sbgoldbwt  47769  nnsum3primesle9  47786  nnsum4primesoddALTV  47789  evengpoap3  47791  bgoldbtbndlem1  47797  bgoldbtbnd  47801