Theorem 10nn 12146

Description: 10 is a positive integer. (Contributed by NM, 8-Nov-2012.) (Revised by AV, 6-Sep-2021.)

Assertion

Ref	Expression
10nn	⊢ ;10 ∈ ℕ

Proof of Theorem 10nn

Step	Hyp	Ref	Expression
1		9p1e10 12132	. 2 ⊢ (9 + 1) = ;10
2		9nn 11765	. . 3 ⊢ 9 ∈ ℕ
3		peano2nn 11679	. . 3 ⊢ (9 ∈ ℕ → (9 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (9 + 1) ∈ ℕ
5	1, 4	eqeltrri 2850	1 ⊢ ;10 ∈ ℕ

Syntax hints:   ∈ wcel 2112  (class class class)co 7151  0cc0 10568  1c1 10569   + caddc 10571  ℕcn 11667  9c9 11729  ;cdc 12130

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-resscn 10625  ax-1cn 10626  ax-icn 10627  ax-addcl 10628  ax-addrcl 10629  ax-mulcl 10630  ax-mulrcl 10631  ax-mulcom 10632  ax-addass 10633  ax-mulass 10634  ax-distr 10635  ax-i2m1 10636  ax-1ne0 10637  ax-1rid 10638  ax-rnegex 10639  ax-rrecex 10640  ax-cnre 10641  ax-pre-lttri 10642  ax-pre-lttrn 10643  ax-pre-ltadd 10644

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-ov 7154  df-om 7581  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-er 8300  df-en 8529  df-dom 8530  df-sdom 8531  df-pnf 10708  df-mnf 10709  df-ltxr 10711  df-nn 11668  df-2 11730  df-3 11731  df-4 11732  df-5 11733  df-6 11734  df-7 11735  df-8 11736  df-9 11737  df-dec 12131

This theorem is referenced by:  10pos  12147  decnncl2  12154  declt  12158  decltc  12159  declti  12168  dec10p  12173  3dec  13669  3dvds  15725  163prm  16509  631prm  16511  plendx  16717  pleid  16718  otpsstr  16719  ressle  16723  odrngstr  16730  imasvalstr  16776  isposix  17626  ipostr  17822  cnfldstr  20161  bclbnd  25956  ex-prmo  28336  rpdp2cl  30673  dp2ltsuc  30677  dpmul10  30686  decdiv10  30687  dpmul100  30688  dp3mul10  30689  dpadd2  30701  dpadd  30702  dpadd3  30703  dpmul  30704  dpmul4  30705  oppgle  30755  idlsrgstr  31161  hgt750lem  32143  tgoldbachgt  32155  60gcd6e6  39564  aks4d1p1p7  39633  rmydioph  40321  1t10e1p1e11  44228  257prm  44439  127prm  44477  3exp4mod41  44494  41prothprmlem1  44495  bgoldbtbndlem1  44683  bgoldbachlt  44691  tgblthelfgott  44693  tgoldbachlt  44694