Theorem 7re 12311

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 12285	. 2 ⊢ 7 = (6 + 1)
2		6re 12308	. . 3 ⊢ 6 ∈ ℝ
3		1re 11181	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11197	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2858	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2142  (class class class)co 7396  ℝcr 11072  1c1 11074   + caddc 11076  6c6 12276  7c7 12277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-1cn 11131  ax-icn 11132  ax-addcl 11133  ax-addrcl 11134  ax-mulcl 11135  ax-mulrcl 11136  ax-i2m1 11141  ax-1ne0 11142  ax-rrecex 11145  ax-cnre 11146

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284  df-7 12285

This theorem is referenced by:  8re  12314  5lt7  12407  4lt7  12408  3lt7  12409  2lt7  12410  1lt7  12411  7lt8  12412  6lt8  12413  7lt9  12420  6lt9  12421  7lt10  12827  bposlem8  27355  lgsdir2lem1  27389  hgt750lem2  34946  hgt750leme  34952  problem4  36018  60gcd7e1  42622  lcmineqlem  42669  3lexlogpow5ineq1  42671  3lexlogpow5ineq2  42672  3lexlogpow5ineq4  42673  3lexlogpow5ineq3  42674  aks4d1p1p3  42686  aks4d1p1p2  42687  aks4d1p1p4  42688  aks4d1p1p7  42691  aks4d1p2  42694  aks4d1p3  42695  7rp  42911  mod42tp1mod8  48211  stgoldbwt  48398  sbgoldbwt  48399  nnsum3primesle9  48416  nnsum4primesoddALTV  48419  evengpoap3  48421  bgoldbtbndlem1  48427  bgoldbtbnd  48431