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 12729

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 12707	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12335	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11203	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11219	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11220	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11205	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11219	. 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 7410 ℝcr 11094 0cc0 11095 1c1 11096 + caddc 11098 · cmul 11100 9c9 12297 cdc 12706

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-ext 2735 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-i2m1 11163 ax-1ne0 11164 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-sb 2097 df-clab 2742 df-cleq 2755 df-clel 2838 df-ne 2959 df-ral 3080 df-rex 3090 df-rab 3417 df-v 3457 df-dif 3908 df-un 3910 df-ss 3922 df-nul 4287 df-if 4488 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-br 5110 df-iota 6492 df-fv 6544 df-ov 7413 df-2 12298 df-3 12299 df-4 12300 df-5 12301 df-6 12302 df-7 12303 df-8 12304 df-9 12305 df-dec 12707

This theorem is referenced by: 1lt10OLD 12852 0.999... 15931 bpoly4 16108 plendxnocndx 17432 slotsdifdsndx 17442 slotsdifunifndx 17449 slotsdifplendx2 17464 bposlem4 27451 bposlem5 27452 dp2cl 33199 dp2lt10 33203 dp2lt 33204 dp2ltsuc 33205 dp2ltc 33206 dpfrac1 33211 dplti 33224 dpgti 33225 dpexpp1 33227 hgt750lem 35038 problem2 36158 lcmineqlem23 42838 aks4d1p1p7 42861 goldrasin 47639 bgoldbtbndlem1 48590 tgblthelfgott 48600 tgoldbach 48602

W3C validator