MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  10nn0 Structured version   Unicode version

Theorem 10nn0 10895
Description: 10 is a nonnegative integer. (Contributed by Mario Carneiro, 19-Apr-2015.)
Assertion
Ref Expression
10nn0  |-  10  e.  NN0

Proof of Theorem 10nn0
StepHypRef Expression
1 10nn 10776 . 2  |-  10  e.  NN
21nnnn0i 10878 1  |-  10  e.  NN0
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1868   10c10 10668   NN0cn0 10870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pow 4599  ax-pr 4657  ax-un 6594  ax-1cn 9598
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4761  df-id 4765  df-po 4771  df-so 4772  df-fr 4809  df-we 4811  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-pred 5396  df-ord 5442  df-on 5443  df-lim 5444  df-suc 5445  df-iota 5562  df-fun 5600  df-fn 5601  df-f 5602  df-f1 5603  df-fo 5604  df-f1o 5605  df-fv 5606  df-ov 6305  df-om 6704  df-wrecs 7033  df-recs 7095  df-rdg 7133  df-nn 10611  df-2 10669  df-3 10670  df-4 10671  df-5 10672  df-6 10673  df-7 10674  df-8 10675  df-9 10676  df-10 10677  df-n0 10871
This theorem is referenced by:  decnncl  11065  deccl  11066  dec0u  11067  dec0h  11068  decsuc  11075  decma  11090  decmac  11091  decma2c  11092  decadd  11093  decaddc  11094  decmul1c  11099  decmul2c  11100  dec2dvds  15023  decsplit0b  15040  decsplit1  15042  decsplit  15043  karatsuba  15044  139prm  15083  317prm  15085  1259lem1  15090  1259lem3  15092  2503lem1  15096  4001lem1  15100  4001lem3  15102  rmydioph  35789  tgoldbach  38623
  Copyright terms: Public domain W3C validator