Theorem 1nn0 9331

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

Assertion

Ref	Expression
1nn0	⊢ 1 ∈ ℕ0

Proof of Theorem 1nn0

Step	Hyp	Ref	Expression
1		1nn 9067	. 2 ⊢ 1 ∈ ℕ
2	1	nnnn0i 9323	1 ⊢ 1 ∈ ℕ0

Syntax hints:   ∈ wcel 2177  1c1 7946  ℕ₀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-1re 8039

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-ral 2490  df-v 2775  df-un 3174  df-in 3176  df-ss 3183  df-int 3892  df-inn 9057  df-n0 9316

This theorem is referenced by:  peano2nn0  9355  deccl  9538  10nn0  9541  numsucc  9563  numadd  9570  numaddc  9571  11multnc  9591  6p5lem  9593  6p6e12  9597  7p5e12  9600  8p4e12  9605  9p2e11  9610  9p3e12  9611  10p10e20  9618  4t4e16  9622  5t2e10  9623  5t4e20  9625  6t3e18  9628  6t4e24  9629  7t3e21  9633  7t4e28  9634  8t3e24  9639  9t3e27  9646  9t9e81  9652  nn01to3  9758  fz0to3un2pr  10265  elfzom1elp1fzo  10353  fzo0sn0fzo1  10372  fldiv4lem1div2  10472  1tonninf  10608  expn1ap0  10716  nn0expcl  10720  sqval  10764  sq10  10879  nn0opthlem1d  10887  fac2  10898  bccl  10934  hashsng  10965  1elfz0hash  10973  snopiswrd  11026  wrdred1hash  11059  pfx1  11179  bcxmas  11875  arisum  11884  geoisum1  11905  geoisum1c  11906  cvgratnnlemsumlt  11914  mertenslem2  11922  fprodnn0cl  11998  ege2le3  12057  ef4p  12080  efgt1p2  12081  efgt1p  12082  sin01gt0  12148  dvds1  12239  3dvds2dec  12252  5ndvds6  12321  bitsmod  12342  bitsinv1lem  12347  isprm5  12539  pcelnn  12719  pockthg  12755  dec5nprm  12812  dec2nprm  12813  modxp1i  12816  2exp8  12833  2exp11  12834  2exp16  12835  2expltfac  12837  ennnfonelemhom  12861  ocndx  13118  ocid  13119  basendxnocndx  13120  plendxnocndx  13121  dsndx  13122  dsid  13123  dsslid  13124  dsndxnn  13125  basendxltdsndx  13126  slotsdifdsndx  13132  unifndx  13133  unifid  13134  unifndxnn  13135  basendxltunifndx  13136  slotsdifunifndx  13139  homndx  13140  homid  13141  homslid  13142  ccondx  13143  ccoid  13144  ccoslid  13145  imasvalstrd  13177  prdsvalstrd  13178  cnfldstr  14395  dveflem  15273  plyid  15293  1sgmprm  15541  perfectlem1  15546  perfectlem2  15547  2lgslem3a  15645  2lgslem3c  15647  edgfid  15680  edgfndx  15681  edgfndxnn  15682  basendxltedgfndx  15684  1kp2ke3k  15799  ex-exp  15802  ex-fac  15803  012of  16069  isomninnlem  16110  trilpolemisumle  16118  iswomninnlem  16129  iswomni0  16131  ismkvnnlem  16132