Theorem 7re 12221

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 12196	. 2 ⊢ 7 = (6 + 1)
2		6re 12218	. . 3 ⊢ 6 ∈ ℝ
3		1re 11115	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11130	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2824	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7349  ℝcr 11008  1c1 11010   + caddc 11012  6c6 12187  7c7 12188

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 2701  ax-1cn 11067  ax-icn 11068  ax-addcl 11069  ax-addrcl 11070  ax-mulcl 11071  ax-mulrcl 11072  ax-i2m1 11077  ax-1ne0 11078  ax-rrecex 11081  ax-cnre 11082

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 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-2 12191  df-3 12192  df-4 12193  df-5 12194  df-6 12195  df-7 12196

This theorem is referenced by:  8re  12224  8pos  12240  5lt7  12310  4lt7  12311  3lt7  12312  2lt7  12313  1lt7  12314  7lt8  12315  6lt8  12316  7lt9  12323  6lt9  12324  7lt10  12724  6lt10  12725  bposlem8  27200  lgsdir2lem1  27234  hgt750lem2  34626  hgt750leme  34632  problem4  35651  60gcd7e1  41988  lcmineqlem  42035  3lexlogpow5ineq1  42037  3lexlogpow5ineq2  42038  3lexlogpow5ineq4  42039  3lexlogpow5ineq3  42040  aks4d1p1p3  42052  aks4d1p1p2  42053  aks4d1p1p4  42054  aks4d1p1p7  42057  aks4d1p2  42060  aks4d1p3  42061  7rp  42285  mod42tp1mod8  47596  stgoldbwt  47770  sbgoldbwt  47771  nnsum3primesle9  47788  nnsum4primesoddALTV  47791  evengpoap3  47793  bgoldbtbndlem1  47799  bgoldbtbnd  47803