Metamath Proof Explorer

Theorem gzaddcl

Description: The gaussian integers are closed under addition. (Contributed by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion gzaddcl ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → A + B ∈ ℤ i

Proof

Step Hyp Ref Expression
1 gzcn ⊢ A ∈ ℤ i → A ∈ ℂ
2 gzcn ⊢ B ∈ ℤ i → B ∈ ℂ
3 addcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B ∈ ℂ
4 1 2 3 syl2an ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → A + B ∈ ℂ
5 readd ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A + B = ℜ ⁡ A + ℜ ⁡ B
6 1 2 5 syl2an ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℜ ⁡ A + B = ℜ ⁡ A + ℜ ⁡ B
7 elgz ⊢ A ∈ ℤ i ↔ A ∈ ℂ ∧ ℜ ⁡ A ∈ ℤ ∧ ℑ ⁡ A ∈ ℤ
8 7 simp2bi ⊢ A ∈ ℤ i → ℜ ⁡ A ∈ ℤ
9 elgz ⊢ B ∈ ℤ i ↔ B ∈ ℂ ∧ ℜ ⁡ B ∈ ℤ ∧ ℑ ⁡ B ∈ ℤ
10 9 simp2bi ⊢ B ∈ ℤ i → ℜ ⁡ B ∈ ℤ
11 zaddcl ⊢ ℜ ⁡ A ∈ ℤ ∧ ℜ ⁡ B ∈ ℤ → ℜ ⁡ A + ℜ ⁡ B ∈ ℤ
12 8 10 11 syl2an ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℜ ⁡ A + ℜ ⁡ B ∈ ℤ
13 6 12 eqeltrd ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℜ ⁡ A + B ∈ ℤ
14 imadd ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℑ ⁡ A + B = ℑ ⁡ A + ℑ ⁡ B
15 1 2 14 syl2an ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℑ ⁡ A + B = ℑ ⁡ A + ℑ ⁡ B
16 7 simp3bi ⊢ A ∈ ℤ i → ℑ ⁡ A ∈ ℤ
17 9 simp3bi ⊢ B ∈ ℤ i → ℑ ⁡ B ∈ ℤ
18 zaddcl ⊢ ℑ ⁡ A ∈ ℤ ∧ ℑ ⁡ B ∈ ℤ → ℑ ⁡ A + ℑ ⁡ B ∈ ℤ
19 16 17 18 syl2an ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℑ ⁡ A + ℑ ⁡ B ∈ ℤ
20 15 19 eqeltrd ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℑ ⁡ A + B ∈ ℤ
21 elgz ⊢ A + B ∈ ℤ i ↔ A + B ∈ ℂ ∧ ℜ ⁡ A + B ∈ ℤ ∧ ℑ ⁡ A + B ∈ ℤ
22 4 13 20 21 syl3anbrc ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → A + B ∈ ℤ i