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 = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℤ ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgcd	⊢ gcd
1		vx	⊢ 𝑥
2		cz	⊢ ℤ
3		vy	⊢ 𝑦
4	1	cv	⊢ 𝑥
5		cc0	⊢ 0
6	4 5	wceq	⊢ 𝑥 = 0
7	3	cv	⊢ 𝑦
8	7 5	wceq	⊢ 𝑦 = 0
9	6 8	wa	⊢ ( 𝑥 = 0 ∧ 𝑦 = 0 )
10		vn	⊢ 𝑛
11	10	cv	⊢ 𝑛
12		cdvds	⊢ ∥
13	11 4 12	wbr	⊢ 𝑛 ∥ 𝑥
14	11 7 12	wbr	⊢ 𝑛 ∥ 𝑦
15	13 14	wa	⊢ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 )
16	15 10 2	crab	⊢ { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) }
17		cr	⊢ ℝ
18		clt	⊢ <
19	16 17 18	csup	⊢ sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < )
20	9 5 19	cif	⊢ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) )
21	1 3 2 2 20	cmpo	⊢ ( 𝑥 ∈ ℤ , 𝑦 ∈ ℤ ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) ) )
22	0 21	wceq	⊢ gcd = ( 𝑥 ∈ ℤ , 𝑦 ∈ ℤ ↦ if ( ( 𝑥 = 0 ∧ 𝑦 = 0 ) , 0 , sup ( { 𝑛 ∈ ℤ ∣ ( 𝑛 ∥ 𝑥 ∧ 𝑛 ∥ 𝑦 ) } , ℝ , < ) ) )