Theorem nnssz 12055

Description: Positive integers are a subset of integers. (Contributed by NM, 9-Jan-2002.) Reduce dependencies on axioms. (Revised by Steven Nguyen, 29-Nov-2022.)

Assertion

Ref	Expression
nnssz	⊢ ℕ ⊆ ℤ

Proof of Theorem nnssz

Step	Hyp	Ref	Expression
1		nnre 11695	. . 3 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℝ)
2		3mix2 1329	. . 3 ⊢ (𝑥 ∈ ℕ → (𝑥 = 0 ∨ 𝑥 ∈ ℕ ∨ -𝑥 ∈ ℕ))
3		elz 12036	. . 3 ⊢ (𝑥 ∈ ℤ ↔ (𝑥 ∈ ℝ ∧ (𝑥 = 0 ∨ 𝑥 ∈ ℕ ∨ -𝑥 ∈ ℕ)))
4	1, 2, 3	sylanbrc 586	. 2 ⊢ (𝑥 ∈ ℕ → 𝑥 ∈ ℤ)
5	4	ssriv 3899	1 ⊢ ℕ ⊆ ℤ

Syntax hints:   ∨ w3o 1084   = wceq 1539   ∈ wcel 2112   ⊆ wss 3861  ℝcr 10588  0cc0 10589  -cneg 10923  ℕcn 11688  ℤcz 12034

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 5174  ax-nul 5181  ax-pr 5303  ax-un 7466  ax-1cn 10647  ax-icn 10648  ax-addcl 10649  ax-addrcl 10650  ax-mulcl 10651  ax-mulrcl 10652  ax-i2m1 10657  ax-1ne0 10658  ax-rrecex 10661  ax-cnre 10662

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  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-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3700  df-csb 3809  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-pss 3880  df-nul 4229  df-if 4425  df-pw 4500  df-sn 4527  df-pr 4529  df-tp 4531  df-op 4533  df-uni 4803  df-iun 4889  df-br 5038  df-opab 5100  df-mpt 5118  df-tr 5144  df-id 5435  df-eprel 5440  df-po 5448  df-so 5449  df-fr 5488  df-we 5490  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-rn 5540  df-res 5541  df-ima 5542  df-pred 6132  df-ord 6178  df-on 6179  df-lim 6180  df-suc 6181  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-ov 7160  df-om 7587  df-wrecs 7964  df-recs 8025  df-rdg 8063  df-neg 10925  df-nn 11689  df-z 12035

This theorem is referenced by:  nn0ssz  12056  nnz  12057  nnzi  12059  zmin  12398  nnssq  12412  divcnvshft  15272  znnen  15627  nthruc  15667  alzdvds  15735  evennn2n  15766  lcmfnnval  16035  lcmfnncl  16040  pclem  16245  prmreclem1  16322  ftalem5  25776  2sqreunnltblem  26149  archiabllem1b  30986  reprsuc  32128  divcnvlin  33227  diophin  40132  hashnzfzclim  41445