Theorem 7re 12338

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 12313	. 2 ⊢ 7 = (6 + 1)
2		6re 12335	. . 3 ⊢ 6 ∈ ℝ
3		1re 11240	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11255	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2831	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7410  ℝcr 11133  1c1 11135   + caddc 11137  6c6 12304  7c7 12305

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 2708  ax-1cn 11192  ax-icn 11193  ax-addcl 11194  ax-addrcl 11195  ax-mulcl 11196  ax-mulrcl 11197  ax-i2m1 11202  ax-1ne0 11203  ax-rrecex 11206  ax-cnre 11207

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 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-iota 6489  df-fv 6544  df-ov 7413  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313

This theorem is referenced by:  8re  12341  8pos  12357  5lt7  12432  4lt7  12433  3lt7  12434  2lt7  12435  1lt7  12436  7lt8  12437  6lt8  12438  7lt9  12445  6lt9  12446  7lt10  12846  6lt10  12847  bposlem8  27259  lgsdir2lem1  27293  hgt750lem2  34689  hgt750leme  34695  problem4  35695  60gcd7e1  42023  lcmineqlem  42070  3lexlogpow5ineq1  42072  3lexlogpow5ineq2  42073  3lexlogpow5ineq4  42074  3lexlogpow5ineq3  42075  aks4d1p1p3  42087  aks4d1p1p2  42088  aks4d1p1p4  42089  aks4d1p1p7  42092  aks4d1p2  42095  aks4d1p3  42096  7rp  42318  mod42tp1mod8  47583  stgoldbwt  47757  sbgoldbwt  47758  nnsum3primesle9  47775  nnsum4primesoddALTV  47778  evengpoap3  47780  bgoldbtbndlem1  47786  bgoldbtbnd  47790