Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elnn0 | Structured version Visualization version GIF version |
Description: Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002.) |
Ref | Expression |
---|---|
elnn0 | ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-n0 11293 | . . 3 ⊢ ℕ0 = (ℕ ∪ {0}) | |
2 | 1 | eleq2i 2693 | . 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0})) |
3 | elun 3753 | . 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0})) | |
4 | c0ex 10034 | . . . 4 ⊢ 0 ∈ V | |
5 | 4 | elsn2 4211 | . . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0) |
6 | 5 | orbi2i 541 | . 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
7 | 2, 3, 6 | 3bitri 286 | 1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∨ wo 383 = wceq 1483 ∈ wcel 1990 ∪ cun 3572 {csn 4177 0cc0 9936 ℕcn 11020 ℕ0cn0 11292 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-mulcl 9998 ax-i2m1 10004 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-un 3579 df-sn 4178 df-n0 11293 |
This theorem is referenced by: 0nn0 11307 nn0ge0 11318 nnnn0addcl 11323 nnm1nn0 11334 elnnnn0b 11337 nn0sub 11343 elnn0z 11390 elznn0nn 11391 elznn0 11392 elznn 11393 nn0lt10b 11439 nn0ind-raph 11477 nn0ledivnn 11941 expp1 12867 expneg 12868 expcllem 12871 facp1 13065 faclbnd 13077 faclbnd3 13079 faclbnd4lem1 13080 faclbnd4lem3 13082 faclbnd4 13084 bcn1 13100 bcval5 13105 hashv01gt1 13133 hashnncl 13157 seqcoll2 13249 relexpsucr 13769 relexpsucl 13773 relexpcnv 13775 relexprelg 13778 relexpdmg 13782 relexprng 13786 relexpfld 13789 relexpaddg 13793 fz1f1o 14441 arisum 14592 arisum2 14593 geomulcvg 14607 fprodfac 14703 ef0lem 14809 nn0enne 15094 nn0o1gt2 15097 bezoutlem3 15258 dfgcd2 15263 mulgcd 15265 eucalgf 15296 eucalginv 15297 eucalglt 15298 prmdvdsexpr 15429 rpexp1i 15433 nn0gcdsq 15460 odzdvds 15500 pceq0 15575 fldivp1 15601 pockthg 15610 1arith 15631 4sqlem17 15665 4sqlem19 15667 vdwmc2 15683 vdwlem13 15697 0ram 15724 ram0 15726 ramz 15729 ramcl 15733 mulgnn0p1 17552 mulgnn0subcl 17554 mulgneg 17560 mulgnn0z 17567 mulgnn0dir 17571 mulgnn0ass 17578 submmulg 17586 odcl 17955 mndodcongi 17962 oddvdsnn0 17963 odnncl 17964 oddvds 17966 dfod2 17981 odcl2 17982 gexcl 17995 gexdvds 17999 gexnnod 18003 sylow1lem1 18013 mulgnn0di 18231 torsubg 18257 ablfac1eu 18472 evlslem3 19514 gzrngunitlem 19811 zringlpirlem3 19834 prmirredlem 19841 prmirred 19843 znf1o 19900 dscmet 22377 dvexp2 23717 tdeglem4 23820 dgrnznn 24003 coefv0 24004 dgreq0 24021 dgrcolem2 24030 dvply1 24039 aaliou2 24095 radcnv0 24170 logfac 24347 logtayl 24406 cxpexp 24414 leibpilem1 24667 birthdaylem2 24679 harmonicbnd3 24734 sqf11 24865 ppiltx 24903 sqff1o 24908 lgsdir 25057 lgsabs1 25061 lgseisenlem1 25100 2sqlem7 25149 2sqblem 25156 chebbnd1lem1 25158 numclwwlkffin0 27215 znsqcld 29512 xrsmulgzz 29678 ressmulgnn0 29684 nexple 30071 eulerpartlemsv2 30420 eulerpartlemv 30426 eulerpartlemb 30430 eulerpartlemf 30432 eulerpartlemgvv 30438 eulerpartlemgh 30440 fz0n 31616 bccolsum 31625 nn0prpw 32318 fzsplit1nn0 37317 pell1qrgaplem 37437 monotoddzzfi 37507 jm2.22 37562 jm2.23 37563 rmydioph 37581 expdioph 37590 rp-isfinite6 37864 relexpss1d 37997 relexpmulg 38002 iunrelexpmin2 38004 relexp0a 38008 relexpxpmin 38009 relexpaddss 38010 wallispilem3 40284 etransclem24 40475 pwdif 41501 lighneallem3 41524 lighneallem4 41527 nn0o1gt2ALTV 41605 nn0oALTV 41607 ztprmneprm 42125 blennn0elnn 42371 blen1b 42382 nn0sumshdiglem1 42415 |
Copyright terms: Public domain | W3C validator |