Theorem 7re 12049

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 12024	. 2 ⊢ 7 = (6 + 1)
2		6re 12046	. . 3 ⊢ 6 ∈ ℝ
3		1re 10959	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10974	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2836	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7268  ℝcr 10854  1c1 10856   + caddc 10858  6c6 12015  7c7 12016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710  ax-1cn 10913  ax-icn 10914  ax-addcl 10915  ax-addrcl 10916  ax-mulcl 10917  ax-mulrcl 10918  ax-i2m1 10923  ax-1ne0 10924  ax-rrecex 10927  ax-cnre 10928

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-iota 6388  df-fv 6438  df-ov 7271  df-2 12019  df-3 12020  df-4 12021  df-5 12022  df-6 12023  df-7 12024

This theorem is referenced by:  8re  12052  8pos  12068  5lt7  12143  4lt7  12144  3lt7  12145  2lt7  12146  1lt7  12147  7lt8  12148  6lt8  12149  7lt9  12156  6lt9  12157  7lt10  12552  6lt10  12553  bposlem8  26420  lgsdir2lem1  26454  hgt750lem2  32611  hgt750leme  32617  problem4  33605  60gcd7e1  39993  lcmineqlem  40040  3lexlogpow5ineq1  40042  3lexlogpow5ineq2  40043  3lexlogpow5ineq4  40044  3lexlogpow5ineq3  40045  aks4d1p1p3  40057  aks4d1p1p2  40058  aks4d1p1p4  40059  aks4d1p1p7  40062  aks4d1p2  40065  aks4d1p3  40066  mod42tp1mod8  45006  stgoldbwt  45180  sbgoldbwt  45181  nnsum3primesle9  45198  nnsum4primesoddALTV  45201  evengpoap3  45203  bgoldbtbndlem1  45209  bgoldbtbnd  45213