Theorem 7re 12338

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 12313	. 2 ⊢ 7 = (6 + 1)
2		6re 12335	. . 3 ⊢ 6 ∈ ℝ
3		1re 11246	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11261	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2821	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2098  (class class class)co 7419  ℝcr 11139  1c1 11141   + caddc 11143  6c6 12304  7c7 12305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-1cn 11198  ax-icn 11199  ax-addcl 11200  ax-addrcl 11201  ax-mulcl 11202  ax-mulrcl 11203  ax-i2m1 11208  ax-1ne0 11209  ax-rrecex 11212  ax-cnre 11213

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-ne 2930  df-ral 3051  df-rex 3060  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-iota 6501  df-fv 6557  df-ov 7422  df-2 12308  df-3 12309  df-4 12310  df-5 12311  df-6 12312  df-7 12313

This theorem is referenced by:  8re  12341  8pos  12357  5lt7  12432  4lt7  12433  3lt7  12434  2lt7  12435  1lt7  12436  7lt8  12437  6lt8  12438  7lt9  12445  6lt9  12446  7lt10  12843  6lt10  12844  bposlem8  27269  lgsdir2lem1  27303  hgt750lem2  34415  hgt750leme  34421  problem4  35403  60gcd7e1  41608  lcmineqlem  41655  3lexlogpow5ineq1  41657  3lexlogpow5ineq2  41658  3lexlogpow5ineq4  41659  3lexlogpow5ineq3  41660  aks4d1p1p3  41672  aks4d1p1p2  41673  aks4d1p1p4  41674  aks4d1p1p7  41677  aks4d1p2  41680  aks4d1p3  41681  mod42tp1mod8  47079  stgoldbwt  47253  sbgoldbwt  47254  nnsum3primesle9  47271  nnsum4primesoddALTV  47274  evengpoap3  47276  bgoldbtbndlem1  47282  bgoldbtbnd  47286