10re - Metamath Proof Explorer

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

Theorem 10re 12861

Description: The number 10 is real. (Contributed by NM, 5-Feb-2007.) (Revised by AV, 8-Sep-2021.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 8-Oct-2022.)

**Assertion**
Ref	Expression
10re	⊢ ;10 ∈ ℝ

**Proof of Theorem 10re**
Step	Hyp	Ref	Expression
1		df-dec 12839	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12466	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11332	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11348	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11349	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11334	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11348	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2860	1 ⊢ ;10 ∈ ℝ

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∈ wcel 2147 (class class class)co 7440 ℝcr 11223 0cc0 11224 1c1 11225 + caddc 11227 · cmul 11229 9c9 12428 cdc 12838

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 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-i2m1 11292 ax-1ne0 11293 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297

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 4839 df-uni 4871 df-br 5107 df-iota 6509 df-fv 6563 df-ov 7443 df-2 12429 df-3 12430 df-4 12431 df-5 12432 df-6 12433 df-7 12434 df-8 12435 df-9 12436 df-dec 12839

This theorem is used by: 1lt10OLD 12984 0.999... 16076 bpoly4 16251 plendxnocndx 17581 slotsdifdsndx 17591 slotsdifunifndx 17598 slotsdifplendx2 17613 bposlem4 27641 bposlem5 27642 dp2cl 33513 dp2lt10 33517 dp2lt 33518 dp2ltsuc 33519 dp2ltc 33520 dpfrac1 33525 dplti 33538 dpgti 33539 dpexpp1 33541 hgt750lem 35347 problem2 36597 lcmineqlem23 43292 aks4d1p1p7 43315 goldrasin 48132 bgoldbtbndlem1 49106 tgblthelfgott 49116 tgoldbach 49118

W3C validator