Theorem 7re 12362

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 12336	. 2 ⊢ 7 = (6 + 1)
2		6re 12359	. . 3 ⊢ 6 ∈ ℝ
3		1re 11236	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11252	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2858	1 ⊢ 7 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7417  ℝcr 11127  1c1 11129   + caddc 11131  6c6 12327  7c7 12328

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-1cn 11186  ax-icn 11187  ax-addcl 11188  ax-addrcl 11189  ax-mulcl 11190  ax-mulrcl 11191  ax-i2m1 11196  ax-1ne0 11197  ax-rrecex 11200  ax-cnre 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7420  df-2 12331  df-3 12332  df-4 12333  df-5 12334  df-6 12335  df-7 12336

This theorem is used by:  8re  12365  5lt7  12458  4lt7  12459  3lt7  12460  2lt7  12461  1lt7  12462  7lt8  12463  6lt8  12464  7lt9  12471  6lt9  12472  7lt10  12879  bposlem8  27535  lgsdir2lem1  27569  hgt750lem2  35168  hgt750leme  35174  problem4  36255  60gcd7e1  42879  lcmineqlem  42926  3lexlogpow5ineq1  42928  3lexlogpow5ineq2  42929  3lexlogpow5ineq4  42930  3lexlogpow5ineq3  42931  aks4d1p1p3  42943  aks4d1p1p2  42944  aks4d1p1p4  42945  aks4d1p1p7  42948  aks4d1p2  42951  aks4d1p3  42952  7rp  43185  mod42tp1mod8  48513  stgoldbwt  48700  sbgoldbwt  48701  nnsum3primesle9  48718  nnsum4primesoddALTV  48721  evengpoap3  48723  bgoldbtbndlem1  48729  bgoldbtbnd  48733