Metamath Proof Explorer

Theorem gzsubcl

Description: The gaussian integers are closed under subtraction. (Contributed by Mario Carneiro, 14-Jul-2014)

Ref Expression
Assertion gzsubcl ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → A − B ∈ ℤ i

Proof

Step Hyp Ref Expression
1 gzcn ⊢ A ∈ ℤ i → A ∈ ℂ
2 gzcn ⊢ B ∈ ℤ i → B ∈ ℂ
3 negsub ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + − B = A − B
4 1 2 3 syl2an ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → A + − B = A − B
5 gznegcl ⊢ B ∈ ℤ i → − B ∈ ℤ i
6 gzaddcl ⊢ A ∈ ℤ i ∧ − B ∈ ℤ i → A + − B ∈ ℤ i
7 5 6 sylan2 ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → A + − B ∈ ℤ i
8 4 7 eqeltrrd ⊢ A ∈ ℤ i ∧ B ∈ ℤ i → A − B ∈ ℤ i