Metamath Proof Explorer

Theorem gzreim

Description: Construct a gaussian integer from real and imaginary parts. (Contributed by Mario Carneiro, 16-Jul-2014)

Ref Expression
Assertion gzreim ⊢ A ∈ ℤ ∧ B ∈ ℤ → A + i ⁢ B ∈ ℤ i

Proof

Step Hyp Ref Expression
1 zgz ⊢ A ∈ ℤ → A ∈ ℤ i
2 igz ⊢ i ∈ ℤ i
3 zgz ⊢ B ∈ ℤ → B ∈ ℤ i
4 gzmulcl ⊢ i ∈ ℤ i ∧ B ∈ ℤ i → i ⁢ B ∈ ℤ i
5 2 3 4 sylancr ⊢ B ∈ ℤ → i ⁢ B ∈ ℤ i
6 gzaddcl ⊢ A ∈ ℤ i ∧ i ⁢ B ∈ ℤ i → A + i ⁢ B ∈ ℤ i
7 1 5 6 syl2an ⊢ A ∈ ℤ ∧ B ∈ ℤ → A + i ⁢ B ∈ ℤ i