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] )