Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  zaddcl Structured version   Visualization 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 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ)

Proof of Theorem zaddcl
Dummy variables 𝑣 𝑢 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elz2 11584 . 2 (𝑀 ∈ ℤ ↔ ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝑀 = (𝑥𝑦))
2 elz2 11584 . 2 (𝑁 ∈ ℤ ↔ ∃𝑧 ∈ ℕ ∃𝑤 ∈ ℕ 𝑁 = (𝑧𝑤))
3 reeanv 3243 . . 3 (∃𝑥 ∈ ℕ ∃𝑧 ∈ ℕ (∃𝑦 ∈ ℕ 𝑀 = (𝑥𝑦) ∧ ∃𝑤 ∈ ℕ 𝑁 = (𝑧𝑤)) ↔ (∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝑀 = (𝑥𝑦) ∧ ∃𝑧 ∈ ℕ ∃𝑤 ∈ ℕ 𝑁 = (𝑧𝑤)))
4 reeanv 3243 . . . . 5 (∃𝑦 ∈ ℕ ∃𝑤 ∈ ℕ (𝑀 = (𝑥𝑦) ∧ 𝑁 = (𝑧𝑤)) ↔ (∃𝑦 ∈ ℕ 𝑀 = (𝑥𝑦) ∧ ∃𝑤 ∈ ℕ 𝑁 = (𝑧𝑤)))
5 nnaddcl 11232 . . . . . . . . . 10 ((𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑥 + 𝑧) ∈ ℕ)
65adantr 472 . . . . . . . . 9 (((𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (𝑥 + 𝑧) ∈ ℕ)
7 nnaddcl 11232 . . . . . . . . . 10 ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) → (𝑦 + 𝑤) ∈ ℕ)
87adantl 473 . . . . . . . . 9 (((𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → (𝑦 + 𝑤) ∈ ℕ)
9 nncn 11218 . . . . . . . . . . . 12 (𝑥 ∈ ℕ → 𝑥 ∈ ℂ)
10 nncn 11218 . . . . . . . . . . . 12 (𝑧 ∈ ℕ → 𝑧 ∈ ℂ)
119, 10anim12i 591 . . . . . . . . . . 11 ((𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ))
12 nncn 11218 . . . . . . . . . . . 12 (𝑦 ∈ ℕ → 𝑦 ∈ ℂ)
13 nncn 11218 . . . . . . . . . . . 12 (𝑤 ∈ ℕ → 𝑤 ∈ ℂ)
1412, 13anim12i 591 . . . . . . . . . . 11 ((𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ) → (𝑦 ∈ ℂ ∧ 𝑤 ∈ ℂ))
15 addsub4 10514 . . . . . . . . . . 11 (((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) ∧ (𝑦 ∈ ℂ ∧ 𝑤 ∈ ℂ)) → ((𝑥 + 𝑧) − (𝑦 + 𝑤)) = ((𝑥𝑦) + (𝑧𝑤)))
1611, 14, 15syl2an 495 . . . . . . . . . 10 (((𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → ((𝑥 + 𝑧) − (𝑦 + 𝑤)) = ((𝑥𝑦) + (𝑧𝑤)))
1716eqcomd 2764 . . . . . . . . 9 (((𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → ((𝑥𝑦) + (𝑧𝑤)) = ((𝑥 + 𝑧) − (𝑦 + 𝑤)))
18 rspceov 6853 . . . . . . . . 9 (((𝑥 + 𝑧) ∈ ℕ ∧ (𝑦 + 𝑤) ∈ ℕ ∧ ((𝑥𝑦) + (𝑧𝑤)) = ((𝑥 + 𝑧) − (𝑦 + 𝑤))) → ∃𝑢 ∈ ℕ ∃𝑣 ∈ ℕ ((𝑥𝑦) + (𝑧𝑤)) = (𝑢𝑣))
196, 8, 17, 18syl3anc 1477 . . . . . . . 8 (((𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → ∃𝑢 ∈ ℕ ∃𝑣 ∈ ℕ ((𝑥𝑦) + (𝑧𝑤)) = (𝑢𝑣))
20 elz2 11584 . . . . . . . 8 (((𝑥𝑦) + (𝑧𝑤)) ∈ ℤ ↔ ∃𝑢 ∈ ℕ ∃𝑣 ∈ ℕ ((𝑥𝑦) + (𝑧𝑤)) = (𝑢𝑣))
2119, 20sylibr 224 . . . . . . 7 (((𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → ((𝑥𝑦) + (𝑧𝑤)) ∈ ℤ)
22 oveq12 6820 . . . . . . . 8 ((𝑀 = (𝑥𝑦) ∧ 𝑁 = (𝑧𝑤)) → (𝑀 + 𝑁) = ((𝑥𝑦) + (𝑧𝑤)))
2322eleq1d 2822 . . . . . . 7 ((𝑀 = (𝑥𝑦) ∧ 𝑁 = (𝑧𝑤)) → ((𝑀 + 𝑁) ∈ ℤ ↔ ((𝑥𝑦) + (𝑧𝑤)) ∈ ℤ))
2421, 23syl5ibrcom 237 . . . . . 6 (((𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ)) → ((𝑀 = (𝑥𝑦) ∧ 𝑁 = (𝑧𝑤)) → (𝑀 + 𝑁) ∈ ℤ))
2524rexlimdvva 3174 . . . . 5 ((𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ) → (∃𝑦 ∈ ℕ ∃𝑤 ∈ ℕ (𝑀 = (𝑥𝑦) ∧ 𝑁 = (𝑧𝑤)) → (𝑀 + 𝑁) ∈ ℤ))
264, 25syl5bir 233 . . . 4 ((𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ) → ((∃𝑦 ∈ ℕ 𝑀 = (𝑥𝑦) ∧ ∃𝑤 ∈ ℕ 𝑁 = (𝑧𝑤)) → (𝑀 + 𝑁) ∈ ℤ))
2726rexlimivv 3172 . . 3 (∃𝑥 ∈ ℕ ∃𝑧 ∈ ℕ (∃𝑦 ∈ ℕ 𝑀 = (𝑥𝑦) ∧ ∃𝑤 ∈ ℕ 𝑁 = (𝑧𝑤)) → (𝑀 + 𝑁) ∈ ℤ)
283, 27sylbir 225 . 2 ((∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ 𝑀 = (𝑥𝑦) ∧ ∃𝑧 ∈ ℕ ∃𝑤 ∈ ℕ 𝑁 = (𝑧𝑤)) → (𝑀 + 𝑁) ∈ ℤ)
291, 2, 28syl2anb 497 1 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + 𝑁) ∈ ℤ)