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

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

StepHypRef Expression
1 elz 8003 . . . 4 (𝑁 ℤ ↔ (𝑁 (𝑁 = 0 𝑁 -𝑁 ℕ)))
21simprbi 260 . . 3 (𝑁 ℤ → (𝑁 = 0 𝑁 -𝑁 ℕ))
32adantl 262 . 2 ((𝑀 𝑁 ℤ) → (𝑁 = 0 𝑁 -𝑁 ℕ))
4 zcn 8006 . . . . . . 7 (𝑀 ℤ → 𝑀 ℂ)
54adantr 261 . . . . . 6 ((𝑀 𝑁 ℤ) → 𝑀 ℂ)
65addid1d 6939 . . . . 5 ((𝑀 𝑁 ℤ) → (𝑀 + 0) = 𝑀)
7 simpl 102 . . . . 5 ((𝑀 𝑁 ℤ) → 𝑀 ℤ)
86, 7eqeltrd 2111 . . . 4 ((𝑀 𝑁 ℤ) → (𝑀 + 0) ℤ)
9 oveq2 5463 . . . . 5 (𝑁 = 0 → (𝑀 + 𝑁) = (𝑀 + 0))
109eleq1d 2103 . . . 4 (𝑁 = 0 → ((𝑀 + 𝑁) ℤ ↔ (𝑀 + 0) ℤ))
118, 10syl5ibrcom 146 . . 3 ((𝑀 𝑁 ℤ) → (𝑁 = 0 → (𝑀 + 𝑁) ℤ))
12 zaddcllempos 8038 . . . . 5 ((𝑀 𝑁 ℕ) → (𝑀 + 𝑁) ℤ)
1312ex 108 . . . 4 (𝑀 ℤ → (𝑁 ℕ → (𝑀 + 𝑁) ℤ))
1413adantr 261 . . 3 ((𝑀 𝑁 ℤ) → (𝑁 ℕ → (𝑀 + 𝑁) ℤ))
15 zre 8005 . . . 4 (𝑁 ℤ → 𝑁 ℝ)
16 zaddcllemneg 8040 . . . . 5 ((𝑀 𝑁 -𝑁 ℕ) → (𝑀 + 𝑁) ℤ)
17163expia 1105 . . . 4 ((𝑀 𝑁 ℝ) → (-𝑁 ℕ → (𝑀 + 𝑁) ℤ))
1815, 17sylan2 270 . . 3 ((𝑀 𝑁 ℤ) → (-𝑁 ℕ → (𝑀 + 𝑁) ℤ))
1911, 14, 183jaod 1198 . 2 ((𝑀 𝑁 ℤ) → ((𝑁 = 0 𝑁 -𝑁 ℕ) → (𝑀 + 𝑁) ℤ))
203, 19mpd 13 1 ((𝑀 𝑁 ℤ) → (𝑀 + 𝑁) ℤ)