Theorem gzmulclALT

Description: The gaussian integers are closed under multiplication. Alternate (shorter) proof. (Contributed by AV, 25-Oct-2026) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ax-icn	⊢ i ∈ ℂ
2		i2	⊢ ( i ↑ 2 ) = - 1
3		neg1z	⊢ - 1 ∈ ℤ
4		zgz	⊢ ( - 1 ∈ ℤ → - 1 ∈ ℤ[i] )
5	3 4	ax-mp	⊢ - 1 ∈ ℤ[i]
6	2 5	eqeltri	⊢ ( i ↑ 2 ) ∈ ℤ[i]
7		gzilaz	⊢ ℤ[i] = ( Z[]l ‘ i )
8	7	lazmulcl	⊢ ( ( i ∈ ℂ ∧ ( i ↑ 2 ) ∈ ℤ[i] ) → ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( 𝐴 · 𝐵 ) ∈ ℤ[i] ) )
9	1 6 8	mp2an	⊢ ( ( 𝐴 ∈ ℤ[i] ∧ 𝐵 ∈ ℤ[i] ) → ( 𝐴 · 𝐵 ) ∈ ℤ[i] )