Metamath Proof Explorer

Theorem gzmulcl

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

Ref Expression
Assertion gzmulcl ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → A ⁢ B ∈ ℤ i

Proof

Step Hyp Ref Expression
1 gzcn ⊢ A ∈ ℤ i → A ∈ ℂ
2 gzcn ⊢ B ∈ ℤ i → B ∈ ℂ
3 mulcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ∈ ℂ
4 1 2 3 syl2an ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → A ⁢ B ∈ ℂ
5 remul ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℜ ⁡ A ⁢ B = ℜ ⁡ A ⁢ ℜ ⁡ B − ℑ ⁡ A ⁢ ℑ ⁡ B
6 1 2 5 syl2an ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℜ ⁡ A ⁢ B = ℜ ⁡ 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 zmulcl ⊢ ℜ ⁡ A ∈ ℤ ∧ ℜ ⁡ B ∈ ℤ → ℜ ⁡ A ⁢ ℜ ⁡ B ∈ ℤ
12 8 10 11 syl2an ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℜ ⁡ A ⁢ ℜ ⁡ B ∈ ℤ
13 7 simp3bi ⊢ A ∈ ℤ i → ℑ ⁡ A ∈ ℤ
14 9 simp3bi ⊢ B ∈ ℤ i → ℑ ⁡ B ∈ ℤ
15 zmulcl ⊢ ℑ ⁡ A ∈ ℤ ∧ ℑ ⁡ B ∈ ℤ → ℑ ⁡ A ⁢ ℑ ⁡ B ∈ ℤ
16 13 14 15 syl2an ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℑ ⁡ A ⁢ ℑ ⁡ B ∈ ℤ
17 12 16 zsubcld ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℜ ⁡ A ⁢ ℜ ⁡ B − ℑ ⁡ A ⁢ ℑ ⁡ B ∈ ℤ
18 6 17 eqeltrd ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℜ ⁡ A ⁢ B ∈ ℤ
19 immul ⊢ A ∈ ℂ ∧ B ∈ ℂ → ℑ ⁡ A ⁢ B = ℜ ⁡ A ⁢ ℑ ⁡ B + ℑ ⁡ A ⁢ ℜ ⁡ B
20 1 2 19 syl2an ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℑ ⁡ A ⁢ B = ℜ ⁡ A ⁢ ℑ ⁡ B + ℑ ⁡ A ⁢ ℜ ⁡ B
21 zmulcl ⊢ ℜ ⁡ A ∈ ℤ ∧ ℑ ⁡ B ∈ ℤ → ℜ ⁡ A ⁢ ℑ ⁡ B ∈ ℤ
22 8 14 21 syl2an ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℜ ⁡ A ⁢ ℑ ⁡ B ∈ ℤ
23 zmulcl ⊢ ℑ ⁡ A ∈ ℤ ∧ ℜ ⁡ B ∈ ℤ → ℑ ⁡ A ⁢ ℜ ⁡ B ∈ ℤ
24 13 10 23 syl2an ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℑ ⁡ A ⁢ ℜ ⁡ B ∈ ℤ
25 22 24 zaddcld ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℜ ⁡ A ⁢ ℑ ⁡ B + ℑ ⁡ A ⁢ ℜ ⁡ B ∈ ℤ
26 20 25 eqeltrd ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → ℑ ⁡ A ⁢ B ∈ ℤ
27 elgz ⊢ A ⁢ B ∈ ℤ i ↔ A ⁢ B ∈ ℂ ∧ ℜ ⁡ A ⁢ B ∈ ℤ ∧ ℑ ⁡ A ⁢ B ∈ ℤ
28 4 18 26 27 syl3anbrc ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → A ⁢ B ∈ ℤ i