![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nn0ssre | Structured version Visualization version GIF version |
Description: Nonnegative integers are a subset of the reals. (Contributed by Raph Levien, 10-Dec-2002.) |
Ref | Expression |
---|---|
nn0ssre | ⊢ ℕ0 ⊆ ℝ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-n0 11748 | . 2 ⊢ ℕ0 = (ℕ ∪ {0}) | |
2 | nnssre 11492 | . . 3 ⊢ ℕ ⊆ ℝ | |
3 | 0re 10492 | . . . 4 ⊢ 0 ∈ ℝ | |
4 | snssi 4650 | . . . 4 ⊢ (0 ∈ ℝ → {0} ⊆ ℝ) | |
5 | 3, 4 | ax-mp 5 | . . 3 ⊢ {0} ⊆ ℝ |
6 | 2, 5 | unssi 4084 | . 2 ⊢ (ℕ ∪ {0}) ⊆ ℝ |
7 | 1, 6 | eqsstri 3924 | 1 ⊢ ℕ0 ⊆ ℝ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2080 ∪ cun 3859 ⊆ wss 3861 {csn 4474 ℝcr 10385 0cc0 10386 ℕcn 11488 ℕ0cn0 11747 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-sep 5097 ax-nul 5104 ax-pow 5160 ax-pr 5224 ax-un 7322 ax-1cn 10444 ax-icn 10445 ax-addcl 10446 ax-addrcl 10447 ax-mulcl 10448 ax-mulrcl 10449 ax-i2m1 10454 ax-1ne0 10455 ax-rnegex 10457 ax-rrecex 10458 ax-cnre 10459 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ne 2984 df-ral 3109 df-rex 3110 df-reu 3111 df-rab 3113 df-v 3438 df-sbc 3708 df-csb 3814 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-pss 3878 df-nul 4214 df-if 4384 df-pw 4457 df-sn 4475 df-pr 4477 df-tp 4479 df-op 4481 df-uni 4748 df-iun 4829 df-br 4965 df-opab 5027 df-mpt 5044 df-tr 5067 df-id 5351 df-eprel 5356 df-po 5365 df-so 5366 df-fr 5405 df-we 5407 df-xp 5452 df-rel 5453 df-cnv 5454 df-co 5455 df-dm 5456 df-rn 5457 df-res 5458 df-ima 5459 df-pred 6026 df-ord 6072 df-on 6073 df-lim 6074 df-suc 6075 df-iota 6192 df-fun 6230 df-fn 6231 df-f 6232 df-f1 6233 df-fo 6234 df-f1o 6235 df-fv 6236 df-ov 7022 df-om 7440 df-wrecs 7801 df-recs 7863 df-rdg 7901 df-nn 11489 df-n0 11748 |
This theorem is referenced by: nn0re 11756 nn0rei 11758 nn0red 11806 ssnn0fi 13203 fsuppmapnn0fiublem 13208 fsuppmapnn0fiub 13209 hashxrcl 13568 ramtlecl 16165 ramcl2lem 16174 ramxrcl 16182 0ram2 16186 0ramcl 16188 mdegleb 24341 mdeglt 24342 mdegldg 24343 mdegxrcl 24344 mdegcl 24346 mdegaddle 24351 mdegmullem 24355 deg1mul3le 24393 plyeq0lem 24483 dgrval 24501 dgrcl 24506 dgrub 24507 dgrlb 24509 aannenlem2 24601 taylfval 24630 tgcgr4 25999 motcgrg 26012 hashxpe 30205 dplti 30257 xrsmulgzz 30331 nn0omnd 30560 nn0archi 30562 esumcst 30931 oddpwdc 31221 breprexp 31513 lermxnn0 39045 hbtlem2 39222 ssnn0ssfz 43889 |
Copyright terms: Public domain | W3C validator |