Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 10re | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
10re | ⊢ ;10 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dec 12086 | . 2 ⊢ ;10 = (((9 + 1) · 1) + 0) | |
2 | 9re 11723 | . . . . 5 ⊢ 9 ∈ ℝ | |
3 | 1re 10627 | . . . . 5 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 10642 | . . . 4 ⊢ (9 + 1) ∈ ℝ |
5 | 4, 3 | remulcli 10643 | . . 3 ⊢ ((9 + 1) · 1) ∈ ℝ |
6 | 0re 10629 | . . 3 ⊢ 0 ∈ ℝ | |
7 | 5, 6 | readdcli 10642 | . 2 ⊢ (((9 + 1) · 1) + 0) ∈ ℝ |
8 | 1, 7 | eqeltri 2909 | 1 ⊢ ;10 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2114 (class class class)co 7142 ℝcr 10522 0cc0 10523 1c1 10524 + caddc 10526 · cmul 10528 9c9 11686 ;cdc 12085 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-1cn 10581 ax-icn 10582 ax-addcl 10583 ax-addrcl 10584 ax-mulcl 10585 ax-mulrcl 10586 ax-i2m1 10591 ax-1ne0 10592 ax-rnegex 10594 ax-rrecex 10595 ax-cnre 10596 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-rab 3147 df-v 3488 df-dif 3927 df-un 3929 df-in 3931 df-ss 3940 df-nul 4280 df-if 4454 df-sn 4554 df-pr 4556 df-op 4560 df-uni 4825 df-br 5053 df-iota 6300 df-fv 6349 df-ov 7145 df-2 11687 df-3 11688 df-4 11689 df-5 11690 df-6 11691 df-7 11692 df-8 11693 df-9 11694 df-dec 12086 |
This theorem is referenced by: 8lt10 12217 7lt10 12218 6lt10 12219 5lt10 12220 4lt10 12221 3lt10 12222 2lt10 12223 1lt10 12224 0.999... 15222 bpoly4 15398 cnfldfun 20540 thlle 20824 bposlem4 25849 bposlem5 25850 dp2cl 30542 dp2lt10 30546 dp2lt 30547 dp2ltsuc 30548 dp2ltc 30549 dpfrac1 30554 dplti 30567 dpgti 30568 dpexpp1 30570 hgt750lem 31929 problem2 32916 bgoldbtbndlem1 44055 tgblthelfgott 44065 tgoldbach 44067 |
Copyright terms: Public domain | W3C validator |