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 12706

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 12684	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12312	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11176	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11192	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11193	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11178	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11192	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2857	1 ⊢ ;10 ∈ ℝ

Colors of variables: wff setvar class

Syntax hints: ∈ wcel 2141 (class class class)co 7390 ℝcr 11067 0cc0 11068 1c1 11069 + caddc 11071 · cmul 11073 9c9 12274 cdc 12683

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-ext 2733 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-i2m1 11136 ax-1ne0 11137 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-sb 2090 df-clab 2740 df-cleq 2753 df-clel 2836 df-ne 2957 df-ral 3076 df-rex 3086 df-rab 3414 df-v 3455 df-dif 3907 df-un 3909 df-ss 3921 df-nul 4286 df-if 4480 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-br 5100 df-iota 6471 df-fv 6523 df-ov 7393 df-2 12275 df-3 12276 df-4 12277 df-5 12278 df-6 12279 df-7 12280 df-8 12281 df-9 12282 df-dec 12684

This theorem is referenced by: 1lt10OLD 12829 0.999... 15892 bpoly4 16070 plendxnocndx 17394 slotsdifdsndx 17404 slotsdifunifndx 17411 slotsdifplendx2 17426 bposlem4 27326 bposlem5 27327 dp2cl 33016 dp2lt10 33020 dp2lt 33021 dp2ltsuc 33022 dp2ltc 33023 dpfrac1 33028 dplti 33041 dpgti 33042 dpexpp1 33044 hgt750lem 34907 problem2 35969 lcmineqlem23 42621 aks4d1p1p7 42644 goldrasin 47429 bgoldbtbndlem1 48380 tgblthelfgott 48390 tgoldbach 48392

W3C validator