Theorem 7re 11309

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 11290	. 2 ⊢ 7 = (6 + 1)
2		6re 11307	. . 3 ⊢ 6 ∈ ℝ
3		1re 10245	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 10259	. 2 ⊢ (6 + 1) ∈ ℝ
5	1, 4	eqeltri 2846	1 ⊢ 7 ∈ ℝ

Syntax hints:   ∈ wcel 2145  (class class class)co 6796  ℝcr 10141  1c1 10143   + caddc 10145  6c6 11280  7c7 11281

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-1cn 10200  ax-icn 10201  ax-addcl 10202  ax-addrcl 10203  ax-mulcl 10204  ax-mulrcl 10205  ax-i2m1 10210  ax-1ne0 10211  ax-rrecex 10214  ax-cnre 10215

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-iota 5993  df-fv 6038  df-ov 6799  df-2 11285  df-3 11286  df-4 11287  df-5 11288  df-6 11289  df-7 11290

This theorem is referenced by:  7cn  11310  8re  11311  8pos  11327  5lt7  11417  4lt7  11418  3lt7  11419  2lt7  11420  1lt7  11421  7lt8  11422  6lt8  11423  7lt9  11430  6lt9  11431  7lt10OLD  11439  6lt10OLD  11440  7lt10  11881  6lt10  11882  bposlem8  25237  lgsdir2lem1  25271  hgt750lem2  31070  hgt750leme  31076  problem4  31900  mod42tp1mod8  42044  stgoldbwt  42189  sbgoldbwt  42190  nnsum3primesle9  42207  nnsum4primesoddALTV  42210  evengpoap3  42212  bgoldbtbndlem1  42218  bgoldbtbnd  42222