Theorem 10nn 12555

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 12541	. 2 ⊢ (9 + 1) = ;10
2		9nn 12173	. . 3 ⊢ 9 ∈ ℕ
3		peano2nn 12087	. . 3 ⊢ (9 ∈ ℕ → (9 + 1) ∈ ℕ)
4	2, 3	ax-mp 5	. 2 ⊢ (9 + 1) ∈ ℕ
5	1, 4	eqeltrri 2834	1 ⊢ ;10 ∈ ℕ

Syntax hints:   ∈ wcel 2105  (class class class)co 7338  0cc0 10973  1c1 10974   + caddc 10976  ℕcn 12075  9c9 12137  ;cdc 12539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-iun 4944  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-ov 7341  df-om 7782  df-2nd 7901  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-er 8570  df-en 8806  df-dom 8807  df-sdom 8808  df-pnf 11113  df-mnf 11114  df-ltxr 11116  df-nn 12076  df-2 12138  df-3 12139  df-4 12140  df-5 12141  df-6 12142  df-7 12143  df-8 12144  df-9 12145  df-dec 12540

This theorem is referenced by:  10pos  12556  decnncl2  12563  declt  12567  decltc  12568  declti  12577  dec10p  12582  3dec  14082  3dvds  16140  163prm  16924  631prm  16926  plendx  17174  pleid  17175  plendxnn  17176  otpsstr  17184  odrngstr  17211  imasvalstr  17260  isposixOLD  18142  ipostr  18345  cnfldstr  20706  bclbnd  26535  ex-prmo  29112  rpdp2cl  31443  dp2ltsuc  31447  dpmul10  31456  decdiv10  31457  dpmul100  31458  dp3mul10  31459  dpadd2  31471  dpadd  31472  dpadd3  31473  dpmul  31474  dpmul4  31475  oppgleOLD  31526  idlsrgstr  31944  hgt750lem  32931  tgoldbachgt  32943  60gcd6e6  40317  aks4d1p1p7  40387  rmydioph  41150  1t10e1p1e11  45220  257prm  45431  127prm  45469  3exp4mod41  45486  41prothprmlem1  45487  bgoldbtbndlem1  45675  bgoldbachlt  45683  tgblthelfgott  45685  tgoldbachlt  45686