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 12752

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 12730	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12357	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11225	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11241	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11242	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11227	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11241	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2861	1 ⊢ ;10 ∈ ℝ

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∈ wcel 2146 (class class class)co 7419 ℝcr 11116 0cc0 11117 1c1 11118 + caddc 11120 · cmul 11122 9c9 12319 cdc 12729

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 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-ext 2737 ax-1cn 11175 ax-icn 11176 ax-addcl 11177 ax-addrcl 11178 ax-mulcl 11179 ax-mulrcl 11180 ax-i2m1 11185 ax-1ne0 11186 ax-rnegex 11188 ax-rrecex 11189 ax-cnre 11190

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 2100 df-clab 2744 df-cleq 2757 df-clel 2840 df-ne 2961 df-ral 3082 df-rex 3092 df-rab 3419 df-v 3459 df-dif 3909 df-un 3911 df-ss 3923 df-nul 4287 df-if 4490 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-br 5112 df-iota 6496 df-fv 6548 df-ov 7422 df-2 12320 df-3 12321 df-4 12322 df-5 12323 df-6 12324 df-7 12325 df-8 12326 df-9 12327 df-dec 12730

This theorem is used by: 1lt10OLD 12875 0.999... 15960 bpoly4 16137 plendxnocndx 17461 slotsdifdsndx 17471 slotsdifunifndx 17478 slotsdifplendx2 17493 bposlem4 27504 bposlem5 27505 dp2cl 33271 dp2lt10 33275 dp2lt 33276 dp2ltsuc 33277 dp2ltc 33278 dpfrac1 33283 dplti 33296 dpgti 33297 dpexpp1 33299 hgt750lem 35105 problem2 36197 lcmineqlem23 42878 aks4d1p1p7 42901 goldrasin 47679 bgoldbtbndlem1 48630 tgblthelfgott 48640 tgoldbach 48642

W3C validator