Theorem 7re 12436

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 12410	. 2 ⊢ 7 = (6 + 1)
2		6re 12433	. . 3 ⊢ 6 ∈ ℝ
3		1re 11308	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11324	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2857	1 ⊢ 7 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2145  (class class class)co 7420  ℝcr 11199  1c1 11201   + caddc 11203  6c6 12401  7c7 12402

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 2733  ax-1cn 11258  ax-icn 11259  ax-addcl 11260  ax-addrcl 11261  ax-mulcl 11262  ax-mulrcl 11263  ax-i2m1 11268  ax-1ne0 11269  ax-rrecex 11272  ax-cnre 11273

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 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 6494  df-fv 6546  df-ov 7423  df-2 12405  df-3 12406  df-4 12407  df-5 12408  df-6 12409  df-7 12410

This theorem is used by:  8re  12439  5lt7  12532  4lt7  12533  3lt7  12534  2lt7  12535  1lt7  12536  7lt8  12537  6lt8  12538  7lt9  12545  6lt9  12546  7lt10  12953  bposlem8  27618  lgsdir2lem1  27652  hgt750lem2  35281  hgt750leme  35287  problem4  36433  60gcd7e1  43055  lcmineqlem  43102  3lexlogpow5ineq1  43104  3lexlogpow5ineq2  43105  3lexlogpow5ineq4  43106  3lexlogpow5ineq3  43107  aks4d1p1p3  43119  aks4d1p1p2  43120  aks4d1p1p4  43121  aks4d1p1p7  43124  aks4d1p2  43127  aks4d1p3  43128  7rp  43359  mod42tp1mod8  48686  stgoldbwt  48873  sbgoldbwt  48874  nnsum3primesle9  48891  nnsum4primesoddALTV  48894  evengpoap3  48896  bgoldbtbndlem1  48902  bgoldbtbnd  48906