Metamath Proof Explorer

Theorem gcdf

Description: Domain and codomain of the gcd operator. (Contributed by Paul Chapman, 31-Mar-2011) (Revised by Mario Carneiro, 16-Nov-2013)

Ref Expression
Assertion gcdf ⊢ gcd : ℤ × ℤ ⟶ ℕ 0

Proof

Step Hyp Ref Expression
1 gcdval ⊢ x ∈ ℤ ∧ y ∈ ℤ → x gcd y = if x = 0 ∧ y = 0 0 sup n ∈ ℤ | n ∥ x ∧ n ∥ y ℝ <
2 gcdcl ⊢ x ∈ ℤ ∧ y ∈ ℤ → x gcd y ∈ ℕ 0
3 1 2 eqeltrrd ⊢ x ∈ ℤ ∧ y ∈ ℤ → if x = 0 ∧ y = 0 0 sup n ∈ ℤ | n ∥ x ∧ n ∥ y ℝ < ∈ ℕ 0
4 3 rgen2 ⊢ ∀ x ∈ ℤ ∀ y ∈ ℤ if x = 0 ∧ y = 0 0 sup n ∈ ℤ | n ∥ x ∧ n ∥ y ℝ < ∈ ℕ 0
5 df-gcd ⊢ gcd = x ∈ ℤ , y ∈ ℤ ⟼ if x = 0 ∧ y = 0 0 sup n ∈ ℤ | n ∥ x ∧ n ∥ y ℝ <
6 5 fmpo ⊢ ∀ x ∈ ℤ ∀ y ∈ ℤ if x = 0 ∧ y = 0 0 sup n ∈ ℤ | n ∥ x ∧ n ∥ y ℝ < ∈ ℕ 0 ↔ gcd : ℤ × ℤ ⟶ ℕ 0
7 4 6 mpbi ⊢ gcd : ℤ × ℤ ⟶ ℕ 0