Theorem 7re 12286

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 12261	. 2 ⊢ 7 = (6 + 1)
2		6re 12283	. . 3 ⊢ 6 ∈ ℝ
3		1re 11181	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11196	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2825	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2109  (class class class)co 7390  ℝcr 11074  1c1 11076   + caddc 11078  6c6 12252  7c7 12253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-i2m1 11143  ax-1ne0 11144  ax-rrecex 11147  ax-cnre 11148

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-2 12256  df-3 12257  df-4 12258  df-5 12259  df-6 12260  df-7 12261

This theorem is referenced by:  8re  12289  8pos  12305  5lt7  12375  4lt7  12376  3lt7  12377  2lt7  12378  1lt7  12379  7lt8  12380  6lt8  12381  7lt9  12388  6lt9  12389  7lt10  12789  6lt10  12790  bposlem8  27209  lgsdir2lem1  27243  hgt750lem2  34650  hgt750leme  34656  problem4  35662  60gcd7e1  42000  lcmineqlem  42047  3lexlogpow5ineq1  42049  3lexlogpow5ineq2  42050  3lexlogpow5ineq4  42051  3lexlogpow5ineq3  42052  aks4d1p1p3  42064  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p7  42069  aks4d1p2  42072  aks4d1p3  42073  7rp  42297  mod42tp1mod8  47607  stgoldbwt  47781  sbgoldbwt  47782  nnsum3primesle9  47799  nnsum4primesoddALTV  47802  evengpoap3  47804  bgoldbtbndlem1  47810  bgoldbtbnd  47814