Metamath Proof Explorer

Definition df-gcd

Description: Define the gcd operator. For example, ( -u 6 gcd 9 ) = 3 ( ex-gcd ). For an alternate definition, based on the definition in ApostolNT p. 15, see dfgcd2 . (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Assertion df-gcd ⊢ gcd = x ∈ ℤ , y ∈ ℤ ⟼ if x = 0 ∧ y = 0 0 sup n ∈ ℤ | n ∥ x ∧ n ∥ y ℝ <

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgcd class gcd
1 vx setvar x
2 cz class ℤ
3 vy setvar y
4 1 cv setvar x
5 cc0 class 0
6 4 5 wceq wff x = 0
7 3 cv setvar y
8 7 5 wceq wff y = 0
9 6 8 wa wff x = 0 ∧ y = 0
10 vn setvar n
11 10 cv setvar n
12 cdvds class ∥
13 11 4 12 wbr wff n ∥ x
14 11 7 12 wbr wff n ∥ y
15 13 14 wa wff n ∥ x ∧ n ∥ y
16 15 10 2 crab class n ∈ ℤ | n ∥ x ∧ n ∥ y
17 cr class ℝ
18 clt class <
19 16 17 18 csup class sup n ∈ ℤ | n ∥ x ∧ n ∥ y ℝ <
20 9 5 19 cif class if x = 0 ∧ y = 0 0 sup n ∈ ℤ | n ∥ x ∧ n ∥ y ℝ <
21 1 3 2 2 20 cmpo class x ∈ ℤ , y ∈ ℤ ⟼ if x = 0 ∧ y = 0 0 sup n ∈ ℤ | n ∥ x ∧ n ∥ y ℝ <
22 0 21 wceq wff gcd = x ∈ ℤ , y ∈ ℤ ⟼ if x = 0 ∧ y = 0 0 sup n ∈ ℤ | n ∥ x ∧ n ∥ y ℝ <