Theorem 0nn0 9330

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

Syntax hints:   ∨ wo 710   = wceq 1373   ∈ wcel 2177  0cc0 7945  ℕcn 9056  ℕ₀cn0 9315

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188  ax-1cn 8038  ax-icn 8040  ax-addcl 8041  ax-mulcl 8043  ax-i2m1 8050

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-v 2775  df-un 3174  df-sn 3644  df-n0 9316

This theorem is referenced by:  0xnn0  9384  elnn0z  9405  nn0ind-raph  9510  10nn0  9541  declei  9559  numlti  9560  nummul1c  9572  decaddc2  9579  decrmanc  9580  decrmac  9581  decaddm10  9582  decaddi  9583  decaddci  9584  decaddci2  9585  decmul1  9587  decmulnc  9590  6p5e11  9596  7p4e11  9599  8p3e11  9604  9p2e11  9610  10p10e20  9618  fz01or  10253  0elfz  10260  4fvwrd4  10282  fvinim0ffz  10392  0tonninf  10607  exple1  10762  sq10  10879  bc0k  10923  bcn1  10925  bccl  10934  fihasheq0  10960  iswrdiz  11023  iswrddm0  11040  s1leng  11101  s1fv  11103  eqs1  11105  s111  11108  pfx00g  11151  fsumnn0cl  11789  binom  11870  bcxmas  11875  isumnn0nn  11879  geoserap  11893  ef0lem  12046  ege2le3  12057  ef4p  12080  efgt1p2  12081  efgt1p  12082  nn0o  12293  ndvdssub  12316  5ndvds3  12320  bits0  12334  0bits  12345  gcdval  12355  gcdcl  12362  dfgcd3  12406  nn0seqcvgd  12438  algcvg  12445  eucalg  12456  lcmcl  12469  pw2dvdslemn  12562  pclem0  12684  pcpre1  12690  pcfac  12748  dec5dvds2  12811  2exp11  12834  2exp16  12835  ennnfonelemj0  12847  ennnfonelem0  12851  ennnfonelem1  12853  plendxnocndx  13121  slotsdifdsndx  13132  slotsdifunifndx  13139  imasvalstrd  13177  cnfldstr  14395  nn0subm  14420  znf1o  14488  fczpsrbag  14508  psr1clfi  14525  mplsubgfilemm  14535  dveflem  15273  plyconst  15292  plycolemc  15305  pilem3  15330  1kp2ke3k  15799  ex-fac  15803  012of  16069  isomninnlem  16110  iswomninnlem  16129  iswomni0  16131  ismkvnnlem  16132