Metamath Proof Explorer

Theorem gzaddcl

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

Ref Expression
Assertion gzaddcl ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( 𝐴 + 𝐵 ) ∈ ℤ[i] )

Proof

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