Theorem znegcl 12556

Description: Closure law for negative integers. (Contributed by NM, 9-May-2004.)

Assertion

Ref	Expression
znegcl	⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)

Proof of Theorem znegcl

Step	Hyp	Ref	Expression
1		elz 12520	. 2 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
2		negeq 11379	. . . . 5 ⊢ (𝑁 = 0 → -𝑁 = -0)
3		neg0 11434	. . . . 5 ⊢ -0 = 0
4	2, 3	eqtrdi 2788	. . . 4 ⊢ (𝑁 = 0 → -𝑁 = 0)
5		0z 12529	. . . 4 ⊢ 0 ∈ ℤ
6	4, 5	eqeltrdi 2845	. . 3 ⊢ (𝑁 = 0 → -𝑁 ∈ ℤ)
7		nnnegz 12521	. . 3 ⊢ (𝑁 ∈ ℕ → -𝑁 ∈ ℤ)
8		nnz 12539	. . 3 ⊢ (-𝑁 ∈ ℕ → -𝑁 ∈ ℤ)
9	6, 7, 8	3jaoi 1431	. 2 ⊢ ((𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ) → -𝑁 ∈ ℤ)
10	1, 9	simplbiim 504	1 ⊢ (𝑁 ∈ ℤ → -𝑁 ∈ ℤ)

Syntax hints:   → wi 4   ∨ w3o 1086   = wceq 1542   ∈ wcel 2114  ℝcr 11031  0cc0 11032  -cneg 11372  ℕcn 12168  ℤcz 12518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-pred 6260  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-riota 7318  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7812  df-2nd 7937  df-frecs 8225  df-wrecs 8256  df-recs 8305  df-rdg 8343  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-ltxr 11178  df-sub 11373  df-neg 11374  df-nn 12169  df-z 12519

This theorem is referenced by:  znegclb  12558  nn0negz  12559  zsubcl  12563  zeo  12609  zindd  12624  znegcld  12629  zriotaneg  12636  uzneg  12802  zmax  12889  rebtwnz  12891  qnegcl  12910  fzsubel  13508  fzosubel  13673  ceilid  13804  modcyc2  13860  expsub  14066  seqshft  15041  climshft  15532  negdvdsb  16235  dvdsnegb  16236  summodnegmod  16249  difmod0  16250  dvdssub  16267  odd2np1  16304  divalglem6  16361  bitscmp  16401  gcdneg  16485  neggcd  16486  gcdaddmlem  16487  lcmneg  16566  neglcm  16567  lcmabs  16568  mulgaddcomlem  19067  mulgneg2  19078  mulgsubdir  19084  cycsubgcl  19175  zaddablx  19841  cyggeninv  19852  zsubrg  21413  zringsub  21448  zringmulg  21449  zringinvg  21458  pzriprnglem4  21477  aaliou3lem9  26330  sinperlem  26460  wilthlem3  27050  basellem3  27063  basellem4  27064  basellem8  27068  basellem9  27069  lgsneg  27301  lgsdir2lem4  27308  lgsdir2lem5  27309  ex-fl  30535  ex-mod  30537  pell1234qrdich  43310  rmxyneg  43369  monotoddzzfi  43391  monotoddzz  43392  oddcomabszz  43393  jm2.24  43412  acongtr  43427  fzneg  43431  jm2.26a  43449  cosknegpi  46318  nthrucw  47335  ceilbi  47800  enege  48136  onego  48137  0nodd  48661  2zrngagrp  48740  zlmodzxzequap  48990  flsubz  49013  digvalnn0  49090  dig0  49097  dig2nn0  49102