8re - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 8re		Structured version Visualization version GIF version

Theorem 8re 12332

Description: The number 8 is real. (Contributed by NM, 27-May-1999.)

**Assertion**
Ref	Expression
8re	⊢ 8 ∈ ℝ

**Proof of Theorem 8re**
Step	Hyp	Ref	Expression
1		df-8 12305	. 2 ⊢ 8 = (7 + 1)
2		7re 12329	. . 3 ⊢ 7 ∈ ℝ
3		1re 11238	. . 3 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11253	. 2 ⊢ (7 + 1) ∈ ℝ
5	1, 4	eqeltri 2825	1 ⊢ 8 ∈ ℝ

Colors of variables: wff setvar class

Syntax hints: ∈ wcel 2099 (class class class)co 7414 ℝcr 11131 1c1 11133 + caddc 11135 7c7 12296 8c8 12297

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 ax-1cn 11190 ax-icn 11191 ax-addcl 11192 ax-addrcl 11193 ax-mulcl 11194 ax-mulrcl 11195 ax-i2m1 11200 ax-1ne0 11201 ax-rrecex 11204 ax-cnre 11205

This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-3an 1087 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ne 2937 df-ral 3058 df-rex 3067 df-rab 3429 df-v 3472 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4319 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4904 df-br 5143 df-iota 6494 df-fv 6550 df-ov 7417 df-2 12299 df-3 12300 df-4 12301 df-5 12302 df-6 12303 df-7 12304 df-8 12305

This theorem is referenced by: 9re 12335 9pos 12349 6lt8 12429 5lt8 12430 4lt8 12431 3lt8 12432 2lt8 12433 1lt8 12434 8lt9 12435 7lt9 12436 8th4div3 12456 8lt10 12833 7lt10 12834 ef01bndlem 16154 cos2bnd 16158 slotstnscsi 17334 slotsdnscsi 17366 sralemOLD 21055 chtub 27138 bposlem8 27217 bposlem9 27218 lgsdir2lem1 27251 lgsdir2lem4 27254 lgsdir2lem5 27255 2lgsoddprmlem1 27334 2lgsoddprmlem2 27335 chebbnd1lem2 27396 chebbnd1lem3 27397 chebbnd1 27398 pntlemf 27531 cchhllemOLD 28691 hgt750lem 34277 hgt750lem2 34278 hgt750leme 34284 lcmineqlem23 41516 lcmineqlem 41517 3lexlogpow5ineq2 41520 aks4d1p1 41541 resqrtvalex 43069 imsqrtvalex 43070 fmtnoprmfac2lem1 46900 mod42tp1mod8 46936 nnsum3primesle9 47128 nnsum4primesoddALTV 47131 nnsum4primesevenALTV 47135 bgoldbtbndlem1 47139 tgoldbach 47151

	
		OSZAR »