ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  zaddcl GIF version

Theorem zaddcl 8312
Description: Closure of addition of integers. (Contributed by NM, 9-May-2004.) (Proof shortened by Mario Carneiro, 16-May-2014.)
Assertion
Ref Expression
zaddcl ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ)

Proof of Theorem zaddcl
StepHypRef Expression
1 elz 8274 . . . 4 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ)))
21simprbi 264 . . 3 (𝑁 ∈ ℤ → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
32adantl 266 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ))
4 zcn 8277 . . . . . . 7 (𝑀 ∈ ℤ → 𝑀 ∈ ℂ)
54adantr 265 . . . . . 6 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℂ)
65addid1d 7193 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 0) = 𝑀)
7 simpl 106 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑀 ∈ ℤ)
86, 7eqeltrd 2128 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 0) ∈ ℤ)
9 oveq2 5545 . . . . 5 (𝑁 = 0 → (𝑀 + 𝑁) = (𝑀 + 0))
109eleq1d 2120 . . . 4 (𝑁 = 0 → ((𝑀 + 𝑁) ∈ ℤ ↔ (𝑀 + 0) ∈ ℤ))
118, 10syl5ibrcom 150 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 = 0 → (𝑀 + 𝑁) ∈ ℤ))
12 zaddcllempos 8309 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℤ)
1312ex 112 . . . 4 (𝑀 ∈ ℤ → (𝑁 ∈ ℕ → (𝑀 + 𝑁) ∈ ℤ))
1413adantr 265 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ ℕ → (𝑀 + 𝑁) ∈ ℤ))
15 zre 8276 . . . 4 (𝑁 ∈ ℤ → 𝑁 ∈ ℝ)
16 zaddcllemneg 8311 . . . . 5 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℤ)
17163expia 1115 . . . 4 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℝ) → (-𝑁 ∈ ℕ → (𝑀 + 𝑁) ∈ ℤ))
1815, 17sylan2 274 . . 3 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (-𝑁 ∈ ℕ → (𝑀 + 𝑁) ∈ ℤ))
1911, 14, 183jaod 1208 . 2 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑁 = 0 ∨ 𝑁 ∈ ℕ ∨ -𝑁 ∈ ℕ) → (𝑀 + 𝑁) ∈ ℤ))
203, 19mpd 13 1 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3o 893   = wceq 1257  wcel 1407  (class class class)co 5537  cc 6915  cr 6916  0cc0 6917   + caddc 6920  -cneg 7216  cn 7960  cz 8272
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 552  ax-in2 553  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-13 1418  ax-14 1419  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036  ax-coll 3897  ax-sep 3900  ax-nul 3908  ax-pow 3952  ax-pr 3969  ax-un 4195  ax-setind 4287  ax-iinf 4336  ax-cnex 7003  ax-resscn 7004  ax-1cn 7005  ax-1re 7006  ax-icn 7007  ax-addcl 7008  ax-addrcl 7009  ax-mulcl 7010  ax-addcom 7012  ax-addass 7014  ax-distr 7016  ax-i2m1 7017  ax-0id 7020  ax-rnegex 7021  ax-cnre 7023  ax-pre-ltirr 7024  ax-pre-ltwlin 7025  ax-pre-lttrn 7026  ax-pre-ltadd 7028
This theorem depends on definitions:  df-bi 114  df-dc 752  df-3or 895  df-3an 896  df-tru 1260  df-fal 1263  df-nf 1364  df-sb 1660  df-eu 1917  df-mo 1918  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-ne 2219  df-nel 2313  df-ral 2326  df-rex 2327  df-reu 2328  df-rab 2330  df-v 2574  df-sbc 2785  df-csb 2878  df-dif 2945  df-un 2947  df-in 2949  df-ss 2956  df-nul 3250  df-pw 3386  df-sn 3406  df-pr 3407  df-op 3409  df-uni 3606  df-int 3641  df-iun 3684  df-br 3790  df-opab 3844  df-mpt 3845  df-tr 3880  df-eprel 4051  df-id 4055  df-po 4058  df-iso 4059  df-iord 4128  df-on 4130  df-suc 4133  df-iom 4339  df-xp 4376  df-rel 4377  df-cnv 4378  df-co 4379  df-dm 4380  df-rn 4381  df-res 4382  df-ima 4383  df-iota 4892  df-fun 4929  df-fn 4930  df-f 4931  df-f1 4932  df-fo 4933  df-f1o 4934  df-fv 4935  df-riota 5493  df-ov 5540  df-oprab 5541  df-mpt2 5542  df-1st 5792  df-2nd 5793  df-recs 5948  df-irdg 5985  df-1o 6029  df-2o 6030  df-oadd 6033  df-omul 6034  df-er 6134  df-ec 6136  df-qs 6140  df-ni 6430  df-pli 6431  df-mi 6432  df-lti 6433  df-plpq 6470  df-mpq 6471  df-enq 6473  df-nqqs 6474  df-plqqs 6475  df-mqqs 6476  df-1nqqs 6477  df-rq 6478  df-ltnqqs 6479  df-enq0 6550  df-nq0 6551  df-0nq0 6552  df-plq0 6553  df-mq0 6554  df-inp 6592  df-i1p 6593  df-iplp 6594  df-iltp 6596  df-enr 6839  df-nr 6840  df-ltr 6843  df-0r 6844  df-1r 6845  df-0 6924  df-1 6925  df-r 6927  df-lt 6930  df-pnf 7091  df-mnf 7092  df-xr 7093  df-ltxr 7094  df-le 7095  df-sub 7217  df-neg 7218  df-inn 7961  df-n0 8210  df-z 8273
This theorem is referenced by:  zsubcl  8313  zrevaddcl  8322  zdivadd  8357  zaddcld  8393  eluzaddi  8565  eluzsubi  8566  eluzadd  8567  nn0pzuz  8596  fzen  8979  fzaddel  8994  fzrev3  9021  fzrevral3  9041  elfzmlbp  9062  fzoaddel  9120  zpnn0elfzo  9135  elfzomelpfzo  9159  fzoshftral  9166  climshftlemg  10017  summodnegmod  10101  dvds2ln  10103  dvds2add  10104  dvdsadd  10113  dvdsadd2b  10117  addmodlteqALT  10134  3dvdsdec  10139  3dvds2dec  10140  opoe  10170  opeo  10172
  Copyright terms: Public domain W3C validator