Theorem 7re 12476

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 12450	. 2 ⊢ 7 = (6 + 1)
2		6re 12473	. . 3 ⊢ 6 ∈ ℝ
3		1re 11347	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11363	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2860	1 ⊢ 7 ∈ ℝ

This proof depends on syntax axioms:   ∈ wcel 2147  (class class class)co 7451  ℝcr 11238  1c1 11240   + caddc 11242  6c6 12441  7c7 12442

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-i2m1 11307  ax-1ne0 11308  ax-rrecex 11311  ax-cnre 11312

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-2 12445  df-3 12446  df-4 12447  df-5 12448  df-6 12449  df-7 12450

This theorem is used by:  8re  12479  5lt7  12572  4lt7  12573  3lt7  12574  2lt7  12575  1lt7  12576  7lt8  12577  6lt8  12578  7lt9  12585  6lt9  12586  7lt10  12993  bposlem8  27675  lgsdir2lem1  27709  hgt750lem2  35392  hgt750leme  35398  problem4  36641  60gcd7e1  43321  lcmineqlem  43368  3lexlogpow5ineq1  43370  3lexlogpow5ineq2  43371  3lexlogpow5ineq4  43372  3lexlogpow5ineq3  43373  aks4d1p1p3  43385  aks4d1p1p2  43386  aks4d1p1p4  43387  aks4d1p1p7  43390  aks4d1p2  43393  aks4d1p3  43394  7rp  43625  mod42tp1mod8  48960  stgoldbwt  49147  sbgoldbwt  49148  nnsum3primesle9  49165  nnsum4primesoddALTV  49168  evengpoap3  49170  bgoldbtbndlem1  49176  bgoldbtbnd  49180