Theorem 0nn0 9531

Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002.)

Assertion

Ref	Expression
0nn0	⊢ 0 ∈ ℕ0

Proof of Theorem 0nn0

Step	Hyp	Ref	Expression
1		eqid 2234	. 2 ⊢ 0 = 0
2		elnn0 9518	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 133	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 744	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 716   = wceq 1398   ∈ wcel 2205  0cc0 8143  ℕcn 9257  ℕ₀cn0 9516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-1cn 8236  ax-icn 8238  ax-addcl 8239  ax-mulcl 8241  ax-i2m1 8248

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-un 3218  df-sn 3700  df-n0 9517

This theorem is referenced by:  0xnn0  9589  elnn0z  9610  nn0ind-raph  9716  10nn0  9747  declei  9765  numlti  9766  nummul1c  9778  decaddc2  9785  decrmanc  9786  decrmac  9787  decaddm10  9788  decaddi  9789  decaddci  9790  decaddci2  9791  decmul1  9793  decmulnc  9796  6p5e11  9802  7p4e11  9805  8p3e11  9810  9p2e11  9816  10p10e20  9824  fz01or  10470  0elfz  10477  4fvwrd4  10499  fvinim0ffz  10612  0tonninf  10829  exple1  10984  sq10  11102  bc0k  11146  bcn1  11148  bccl  11157  fihasheq0  11184  hashfibc  11235  iswrdiz  11259  iswrddm0  11276  s1leng  11340  s1fv  11342  eqs1  11344  s111  11347  ccat2s1fstg  11364  pfx00g  11395  s2fv0g  11507  s3fv0g  11511  fsumnn0cl  12117  binom  12198  bcxmas  12203  isumnn0nn  12207  geoserap  12221  ef0lem  12374  ege2le3  12385  ef4p  12408  efgt1p2  12409  efgt1p  12410  nn0o  12621  ndvdssub  12644  5ndvds3  12648  bits0  12662  0bits  12673  gcdval  12683  gcdcl  12690  dfgcd3  12734  nn0seqcvgd  12766  algcvg  12773  eucalg  12784  lcmcl  12797  pw2dvdslemn  12890  pclem0  13012  pcpre1  13018  pcfac  13076  dec5dvds2  13139  2exp11  13162  2exp16  13163  ennnfonelemj0  13239  ennnfonelem0  13243  ennnfonelem1  13245  plendxnocndx  13514  slotsdifdsndx  13525  slotsdifunifndx  13532  imasvalstrd  13565  gfsum0  14107  cnfldstr  14835  nn0subm  14860  znf1o  14928  fczpsrbag  14949  psr1clfi  14972  mplsubgfilemm  14982  dveflem  15720  plyconst  15739  plycolemc  15752  pilem3  15777  clwwlkn0  16532  clwwlk0on0  16555  konigsberglem2  16613  konigsberglem3  16614  konigsberglem5  16616  konigsberg  16617  1kp2ke3k  16621  ex-fac  16625  depindlem1  16630  012of  16906  isomninnlem  16953  iswomninnlem  16973  iswomni0  16975  ismkvnnlem  16976