This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gzmulcl

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

Ref Expression
Assertion gzmulcl ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( 𝐴 · 𝐵 ) ∈ ℤ[i] )

Proof

Step Hyp Ref Expression
1 gzcn ⊢ ( 𝐴 ∈ ℤ[i] → 𝐴 ∈ ℂ )
2 gzcn ⊢ ( 𝐵 ∈ ℤ[i] → 𝐵 ∈ ℂ )
3 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
4 1 2 3 syl2an ⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
5 remul ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℜ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) )
6 1 2 5 syl2an ⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( ℜ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) )
7 elgz ⊢ ( 𝐴 ∈ ℤ[i] ↔ ( 𝐴 ∈ ℂ ∧ ( ℜ ‘ 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ 𝐴 ) ∈ ℤ ) )
8 7 simp2bi ⊢ ( 𝐴 ∈ ℤ[i] → ( ℜ ‘ 𝐴 ) ∈ ℤ )
9 elgz ⊢ ( 𝐵 ∈ ℤ[i] ↔ ( 𝐵 ∈ ℂ ∧ ( ℜ ‘ 𝐵 ) ∈ ℤ ∧ ( ℑ ‘ 𝐵 ) ∈ ℤ ) )
10 9 simp2bi ⊢ ( 𝐵 ∈ ℤ[i] → ( ℜ ‘ 𝐵 ) ∈ ℤ )
11 zmulcl ⊢ ( ( ( ℜ ‘ 𝐴 ) ∈ ℤ ∧ ( ℜ ‘ 𝐵 ) ∈ ℤ ) → ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℤ )
12 8 10 11 syl2an ⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℤ )
13 7 simp3bi ⊢ ( 𝐴 ∈ ℤ[i] → ( ℑ ‘ 𝐴 ) ∈ ℤ )
14 9 simp3bi ⊢ ( 𝐵 ∈ ℤ[i] → ( ℑ ‘ 𝐵 ) ∈ ℤ )
15 zmulcl ⊢ ( ( ( ℑ ‘ 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ 𝐵 ) ∈ ℤ ) → ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℤ )
16 13 14 15 syl2an ⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℤ )
17 12 16 zsubcld ⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( ( ( ℜ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ ℤ )
18 6 17 eqeltrd ⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( ℜ ‘ ( 𝐴 · 𝐵 ) ) ∈ ℤ )
19 immul ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) )
20 1 2 19 syl2an ⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( ℑ ‘ ( 𝐴 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) )
21 zmulcl ⊢ ( ( ( ℜ ‘ 𝐴 ) ∈ ℤ ∧ ( ℑ ‘ 𝐵 ) ∈ ℤ ) → ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℤ )
22 8 14 21 syl2an ⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℤ )
23 zmulcl ⊢ ( ( ( ℑ ‘ 𝐴 ) ∈ ℤ ∧ ( ℜ ‘ 𝐵 ) ∈ ℤ ) → ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℤ )
24 13 10 23 syl2an ⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℤ )
25 22 24 zaddcld ⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( ( ( ℜ ‘ 𝐴 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐴 ) · ( ℜ ‘ 𝐵 ) ) ) ∈ ℤ )
26 20 25 eqeltrd ⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( ℑ ‘ ( 𝐴 · 𝐵 ) ) ∈ ℤ )
27 elgz ⊢ ( ( 𝐴 · 𝐵 ) ∈ ℤ[i] ↔ ( ( 𝐴 · 𝐵 ) ∈ ℂ ∧ ( ℜ ‘ ( 𝐴 · 𝐵 ) ) ∈ ℤ ∧ ( ℑ ‘ ( 𝐴 · 𝐵 ) ) ∈ ℤ ) )
28 4 18 26 27 syl3anbrc ⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( 𝐴 · 𝐵 ) ∈ ℤ[i] )