This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 gcd 𝑦 ) = if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) ) )
2 gcdcl ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( 𝑥 gcd 𝑦 ) ∈ ℕ0 )
3 1 2 eqeltrrd ⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) ) ∈ ℕ0 )
4 3 rgen2 ⊢ ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) ) ∈ ℕ0
5 df-gcd ⊢ gcd = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℤ ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) ) )
6 5 fmpo ⊢ ( ∀ 𝑥 ∈ ℤ ∀ 𝑦 ∈ ℤ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) ) ∈ ℕ0 ↔ gcd : ( ℤ × ℤ ) ⟶ ℕ0 )
7 4 6 mpbi ⊢ gcd : ( ℤ × ℤ ) ⟶ ℕ0