![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 9re | Structured version Visualization version GIF version |
Description: The number 9 is real. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
9re | ⊢ 9 ∈ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-9 11555 | . 2 ⊢ 9 = (8 + 1) | |
2 | 8re 11581 | . . 3 ⊢ 8 ∈ ℝ | |
3 | 1re 10487 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 10502 | . 2 ⊢ (8 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2879 | 1 ⊢ 9 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2081 (class class class)co 7016 ℝcr 10382 1c1 10384 + caddc 10386 8c8 11546 9c9 11547 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-ext 2769 ax-1cn 10441 ax-icn 10442 ax-addcl 10443 ax-addrcl 10444 ax-mulcl 10445 ax-mulrcl 10446 ax-i2m1 10451 ax-1ne0 10452 ax-rrecex 10455 ax-cnre 10456 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-rab 3114 df-v 3439 df-dif 3862 df-un 3864 df-in 3866 df-ss 3874 df-nul 4212 df-if 4382 df-sn 4473 df-pr 4475 df-op 4479 df-uni 4746 df-br 4963 df-iota 6189 df-fv 6233 df-ov 7019 df-2 11548 df-3 11549 df-4 11550 df-5 11551 df-6 11552 df-7 11553 df-8 11554 df-9 11555 |
This theorem is referenced by: 7lt9 11685 6lt9 11686 5lt9 11687 4lt9 11688 3lt9 11689 2lt9 11690 1lt9 11691 10re 11966 9lt10 12079 8lt10 12080 0.999... 15070 cos2bnd 15374 sincos2sgn 15380 cnfldfun 20239 tuslem 22559 setsmsds 22769 tnglem 22932 tngds 22940 2logb9irr 25054 sqrt2cxp2logb9e3 25058 log2tlbnd 25205 bposlem4 25545 bposlem5 25546 bposlem7 25548 bposlem8 25549 bposlem9 25550 ex-fv 27914 dp2lt10 30244 hgt750lem 31539 hgt750lem2 31540 hgt750leme 31546 problem5 32520 31prm 43242 2exp340mod341 43380 341fppr2 43381 9fppr8 43384 nfermltl8rev 43389 nfermltl2rev 43390 wtgoldbnnsum4prm 43449 bgoldbnnsum3prm 43451 bgoldbtbndlem1 43452 |
Copyright terms: Public domain | W3C validator |