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 12837

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 12815	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12442	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11308	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11324	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11325	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11310	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11324	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2856	1 ⊢ ;10 ∈ ℝ

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∈ wcel 2144 (class class class)co 7420 ℝcr 11199 0cc0 11200 1c1 11201 + caddc 11203 · cmul 11205 9c9 12404 cdc 12814

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-ext 2732 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-i2m1 11268 ax-1ne0 11269 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-sb 2099 df-clab 2739 df-cleq 2752 df-clel 2835 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-ss 3896 df-dif 4047 df-un 4151 df-nul 4279 df-if 4482 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-br 5103 df-iota 6494 df-fv 6546 df-ov 7423 df-2 12405 df-3 12406 df-4 12407 df-5 12408 df-6 12409 df-7 12410 df-8 12411 df-9 12412 df-dec 12815

This theorem is used by: 1lt10OLD 12960 0.999... 16050 bpoly4 16225 plendxnocndx 17555 slotsdifdsndx 17565 slotsdifunifndx 17572 slotsdifplendx2 17587 bposlem4 27614 bposlem5 27615 dp2cl 33446 dp2lt10 33450 dp2lt 33451 dp2ltsuc 33452 dp2ltc 33453 dpfrac1 33458 dplti 33471 dpgti 33472 dpexpp1 33474 hgt750lem 35280 problem2 36431 lcmineqlem23 43102 aks4d1p1p7 43125 goldrasin 47929 bgoldbtbndlem1 48903 tgblthelfgott 48913 tgoldbach 48915

W3C validator