Definition df-gcdOLD

Description: gcdOLD ( A , B ) is the largest positive integer that evenly divides both A and B . (Contributed by Jeff Hoffman, 17-Jun-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	df-gcdOLD	$$⊢{gcd}_{\mathrm{OLD}}\left(A,B\right)=sup\left(\left\{x\in \mathbb{N}|\left(\frac{A}{x}\in \mathbb{N}\wedge \frac{B}{x}\in \mathbb{N}\right)\right\},\mathbb{N},<\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1		cB	$$classB$$
2	0 1	cgcdOLD	$$class{gcd}_{\mathrm{OLD}}\left(A,B\right)$$
3		vx	$$setvarx$$
4		cn	$$class\mathbb{N}$$
5		cdiv	$$class÷$$
6	3	cv	$$setvarx$$
7	0 6 5	co	$$class\left(\frac{A}{x}\right)$$
8	7 4	wcel	$$wff\frac{A}{x}\in \mathbb{N}$$
9	1 6 5	co	$$class\left(\frac{B}{x}\right)$$
10	9 4	wcel	$$wff\frac{B}{x}\in \mathbb{N}$$
11	8 10	wa	$$wff\left(\frac{A}{x}\in \mathbb{N}\wedge \frac{B}{x}\in \mathbb{N}\right)$$
12	11 3 4	crab	$$class\left\{x\in \mathbb{N}|\left(\frac{A}{x}\in \mathbb{N}\wedge \frac{B}{x}\in \mathbb{N}\right)\right\}$$
13		clt	$$class<$$
14	12 4 13	csup	$$classsup\left(\left\{x\in \mathbb{N}|\left(\frac{A}{x}\in \mathbb{N}\wedge \frac{B}{x}\in \mathbb{N}\right)\right\},\mathbb{N},<\right)$$
15	2 14	wceq	$$wff{gcd}_{\mathrm{OLD}}\left(A,B\right)=sup\left(\left\{x\in \mathbb{N}|\left(\frac{A}{x}\in \mathbb{N}\wedge \frac{B}{x}\in \mathbb{N}\right)\right\},\mathbb{N},<\right)$$