Metamath Proof Explorer

Theorem zaddcl

Description: Closure of addition of integers. (Contributed by NM, 9-May-2004) (Proof shortened by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion zaddcl ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )

Proof

Step Hyp Ref Expression
1 elz2 ⊢ ( 𝑀 ∈ ℤ ↔ ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑀 = ( 𝑥 − 𝑦 ) )
2 elz2 ⊢ ( 𝑁 ∈ ℤ ↔ ∃ 𝑧 ∈ ℕ ∃ 𝑤 ∈ ℕ 𝑁 = ( 𝑧 − 𝑤 ) )
3 reeanv ⊢ ( ∃ 𝑥 ∈ ℕ ∃ 𝑧 ∈ ℕ ( ∃ 𝑦 ∈ ℕ 𝑀 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑤 ∈ ℕ 𝑁 = ( 𝑧 − 𝑤 ) ) ↔ ( ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑀 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ ℕ ∃ 𝑤 ∈ ℕ 𝑁 = ( 𝑧 − 𝑤 ) ) )
4 reeanv ⊢ ( ∃ 𝑦 ∈ ℕ ∃ 𝑤 ∈ ℕ ( 𝑀 = ( 𝑥 − 𝑦 ) ∧ 𝑁 = ( 𝑧 − 𝑤 ) ) ↔ ( ∃ 𝑦 ∈ ℕ 𝑀 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑤 ∈ ℕ 𝑁 = ( 𝑧 − 𝑤 ) ) )
5 nnaddcl ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → ( 𝑥 + 𝑧 ) ∈ ℕ )
6 5 adantr ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( 𝑥 + 𝑧 ) ∈ ℕ )
7 nnaddcl ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) → ( 𝑦 + 𝑤 ) ∈ ℕ )
8 7 adantl ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( 𝑦 + 𝑤 ) ∈ ℕ )
9 nncn ⊢ ( 𝑥 ∈ ℕ → 𝑥 ∈ ℂ )
10 nncn ⊢ ( 𝑧 ∈ ℕ → 𝑧 ∈ ℂ )
11 9 10 anim12i ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) )
12 nncn ⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℂ )
13 nncn ⊢ ( 𝑤 ∈ ℕ → 𝑤 ∈ ℂ )
14 12 13 anim12i ⊢ ( ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) → ( 𝑦 ∈ ℂ ∧ 𝑤 ∈ ℂ ) )
15 addsub4 ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑤 ∈ ℂ ) ) → ( ( 𝑥 + 𝑧 ) − ( 𝑦 + 𝑤 ) ) = ( ( 𝑥 − 𝑦 ) + ( 𝑧 − 𝑤 ) ) )
16 11 14 15 syl2an ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝑥 + 𝑧 ) − ( 𝑦 + 𝑤 ) ) = ( ( 𝑥 − 𝑦 ) + ( 𝑧 − 𝑤 ) ) )
17 16 eqcomd ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝑥 − 𝑦 ) + ( 𝑧 − 𝑤 ) ) = ( ( 𝑥 + 𝑧 ) − ( 𝑦 + 𝑤 ) ) )
18 rspceov ⊢ ( ( ( 𝑥 + 𝑧 ) ∈ ℕ ∧ ( 𝑦 + 𝑤 ) ∈ ℕ ∧ ( ( 𝑥 − 𝑦 ) + ( 𝑧 − 𝑤 ) ) = ( ( 𝑥 + 𝑧 ) − ( 𝑦 + 𝑤 ) ) ) → ∃ 𝑢 ∈ ℕ ∃ 𝑣 ∈ ℕ ( ( 𝑥 − 𝑦 ) + ( 𝑧 − 𝑤 ) ) = ( 𝑢 − 𝑣 ) )
19 6 8 17 18 syl3anc ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ∃ 𝑢 ∈ ℕ ∃ 𝑣 ∈ ℕ ( ( 𝑥 − 𝑦 ) + ( 𝑧 − 𝑤 ) ) = ( 𝑢 − 𝑣 ) )
20 elz2 ⊢ ( ( ( 𝑥 − 𝑦 ) + ( 𝑧 − 𝑤 ) ) ∈ ℤ ↔ ∃ 𝑢 ∈ ℕ ∃ 𝑣 ∈ ℕ ( ( 𝑥 − 𝑦 ) + ( 𝑧 − 𝑤 ) ) = ( 𝑢 − 𝑣 ) )
21 19 20 sylibr ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝑥 − 𝑦 ) + ( 𝑧 − 𝑤 ) ) ∈ ℤ )
22 oveq12 ⊢ ( ( 𝑀 = ( 𝑥 − 𝑦 ) ∧ 𝑁 = ( 𝑧 − 𝑤 ) ) → ( 𝑀 + 𝑁 ) = ( ( 𝑥 − 𝑦 ) + ( 𝑧 − 𝑤 ) ) )
23 22 eleq1d ⊢ ( ( 𝑀 = ( 𝑥 − 𝑦 ) ∧ 𝑁 = ( 𝑧 − 𝑤 ) ) → ( ( 𝑀 + 𝑁 ) ∈ ℤ ↔ ( ( 𝑥 − 𝑦 ) + ( 𝑧 − 𝑤 ) ) ∈ ℤ ) )
24 21 23 syl5ibrcom ⊢ ( ( ( 𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ ) ∧ ( 𝑦 ∈ ℕ ∧ 𝑤 ∈ ℕ ) ) → ( ( 𝑀 = ( 𝑥 − 𝑦 ) ∧ 𝑁 = ( 𝑧 − 𝑤 ) ) → ( 𝑀 + 𝑁 ) ∈ ℤ ) )
25 24 rexlimdvva ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → ( ∃ 𝑦 ∈ ℕ ∃ 𝑤 ∈ ℕ ( 𝑀 = ( 𝑥 − 𝑦 ) ∧ 𝑁 = ( 𝑧 − 𝑤 ) ) → ( 𝑀 + 𝑁 ) ∈ ℤ ) )
26 4 25 biimtrrid ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑧 ∈ ℕ ) → ( ( ∃ 𝑦 ∈ ℕ 𝑀 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑤 ∈ ℕ 𝑁 = ( 𝑧 − 𝑤 ) ) → ( 𝑀 + 𝑁 ) ∈ ℤ ) )
27 26 rexlimivv ⊢ ( ∃ 𝑥 ∈ ℕ ∃ 𝑧 ∈ ℕ ( ∃ 𝑦 ∈ ℕ 𝑀 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑤 ∈ ℕ 𝑁 = ( 𝑧 − 𝑤 ) ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
28 3 27 sylbir ⊢ ( ( ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℕ 𝑀 = ( 𝑥 − 𝑦 ) ∧ ∃ 𝑧 ∈ ℕ ∃ 𝑤 ∈ ℕ 𝑁 = ( 𝑧 − 𝑤 ) ) → ( 𝑀 + 𝑁 ) ∈ ℤ )
29 1 2 28 syl2anb ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + 𝑁 ) ∈ ℤ )