Metamath Proof Explorer

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 ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → A ⁢ B ∈ ℤ 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 Could not format Z[i] = ( Z[]l ` _i ) : No typesetting found for |- Z[i] = ( Z[]l ` _i ) with typecode |-
8 7 lazmulcl ⊢ i ∈ ℂ ∧ i 2 ∈ ℤ i → A ∈ ℤ i ∧ B ∈ ℤ i → A ⁢ B ∈ ℤ i
9 1 6 8 mp2an ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → A ⁢ B ∈ ℤ i