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 e. Z[i] /\ B e. Z[i] ) -> ( A x. B ) e. Z[i] ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-icn | |- _i e. CC |
|
| 2 | i2 | |- ( _i ^ 2 ) = -u 1 |
|
| 3 | neg1z | |- -u 1 e. ZZ |
|
| 4 | zgz | |- ( -u 1 e. ZZ -> -u 1 e. Z[i] ) |
|
| 5 | 3 4 | ax-mp | |- -u 1 e. Z[i] |
| 6 | 2 5 | eqeltri | |- ( _i ^ 2 ) e. Z[i] |
| 7 | gzilaz | |- Z[i] = ( Z[]l ` _i ) |
|
| 8 | 7 | lazmulcl | |- ( ( _i e. CC /\ ( _i ^ 2 ) e. Z[i] ) -> ( ( A e. Z[i] /\ B e. Z[i] ) -> ( A x. B ) e. Z[i] ) ) |
| 9 | 1 6 8 | mp2an | |- ( ( A e. Z[i] /\ B e. Z[i] ) -> ( A x. B ) e. Z[i] ) |