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 =\left(x\in \mathbb{Z},y\in \mathbb{Z}⟼if\left(\left(x=0\wedge y=0\right),0,sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel x\wedge n\parallel y\right)\right\},ℝ,<\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgcd	$$class\gcd$$
1		vx	$$setvarx$$
2		cz	$$class\mathbb{Z}$$
3		vy	$$setvary$$
4	1	cv	$$setvarx$$
5		cc0	$$class0$$
6	4 5	wceq	$$wffx=0$$
7	3	cv	$$setvary$$
8	7 5	wceq	$$wffy=0$$
9	6 8	wa	$$wff\left(x=0\wedge y=0\right)$$
10		vn	$$setvarn$$
11	10	cv	$$setvarn$$
12		cdvds	$$class\parallel$$
13	11 4 12	wbr	$$wffn\parallel x$$
14	11 7 12	wbr	$$wffn\parallel y$$
15	13 14	wa	$$wff\left(n\parallel x\wedge n\parallel y\right)$$
16	15 10 2	crab	$$class\left\{n\in \mathbb{Z}|\left(n\parallel x\wedge n\parallel y\right)\right\}$$
17		cr	$$classℝ$$
18		clt	$$class<$$
19	16 17 18	csup	$$classsup\left(\left\{n\in \mathbb{Z}|\left(n\parallel x\wedge n\parallel y\right)\right\},ℝ,<\right)$$
20	9 5 19	cif	$$classif\left(\left(x=0\wedge y=0\right),0,sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel x\wedge n\parallel y\right)\right\},ℝ,<\right)\right)$$
21	1 3 2 2 20	cmpo	$$class\left(x\in \mathbb{Z},y\in \mathbb{Z}⟼if\left(\left(x=0\wedge y=0\right),0,sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel x\wedge n\parallel y\right)\right\},ℝ,<\right)\right)\right)$$
22	0 21	wceq	$$wff\gcd =\left(x\in \mathbb{Z},y\in \mathbb{Z}⟼if\left(\left(x=0\wedge y=0\right),0,sup\left(\left\{n\in \mathbb{Z}|\left(n\parallel x\wedge n\parallel y\right)\right\},ℝ,<\right)\right)\right)$$