Theorem 0nn0 9264

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 9251	. . . 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 7879  ℕcn 8990  ℕ₀cn0 9249

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 7972  ax-icn 7974  ax-addcl 7975  ax-mulcl 7977  ax-i2m1 7984

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 3628  df-n0 9250

This theorem is referenced by:  0xnn0  9318  elnn0z  9339  nn0ind-raph  9443  10nn0  9474  declei  9492  numlti  9493  nummul1c  9505  decaddc2  9512  decrmanc  9513  decrmac  9514  decaddm10  9515  decaddi  9516  decaddci  9517  decaddci2  9518  decmul1  9520  decmulnc  9523  6p5e11  9529  7p4e11  9532  8p3e11  9537  9p2e11  9543  10p10e20  9551  fz01or  10186  0elfz  10193  4fvwrd4  10215  fvinim0ffz  10317  0tonninf  10532  exple1  10687  sq10  10804  bc0k  10848  bcn1  10850  bccl  10859  fihasheq0  10885  iswrdiz  10942  iswrddm0  10959  fsumnn0cl  11568  binom  11649  bcxmas  11654  isumnn0nn  11658  geoserap  11672  ef0lem  11825  ege2le3  11836  ef4p  11859  efgt1p2  11860  efgt1p  11861  nn0o  12072  ndvdssub  12095  5ndvds3  12099  bits0  12112  gcdval  12126  gcdcl  12133  dfgcd3  12177  nn0seqcvgd  12209  algcvg  12216  eucalg  12227  lcmcl  12240  pw2dvdslemn  12333  pclem0  12455  pcpre1  12461  pcfac  12519  dec5dvds2  12582  2exp11  12605  2exp16  12606  ennnfonelemj0  12618  ennnfonelem0  12622  ennnfonelem1  12624  slotsdifdsndx  12898  slotsdifunifndx  12905  cnfldstr  14114  nn0subm  14139  znf1o  14207  fczpsrbag  14225  dveflem  14962  plyconst  14981  plycolemc  14994  pilem3  15019  1kp2ke3k  15370  ex-fac  15374  012of  15640  isomninnlem  15674  iswomninnlem  15693  iswomni0  15695  ismkvnnlem  15696