Definition df-gcdOLD 32459

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.)

Assertion

Ref	Expression
df-gcdOLD	|- gcdOLD ( A , B ) = sup ( { x e. NN | ( ( A / x ) e. NN /\ ( B / x ) e. NN ) } , NN , < )

Distinct variable groups:   x, A   x, B

Detailed syntax breakdown of Definition df-gcdOLD

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cgcdOLD 32458	. 2 class gcdOLD ( A , B )
4		vx	. . . . . . . 8 setvar x
5	4	cv 1482	. . . . . . 7 class x
6		cdiv 10684	. . . . . . 7 class /
7	1, 5, 6	co 6650	. . . . . 6 class ( A / x )
8		cn 11020	. . . . . 6 class NN
9	7, 8	wcel 1990	. . . . 5 wff ( A / x ) e. NN
10	2, 5, 6	co 6650	. . . . . 6 class ( B / x )
11	10, 8	wcel 1990	. . . . 5 wff ( B / x ) e. NN
12	9, 11	wa 384	. . . 4 wff ( ( A / x ) e. NN /\ ( B / x ) e. NN )
13	12, 4, 8	crab 2916	. . 3 class { x e. NN | ( ( A / x ) e. NN /\ ( B / x ) e. NN ) }
14		clt 10074	. . 3 class <
15	13, 8, 14	csup 8346	. 2 class sup ( { x e. NN | ( ( A / x ) e. NN /\ ( B / x ) e. NN ) } , NN , < )
16	3, 15	wceq 1483	1 wff gcdOLD ( A , B ) = sup ( { x e. NN | ( ( A / x ) e. NN /\ ( B / x ) e. NN ) } , NN , < )

This definition is referenced by:  ee7.2aOLD  32460