Theorem 7re 12386

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 12361	. 2 ⊢ 7 = (6 + 1)
2		6re 12383	. . 3 ⊢ 6 ∈ ℝ
3		1re 11290	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11305	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2840	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2108  (class class class)co 7448  ℝcr 11183  1c1 11185   + caddc 11187  6c6 12352  7c7 12353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-icn 11243  ax-addcl 11244  ax-addrcl 11245  ax-mulcl 11246  ax-mulrcl 11247  ax-i2m1 11252  ax-1ne0 11253  ax-rrecex 11256  ax-cnre 11257

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-2 12356  df-3 12357  df-4 12358  df-5 12359  df-6 12360  df-7 12361

This theorem is referenced by:  8re  12389  8pos  12405  5lt7  12480  4lt7  12481  3lt7  12482  2lt7  12483  1lt7  12484  7lt8  12485  6lt8  12486  7lt9  12493  6lt9  12494  7lt10  12891  6lt10  12892  bposlem8  27353  lgsdir2lem1  27387  hgt750lem2  34629  hgt750leme  34635  problem4  35636  60gcd7e1  41962  lcmineqlem  42009  3lexlogpow5ineq1  42011  3lexlogpow5ineq2  42012  3lexlogpow5ineq4  42013  3lexlogpow5ineq3  42014  aks4d1p1p3  42026  aks4d1p1p2  42027  aks4d1p1p4  42028  aks4d1p1p7  42031  aks4d1p2  42034  aks4d1p3  42035  7rp  42290  mod42tp1mod8  47476  stgoldbwt  47650  sbgoldbwt  47651  nnsum3primesle9  47668  nnsum4primesoddALTV  47671  evengpoap3  47673  bgoldbtbndlem1  47679  bgoldbtbnd  47683