![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elnnne0 | Structured version Visualization version GIF version |
Description: The positive integer property expressed in terms of difference from zero. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
Ref | Expression |
---|---|
elnnne0 | ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfn2 11932 | . . 3 ⊢ ℕ = (ℕ0 ∖ {0}) | |
2 | 1 | eleq2i 2842 | . 2 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℕ0 ∖ {0})) |
3 | eldifsn 4670 | . 2 ⊢ (𝑁 ∈ (ℕ0 ∖ {0}) ↔ (𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0)) | |
4 | 2, 3 | bitri 278 | 1 ⊢ (𝑁 ∈ ℕ ↔ (𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 400 ∈ wcel 2112 ≠ wne 2949 ∖ cdif 3851 {csn 4515 0cc0 10560 ℕcn 11659 ℕ0cn0 11919 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-sep 5162 ax-nul 5169 ax-pow 5227 ax-pr 5291 ax-un 7452 ax-resscn 10617 ax-1cn 10618 ax-icn 10619 ax-addcl 10620 ax-addrcl 10621 ax-mulcl 10622 ax-mulrcl 10623 ax-mulcom 10624 ax-addass 10625 ax-mulass 10626 ax-distr 10627 ax-i2m1 10628 ax-1ne0 10629 ax-1rid 10630 ax-rnegex 10631 ax-rrecex 10632 ax-cnre 10633 ax-pre-lttri 10634 ax-pre-lttrn 10635 ax-pre-ltadd 10636 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2899 df-ne 2950 df-nel 3054 df-ral 3073 df-rex 3074 df-reu 3075 df-rab 3077 df-v 3409 df-sbc 3694 df-csb 3802 df-dif 3857 df-un 3859 df-in 3861 df-ss 3871 df-pss 3873 df-nul 4222 df-if 4414 df-pw 4489 df-sn 4516 df-pr 4518 df-tp 4520 df-op 4522 df-uni 4792 df-iun 4878 df-br 5026 df-opab 5088 df-mpt 5106 df-tr 5132 df-id 5423 df-eprel 5428 df-po 5436 df-so 5437 df-fr 5476 df-we 5478 df-xp 5523 df-rel 5524 df-cnv 5525 df-co 5526 df-dm 5527 df-rn 5528 df-res 5529 df-ima 5530 df-pred 6119 df-ord 6165 df-on 6166 df-lim 6167 df-suc 6168 df-iota 6287 df-fun 6330 df-fn 6331 df-f 6332 df-f1 6333 df-fo 6334 df-f1o 6335 df-fv 6336 df-ov 7146 df-om 7573 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-er 8292 df-en 8521 df-dom 8522 df-sdom 8523 df-pnf 10700 df-mnf 10701 df-xr 10702 df-ltxr 10703 df-le 10704 df-nn 11660 df-n0 11920 |
This theorem is referenced by: nn0n0n1ge2 11986 nn0nndivcl 11990 fzo1fzo0n0 13122 elfznelfzo 13176 hashnn0n0nn 13787 swrdccatin1 14119 cshwsublen 14190 cshwidxmod 14197 cshwidx0 14200 repswcshw 14206 cshw1 14216 nn0onn 15766 hashfinmndnn 17979 odhash3 18753 prmgrpsimpgd 19289 0ringnnzr 20095 cply1mul 21003 fvmptnn04if 21534 chfacfisf 21539 chfacfisfcpmat 21540 tayl0 25041 dvtaylp 25049 2sqmod 26104 wlkonl1iedg 27539 pthdlem2 27641 crctcsh 27694 clwwlkneq0 27898 hashecclwwlkn1 27946 umgrhashecclwwlk 27947 clwwlknon0 27962 frgrreg 28263 frgrregord013 28264 xnn0gt0 30601 subne0nn 30644 plymulx0 32030 plymulx 32031 signstfvn 32052 signstfveq0a 32059 poimirlem13 35335 poimirlem20 35342 flt0 39951 dvnmul 42936 dvnprodlem3 42941 wallispilem3 43060 fourierdlem103 43202 fourierdlem104 43203 etransclem28 43255 etransclem35 43262 etransclem38 43265 etransclem44 43271 2ffzoeq 44238 lswn0 44314 ztprmneprm 45101 |
Copyright terms: Public domain | W3C validator |