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 12734

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 12712	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12340	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11208	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11224	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11225	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11210	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11224	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2865	1 ⊢ ;10 ∈ ℝ

Colors of variables: wff setvar class

Syntax hints: ∈ wcel 2149 (class class class)co 7411 ℝcr 11099 0cc0 11100 1c1 11101 + caddc 11103 · cmul 11105 9c9 12302 cdc 12711

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-ext 2741 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-i2m1 11168 ax-1ne0 11169 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-sb 2098 df-clab 2748 df-cleq 2761 df-clel 2844 df-ne 2965 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-dif 3916 df-un 3918 df-ss 3930 df-nul 4295 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-br 5114 df-iota 6493 df-fv 6545 df-ov 7414 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-dec 12712

This theorem is referenced by: 1lt10OLD 12857 0.999... 15935 bpoly4 16113 plendxnocndx 17437 slotsdifdsndx 17447 slotsdifunifndx 17454 slotsdifplendx2 17469 bposlem4 27417 bposlem5 27418 dp2cl 33140 dp2lt10 33144 dp2lt 33145 dp2ltsuc 33146 dp2ltc 33147 dpfrac1 33152 dplti 33165 dpgti 33166 dpexpp1 33168 hgt750lem 34983 problem2 36091 lcmineqlem23 42742 aks4d1p1p7 42765 goldrasin 47542 bgoldbtbndlem1 48493 tgblthelfgott 48503 tgoldbach 48505

W3C validator