Theorem 7re 12446

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 12420	. 2 ⊢ 7 = (6 + 1)
2		6re 12443	. . 3 ⊢ 6 ∈ ℝ
3		1re 11318	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11334	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2859	1 ⊢ 7 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2146  (class class class)co 7427  ℝcr 11209  1c1 11211   + caddc 11213  6c6 12411  7c7 12412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-1cn 11268  ax-icn 11269  ax-addcl 11270  ax-addrcl 11271  ax-mulcl 11272  ax-mulrcl 11273  ax-i2m1 11278  ax-1ne0 11279  ax-rrecex 11282  ax-cnre 11283

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-ss 3900  df-dif 4049  df-un 4153  df-nul 4281  df-if 4485  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-iota 6500  df-fv 6554  df-ov 7430  df-2 12415  df-3 12416  df-4 12417  df-5 12418  df-6 12419  df-7 12420

This theorem is used by:  8re  12449  5lt7  12542  4lt7  12543  3lt7  12544  2lt7  12545  1lt7  12546  7lt8  12547  6lt8  12548  7lt9  12555  6lt9  12556  7lt10  12963  bposlem8  27630  lgsdir2lem1  27664  hgt750lem2  35334  hgt750leme  35340  problem4  36554  60gcd7e1  43195  lcmineqlem  43242  3lexlogpow5ineq1  43244  3lexlogpow5ineq2  43245  3lexlogpow5ineq4  43246  3lexlogpow5ineq3  43247  aks4d1p1p3  43259  aks4d1p1p2  43260  aks4d1p1p4  43261  aks4d1p1p7  43264  aks4d1p2  43267  aks4d1p3  43268  7rp  43499  mod42tp1mod8  48826  stgoldbwt  49013  sbgoldbwt  49014  nnsum3primesle9  49031  nnsum4primesoddALTV  49034  evengpoap3  49036  bgoldbtbndlem1  49042  bgoldbtbnd  49046