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 12712

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 12690	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12318	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11182	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11198	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11199	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11184	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11198	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2859	1 ⊢ ;10 ∈ ℝ

Colors of variables: wff setvar class

Syntax hints: ∈ wcel 2143 (class class class)co 7397 ℝcr 11073 0cc0 11074 1c1 11075 + caddc 11077 · cmul 11079 9c9 12280 cdc 12689

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1816 ax-4 1830 ax-5 1931 ax-6 1988 ax-7 2029 ax-8 2145 ax-9 2153 ax-ext 2735 ax-1cn 11132 ax-icn 11133 ax-addcl 11134 ax-addrcl 11135 ax-mulcl 11136 ax-mulrcl 11137 ax-i2m1 11142 ax-1ne0 11143 ax-rnegex 11145 ax-rrecex 11146 ax-cnre 11147

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1101 df-tru 1564 df-fal 1574 df-ex 1801 df-sb 2092 df-clab 2742 df-cleq 2755 df-clel 2838 df-ne 2959 df-ral 3078 df-rex 3088 df-rab 3416 df-v 3457 df-dif 3908 df-un 3910 df-ss 3922 df-nul 4287 df-if 4482 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-br 5102 df-iota 6478 df-fv 6530 df-ov 7400 df-2 12281 df-3 12282 df-4 12283 df-5 12284 df-6 12285 df-7 12286 df-8 12287 df-9 12288 df-dec 12690

This theorem is referenced by: 1lt10OLD 12835 0.999... 15912 bpoly4 16090 plendxnocndx 17414 slotsdifdsndx 17424 slotsdifunifndx 17431 slotsdifplendx2 17446 bposlem4 27352 bposlem5 27353 dp2cl 33058 dp2lt10 33062 dp2lt 33063 dp2ltsuc 33064 dp2ltc 33065 dpfrac1 33070 dplti 33083 dpgti 33084 dpexpp1 33086 hgt750lem 34946 problem2 36017 lcmineqlem23 42669 aks4d1p1p7 42692 goldrasin 47477 bgoldbtbndlem1 48428 tgblthelfgott 48438 tgoldbach 48440

W3C validator