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 12762

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 12740	. 2 ⊢ ;10 = (((9 + 1) · 1) + 0)
2		9re 12367	. . . . 5 ⊢ 9 ∈ ℝ
3		1re 11235	. . . . 5 ⊢ 1 ∈ ℝ
4	2, 3	readdcli 11251	. . . 4 ⊢ (9 + 1) ∈ ℝ
5	4, 3	remulcli 11252	. . 3 ⊢ ((9 + 1) · 1) ∈ ℝ
6		0re 11237	. . 3 ⊢ 0 ∈ ℝ
7	5, 6	readdcli 11251	. 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ
8	1, 7	eqeltri 2856	1 ⊢ ;10 ∈ ℝ

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∈ wcel 2145 (class class class)co 7414 ℝcr 11126 0cc0 11127 1c1 11128 + caddc 11130 · cmul 11132 9c9 12329 cdc 12739

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 2147 ax-9 2155 ax-ext 2732 ax-1cn 11185 ax-icn 11186 ax-addcl 11187 ax-addrcl 11188 ax-mulcl 11189 ax-mulrcl 11190 ax-i2m1 11195 ax-1ne0 11196 ax-rnegex 11198 ax-rrecex 11199 ax-cnre 11200

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 2739 df-cleq 2752 df-clel 2835 df-ne 2956 df-ral 3077 df-rex 3087 df-rab 3413 df-v 3452 df-dif 3902 df-un 3904 df-ss 3916 df-nul 4280 df-if 4483 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-iota 6489 df-fv 6541 df-ov 7417 df-2 12330 df-3 12331 df-4 12332 df-5 12333 df-6 12334 df-7 12335 df-8 12336 df-9 12337 df-dec 12740

This theorem is used by: 1lt10OLD 12885 0.999... 15973 bpoly4 16148 plendxnocndx 17472 slotsdifdsndx 17482 slotsdifunifndx 17489 slotsdifplendx2 17504 bposlem4 27526 bposlem5 27527 dp2cl 33328 dp2lt10 33332 dp2lt 33333 dp2ltsuc 33334 dp2ltc 33335 dpfrac1 33340 dplti 33353 dpgti 33354 dpexpp1 33356 hgt750lem 35162 problem2 36248 lcmineqlem23 42920 aks4d1p1p7 42943 goldrasin 47750 bgoldbtbndlem1 48724 tgblthelfgott 48734 tgoldbach 48736

W3C validator