Theorem 7re 12329

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 12303	. 2 ⊢ 7 = (6 + 1)
2		6re 12326	. . 3 ⊢ 6 ∈ ℝ
3		1re 11203	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11219	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2859	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2143  (class class class)co 7410  ℝcr 11094  1c1 11096   + caddc 11098  6c6 12294  7c7 12295

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-i2m1 11163  ax-1ne0 11164  ax-rrecex 11167  ax-cnre 11168

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-2 12298  df-3 12299  df-4 12300  df-5 12301  df-6 12302  df-7 12303

This theorem is referenced by:  8re  12332  5lt7  12425  4lt7  12426  3lt7  12427  2lt7  12428  1lt7  12429  7lt8  12430  6lt8  12431  7lt9  12438  6lt9  12439  7lt10  12845  bposlem8  27455  lgsdir2lem1  27489  hgt750lem2  35039  hgt750leme  35045  problem4  36160  60gcd7e1  42792  lcmineqlem  42839  3lexlogpow5ineq1  42841  3lexlogpow5ineq2  42842  3lexlogpow5ineq4  42843  3lexlogpow5ineq3  42844  aks4d1p1p3  42856  aks4d1p1p2  42857  aks4d1p1p4  42858  aks4d1p1p7  42861  aks4d1p2  42864  aks4d1p3  42865  7rp  43083  mod42tp1mod8  48374  stgoldbwt  48561  sbgoldbwt  48562  nnsum3primesle9  48579  nnsum4primesoddALTV  48582  evengpoap3  48584  bgoldbtbndlem1  48590  bgoldbtbnd  48594