Theorem 7re 12274

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 12249	. 2 ⊢ 7 = (6 + 1)
2		6re 12271	. . 3 ⊢ 6 ∈ ℝ
3		1re 11144	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11160	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2832	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2114  (class class class)co 7367  ℝcr 11037  1c1 11039   + caddc 11041  6c6 12240  7c7 12241

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-2 12244  df-3 12245  df-4 12246  df-5 12247  df-6 12248  df-7 12249

This theorem is referenced by:  8re  12277  8pos  12293  5lt7  12363  4lt7  12364  3lt7  12365  2lt7  12366  1lt7  12367  7lt8  12368  6lt8  12369  7lt9  12376  6lt9  12377  7lt10  12777  6lt10  12778  bposlem8  27254  lgsdir2lem1  27288  hgt750lem2  34796  hgt750leme  34802  problem4  35850  60gcd7e1  42444  lcmineqlem  42491  3lexlogpow5ineq1  42493  3lexlogpow5ineq2  42494  3lexlogpow5ineq4  42495  3lexlogpow5ineq3  42496  aks4d1p1p3  42508  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1p7  42513  aks4d1p2  42516  aks4d1p3  42517  7rp  42734  mod42tp1mod8  48065  stgoldbwt  48252  sbgoldbwt  48253  nnsum3primesle9  48270  nnsum4primesoddALTV  48273  evengpoap3  48275  bgoldbtbndlem1  48281  bgoldbtbnd  48285