Theorem 0nn0 9292

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 2204	. 2 ⊢ 0 = 0
2		elnn0 9279	. . . 4 ⊢ (0 ∈ ℕ0 ↔ (0 ∈ ℕ ∨ 0 = 0))
3	2	biimpri 133	. . 3 ⊢ ((0 ∈ ℕ ∨ 0 = 0) → 0 ∈ ℕ0)
4	3	olcs 737	. 2 ⊢ (0 = 0 → 0 ∈ ℕ0)
5	1, 4	ax-mp 5	1 ⊢ 0 ∈ ℕ0

Syntax hints:   ∨ wo 709   = wceq 1372   ∈ wcel 2175  0cc0 7907  ℕcn 9018  ℕ₀cn0 9277

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186  ax-1cn 8000  ax-icn 8002  ax-addcl 8003  ax-mulcl 8005  ax-i2m1 8012

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-n0 9278

This theorem is referenced by:  0xnn0  9346  elnn0z  9367  nn0ind-raph  9472  10nn0  9503  declei  9521  numlti  9522  nummul1c  9534  decaddc2  9541  decrmanc  9542  decrmac  9543  decaddm10  9544  decaddi  9545  decaddci  9546  decaddci2  9547  decmul1  9549  decmulnc  9552  6p5e11  9558  7p4e11  9561  8p3e11  9566  9p2e11  9572  10p10e20  9580  fz01or  10215  0elfz  10222  4fvwrd4  10244  fvinim0ffz  10351  0tonninf  10566  exple1  10721  sq10  10838  bc0k  10882  bcn1  10884  bccl  10893  fihasheq0  10919  iswrdiz  10976  iswrddm0  10993  fsumnn0cl  11633  binom  11714  bcxmas  11719  isumnn0nn  11723  geoserap  11737  ef0lem  11890  ege2le3  11901  ef4p  11924  efgt1p2  11925  efgt1p  11926  nn0o  12137  ndvdssub  12160  5ndvds3  12164  bits0  12178  0bits  12189  gcdval  12199  gcdcl  12206  dfgcd3  12250  nn0seqcvgd  12282  algcvg  12289  eucalg  12300  lcmcl  12313  pw2dvdslemn  12406  pclem0  12528  pcpre1  12534  pcfac  12592  dec5dvds2  12655  2exp11  12678  2exp16  12679  ennnfonelemj0  12691  ennnfonelem0  12695  ennnfonelem1  12697  plendxnocndx  12964  slotsdifdsndx  12975  slotsdifunifndx  12982  imasvalstrd  13020  cnfldstr  14238  nn0subm  14263  znf1o  14331  fczpsrbag  14351  psr1clfi  14368  mplsubgfilemm  14378  dveflem  15116  plyconst  15135  plycolemc  15148  pilem3  15173  1kp2ke3k  15524  ex-fac  15528  012of  15794  isomninnlem  15833  iswomninnlem  15852  iswomni0  15854  ismkvnnlem  15855