![]() |
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 12334 | . 2 ⊢ 9 = (8 + 1) | |
2 | 8re 12360 | . . 3 ⊢ 8 ∈ ℝ | |
3 | 1re 11264 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2, 3 | readdcli 11279 | . 2 ⊢ (8 + 1) ∈ ℝ |
5 | 1, 4 | eqeltri 2822 | 1 ⊢ 9 ∈ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 (class class class)co 7424 ℝcr 11157 1c1 11159 + caddc 11161 8c8 12325 9c9 12326 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 ax-1cn 11216 ax-icn 11217 ax-addcl 11218 ax-addrcl 11219 ax-mulcl 11220 ax-mulrcl 11221 ax-i2m1 11226 ax-1ne0 11227 ax-rrecex 11230 ax-cnre 11231 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ne 2931 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3464 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-br 5154 df-iota 6506 df-fv 6562 df-ov 7427 df-2 12327 df-3 12328 df-4 12329 df-5 12330 df-6 12331 df-7 12332 df-8 12333 df-9 12334 |
This theorem is referenced by: 7lt9 12464 6lt9 12465 5lt9 12466 4lt9 12467 3lt9 12468 2lt9 12469 1lt9 12470 10re 12748 9lt10 12860 8lt10 12861 0.999... 15885 cos2bnd 16190 sincos2sgn 16196 slotsdifplendx 17389 dsndxntsetndx 17407 unifndxntsetndx 17414 cnfldfunALTOLDOLD 21372 tuslemOLD 24263 setsmsdsOLD 24475 tnglemOLD 24641 tngdsOLD 24656 2logb9irr 26823 sqrt2cxp2logb9e3 26827 log2tlbnd 26973 bposlem4 27316 bposlem5 27317 bposlem7 27319 bposlem8 27320 bposlem9 27321 ex-fv 30376 dp2lt10 32745 hgt750lem 34497 hgt750lem2 34498 hgt750leme 34504 problem5 35497 60gcd7e1 41704 lcmineqlem23 41750 3lexlogpow5ineq1 41753 3lexlogpow5ineq2 41754 3lexlogpow5ineq4 41755 3lexlogpow5ineq3 41756 3lexlogpow2ineq2 41758 3lexlogpow5ineq5 41759 aks4d1lem1 41761 aks4d1p1 41775 aks4d1p6 41780 aks4d1p7d1 41781 aks4d1p7 41782 aks4d1p8 41786 31prm 47169 2exp340mod341 47305 341fppr2 47306 9fppr8 47309 nfermltl8rev 47314 nfermltl2rev 47315 wtgoldbnnsum4prm 47374 bgoldbnnsum3prm 47376 bgoldbtbndlem1 47377 ackval42 48084 |
Copyright terms: Public domain | W3C validator |