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 11899 | . . 3 ⊢ ℕ0 = (ℕ ∪ {0}) | |
2 | 1 | eleq2i 2904 | . 2 ⊢ (𝐴 ∈ ℕ0 ↔ 𝐴 ∈ (ℕ ∪ {0})) |
3 | elun 4125 | . 2 ⊢ (𝐴 ∈ (ℕ ∪ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 ∈ {0})) | |
4 | c0ex 10635 | . . . 4 ⊢ 0 ∈ V | |
5 | 4 | elsn2 4604 | . . 3 ⊢ (𝐴 ∈ {0} ↔ 𝐴 = 0) |
6 | 5 | orbi2i 909 | . 2 ⊢ ((𝐴 ∈ ℕ ∨ 𝐴 ∈ {0}) ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
7 | 2, 3, 6 | 3bitri 299 | 1 ⊢ (𝐴 ∈ ℕ0 ↔ (𝐴 ∈ ℕ ∨ 𝐴 = 0)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∨ wo 843 = wceq 1537 ∈ wcel 2114 ∪ cun 3934 {csn 4567 0cc0 10537 ℕcn 11638 ℕ0cn0 11898 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-mulcl 10599 ax-i2m1 10605 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3496 df-un 3941 df-sn 4568 df-n0 11899 |
This theorem is referenced by: 0nn0 11913 nn0ge0 11923 nnnn0addcl 11928 nnm1nn0 11939 elnnnn0b 11942 nn0sub 11948 elnn0z 11995 elznn0nn 11996 elznn0 11997 elznn 11998 nn0lt10b 12045 nn0ind-raph 12083 nn0ledivnn 12503 expp1 13437 expneg 13438 expcllem 13441 znsqcld 13527 facp1 13639 faclbnd 13651 faclbnd3 13653 faclbnd4lem1 13654 faclbnd4lem3 13656 faclbnd4 13658 bcn1 13674 bcval5 13679 hashv01gt1 13706 hashnncl 13728 seqcoll2 13824 relexpsucr 14388 relexpsucl 14392 relexpcnv 14394 relexprelg 14397 relexpdmg 14401 relexprng 14405 relexpfld 14408 relexpaddg 14412 fz1f1o 15067 arisum 15215 arisum2 15216 pwdif 15223 geomulcvg 15232 fprodfac 15327 ef0lem 15432 nn0enne 15728 nn0o1gt2 15732 bezoutlem3 15889 dfgcd2 15894 mulgcd 15896 eucalgf 15927 eucalginv 15928 eucalglt 15929 prmdvdsexpr 16061 rpexp1i 16065 nn0gcdsq 16092 odzdvds 16132 pceq0 16207 fldivp1 16233 pockthg 16242 1arith 16263 4sqlem17 16297 4sqlem19 16299 vdwmc2 16315 vdwlem13 16329 0ram 16356 ram0 16358 ramz 16361 ramcl 16365 mulgnn0gsum 18234 mulgnn0p1 18239 mulgnn0subcl 18241 mulgneg 18246 mulgnn0z 18254 mulgnn0dir 18257 mulgnn0ass 18263 submmulg 18271 odcl 18664 mndodcongi 18671 oddvdsnn0 18672 odnncl 18673 oddvds 18675 dfod2 18691 odcl2 18692 gexcl 18705 gexdvds 18709 gexnnod 18713 sylow1lem1 18723 mulgnn0di 18946 torsubg 18974 ablfac1eu 19195 evlslem3 20293 gzrngunitlem 20610 zringlpirlem3 20633 prmirredlem 20640 prmirred 20642 znf1o 20698 dscmet 23182 dvexp2 24551 tdeglem4 24654 dgrnznn 24837 coefv0 24838 dgreq0 24855 dgrcolem2 24864 dvply1 24873 aaliou2 24929 radcnv0 25004 logfac 25184 logtayl 25243 cxpexp 25251 birthdaylem2 25530 harmonicbnd3 25585 sqf11 25716 ppiltx 25754 sqff1o 25759 lgsdir 25908 lgsabs1 25912 lgseisenlem1 25951 2sqlem7 26000 2sqblem 26007 2sqnn 26015 chebbnd1lem1 26045 xrsmulgzz 30665 ressmulgnn0 30671 nexple 31268 eulerpartlemsv2 31616 eulerpartlemv 31622 eulerpartlemb 31626 eulerpartlemf 31628 eulerpartlemgvv 31634 eulerpartlemgh 31636 fz0n 32962 bccolsum 32971 nn0prpw 33671 negn0nposznnd 39188 nn0rppwr 39202 nn0expgcd 39204 fzsplit1nn0 39371 pell1qrgaplem 39490 monotoddzzfi 39559 jm2.22 39612 jm2.23 39613 rmydioph 39631 expdioph 39640 rp-isfinite6 39904 relexpss1d 40070 relexpmulg 40075 iunrelexpmin2 40077 relexp0a 40081 relexpxpmin 40082 relexpaddss 40083 wallispilem3 42372 etransclem24 42563 lighneallem3 43792 lighneallem4 43795 nn0o1gt2ALTV 43879 nn0oALTV 43881 ztprmneprm 44415 blennn0elnn 44657 blen1b 44668 nn0sumshdiglem1 44701 |
Copyright terms: Public domain | W3C validator |