Theorem 7re 12361

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 12335	. 2 ⊢ 7 = (6 + 1)
2		6re 12358	. . 3 ⊢ 6 ∈ ℝ
3		1re 11235	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11251	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2856	1 ⊢ 7 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7414  ℝcr 11126  1c1 11128   + caddc 11130  6c6 12326  7c7 12327

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 2732  ax-1cn 11185  ax-icn 11186  ax-addcl 11187  ax-addrcl 11188  ax-mulcl 11189  ax-mulrcl 11190  ax-i2m1 11195  ax-1ne0 11196  ax-rrecex 11199  ax-cnre 11200

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 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335

This theorem is used by:  8re  12364  5lt7  12457  4lt7  12458  3lt7  12459  2lt7  12460  1lt7  12461  7lt8  12462  6lt8  12463  7lt9  12470  6lt9  12471  7lt10  12878  bposlem8  27530  lgsdir2lem1  27564  hgt750lem2  35163  hgt750leme  35169  problem4  36250  60gcd7e1  42874  lcmineqlem  42921  3lexlogpow5ineq1  42923  3lexlogpow5ineq2  42924  3lexlogpow5ineq4  42925  3lexlogpow5ineq3  42926  aks4d1p1p3  42938  aks4d1p1p2  42939  aks4d1p1p4  42940  aks4d1p1p7  42943  aks4d1p2  42946  aks4d1p3  42947  7rp  43180  mod42tp1mod8  48508  stgoldbwt  48695  sbgoldbwt  48696  nnsum3primesle9  48713  nnsum4primesoddALTV  48716  evengpoap3  48718  bgoldbtbndlem1  48724  bgoldbtbnd  48728