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	|- gcdOLD ( A , B ) = sup ( { x e. NN | ( ( A / x ) e. NN /\ ( B / x ) e. NN ) } , NN , < )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1		cB	|- B
2	0 1	cgcdOLD	|- gcdOLD ( A , B )
3		vx	|- x
4		cn	|- NN
5		cdiv	|- /
6	3	cv	|- x
7	0 6 5	co	|- ( A / x )
8	7 4	wcel	|- ( A / x ) e. NN
9	1 6 5	co	|- ( B / x )
10	9 4	wcel	|- ( B / x ) e. NN
11	8 10	wa	|- ( ( A / x ) e. NN /\ ( B / x ) e. NN )
12	11 3 4	crab	|- { x e. NN | ( ( A / x ) e. NN /\ ( B / x ) e. NN ) }
13		clt	|- <
14	12 4 13	csup	|- sup ( { x e. NN | ( ( A / x ) e. NN /\ ( B / x ) e. NN ) } , NN , < )
15	2 14	wceq	|- gcdOLD ( A , B ) = sup ( { x e. NN | ( ( A / x ) e. NN /\ ( B / x ) e. NN ) } , NN , < )