Theorem 7re 12238

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 12213	. 2 ⊢ 7 = (6 + 1)
2		6re 12235	. . 3 ⊢ 6 ∈ ℝ
3		1re 11132	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11147	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2832	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2113  (class class class)co 7358  ℝcr 11025  1c1 11027   + caddc 11029  6c6 12204  7c7 12205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-icn 11085  ax-addcl 11086  ax-addrcl 11087  ax-mulcl 11088  ax-mulrcl 11089  ax-i2m1 11094  ax-1ne0 11095  ax-rrecex 11098  ax-cnre 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-2 12208  df-3 12209  df-4 12210  df-5 12211  df-6 12212  df-7 12213

This theorem is referenced by:  8re  12241  8pos  12257  5lt7  12327  4lt7  12328  3lt7  12329  2lt7  12330  1lt7  12331  7lt8  12332  6lt8  12333  7lt9  12340  6lt9  12341  7lt10  12740  6lt10  12741  bposlem8  27258  lgsdir2lem1  27292  hgt750lem2  34809  hgt750leme  34815  problem4  35862  60gcd7e1  42269  lcmineqlem  42316  3lexlogpow5ineq1  42318  3lexlogpow5ineq2  42319  3lexlogpow5ineq4  42320  3lexlogpow5ineq3  42321  aks4d1p1p3  42333  aks4d1p1p2  42334  aks4d1p1p4  42335  aks4d1p1p7  42338  aks4d1p2  42341  aks4d1p3  42342  7rp  42567  mod42tp1mod8  47858  stgoldbwt  48032  sbgoldbwt  48033  nnsum3primesle9  48050  nnsum4primesoddALTV  48053  evengpoap3  48055  bgoldbtbndlem1  48061  bgoldbtbnd  48065