Theorem 0nn0 9281

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 2196	. 2 ⊢ 0 = 0
2		elnn0 9268	. . . 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 1364   ∈ wcel 2167  0cc0 7896  ℕcn 9007  ℕ₀cn0 9266

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-1cn 7989  ax-icn 7991  ax-addcl 7992  ax-mulcl 7994  ax-i2m1 8001

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-un 3161  df-sn 3629  df-n0 9267

This theorem is referenced by:  0xnn0  9335  elnn0z  9356  nn0ind-raph  9460  10nn0  9491  declei  9509  numlti  9510  nummul1c  9522  decaddc2  9529  decrmanc  9530  decrmac  9531  decaddm10  9532  decaddi  9533  decaddci  9534  decaddci2  9535  decmul1  9537  decmulnc  9540  6p5e11  9546  7p4e11  9549  8p3e11  9554  9p2e11  9560  10p10e20  9568  fz01or  10203  0elfz  10210  4fvwrd4  10232  fvinim0ffz  10334  0tonninf  10549  exple1  10704  sq10  10821  bc0k  10865  bcn1  10867  bccl  10876  fihasheq0  10902  iswrdiz  10959  iswrddm0  10976  fsumnn0cl  11585  binom  11666  bcxmas  11671  isumnn0nn  11675  geoserap  11689  ef0lem  11842  ege2le3  11853  ef4p  11876  efgt1p2  11877  efgt1p  11878  nn0o  12089  ndvdssub  12112  5ndvds3  12116  bits0  12130  0bits  12141  gcdval  12151  gcdcl  12158  dfgcd3  12202  nn0seqcvgd  12234  algcvg  12241  eucalg  12252  lcmcl  12265  pw2dvdslemn  12358  pclem0  12480  pcpre1  12486  pcfac  12544  dec5dvds2  12607  2exp11  12630  2exp16  12631  ennnfonelemj0  12643  ennnfonelem0  12647  ennnfonelem1  12649  plendxnocndx  12916  slotsdifdsndx  12927  slotsdifunifndx  12934  imasvalstrd  12972  cnfldstr  14190  nn0subm  14215  znf1o  14283  fczpsrbag  14301  psr1clfi  14316  dveflem  15046  plyconst  15065  plycolemc  15078  pilem3  15103  1kp2ke3k  15454  ex-fac  15458  012of  15724  isomninnlem  15761  iswomninnlem  15780  iswomni0  15782  ismkvnnlem  15783