Theorem 7re 12225

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 12200	. 2 ⊢ 7 = (6 + 1)
2		6re 12222	. . 3 ⊢ 6 ∈ ℝ
3		1re 11119	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11134	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2829	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7352  ℝcr 11012  1c1 11014   + caddc 11016  6c6 12191  7c7 12192

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-1cn 11071  ax-icn 11072  ax-addcl 11073  ax-addrcl 11074  ax-mulcl 11075  ax-mulrcl 11076  ax-i2m1 11081  ax-1ne0 11082  ax-rrecex 11085  ax-cnre 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-iota 6442  df-fv 6494  df-ov 7355  df-2 12195  df-3 12196  df-4 12197  df-5 12198  df-6 12199  df-7 12200

This theorem is referenced by:  8re  12228  8pos  12244  5lt7  12314  4lt7  12315  3lt7  12316  2lt7  12317  1lt7  12318  7lt8  12319  6lt8  12320  7lt9  12327  6lt9  12328  7lt10  12727  6lt10  12728  bposlem8  27230  lgsdir2lem1  27264  hgt750lem2  34686  hgt750leme  34692  problem4  35733  60gcd7e1  42118  lcmineqlem  42165  3lexlogpow5ineq1  42167  3lexlogpow5ineq2  42168  3lexlogpow5ineq4  42169  3lexlogpow5ineq3  42170  aks4d1p1p3  42182  aks4d1p1p2  42183  aks4d1p1p4  42184  aks4d1p1p7  42187  aks4d1p2  42190  aks4d1p3  42191  7rp  42420  mod42tp1mod8  47726  stgoldbwt  47900  sbgoldbwt  47901  nnsum3primesle9  47918  nnsum4primesoddALTV  47921  evengpoap3  47923  bgoldbtbndlem1  47929  bgoldbtbnd  47933