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