Theorem 0nn0 7663

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

Assertion

Ref	Expression
0nn0	|- 0 e. NN0

Proof of Theorem 0nn0

Step	Hyp	Ref	Expression
1		eqid 2141	. 2 |- 0 = 0
2		elnn0 7650	. . . 4 |- (0 e. NN0 <-> (0 e. NN \/ 0 = 0))
3	2	biimpri 230	. . 3 |- ((0 e. NN \/ 0 = 0) -> 0 e. NN0)
4	3	olcs 384	. 2 |- (0 = 0 -> 0 e. NN0)
5	1, 4	ax-mp 7	1 |- 0 e. NN0

Syntax hints:   \/ wo 336   = wceq 1586   e. wcel 1588  0cc0 6752  NNcn 6992  NN0cn0 6993

This theorem is referenced by:  nn0addcl 7670  nn0mulcli 7672  nn0mulcl 7673  elnn00nn 7724  zltp1le 7732  nn0ind-raph 7771  fz1eqb 8061  fseq1p1m1 8065  seq00 8168  seq01 8170  ser0cl1i 8191  ser00i 8193  exp0 8198  nn0opth2 8302  nthruz 8380  facnn 8570  fac0 8571  faclbnd4lem1 8585  faclbnd4lem3 8587  bcval 8595  bcn0 8600  bcnn 8601  bcpasci 8606  bccl2 8608  bccl 8609  hash0 8626  ser1ser0i 8704  binomi 8728  bcxmas 8732  isumnn0nnai 8865  geolim1i 8898  dfef2i 8967  ef0lem 8970  efseq0ex 8971  eft0vali 9061  ef4pi 9062  efge1i 9064  efm1limi 9074  ndvdssub 9304  gcdcl 9318  nn0seqcvgd 9333  algr0 9335  algcvg 9339  mulgcdlem6 9356  1arithlem12 9405  1arithlem19 9412  dscmet 10062

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-fv 4147  df-opr 4983  df-oprab 4984  df-1st 5126  df-2nd 5127  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-mp 6607  df-ltp 6608  df-plpr 6682  df-mpr 6683  df-enr 6684  df-nr 6685  df-plr 6686  df-mr 6687  df-0r 6689  df-1r 6690  df-m1r 6691  df-c 6758  df-0 6759  df-1 6760  df-i 6761  df-r 6762  df-plus 6763  df-mul 6764  df-n0 7649

Copyright terms: Public domain