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