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 ( 𝐴 , 𝐵 ) = sup ( { 𝑥 ∈ ℕ ∣ ( ( 𝐴 / 𝑥 ) ∈ ℕ ∧ ( 𝐵 / 𝑥 ) ∈ ℕ ) } , ℕ , < )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cB	⊢ 𝐵
2	0 1	cgcdOLD	⊢ gcdOLD ( 𝐴 , 𝐵 )
3		vx	⊢ 𝑥
4		cn	⊢ ℕ
5		cdiv	⊢ /
6	3	cv	⊢ 𝑥
7	0 6 5	co	⊢ ( 𝐴 / 𝑥 )
8	7 4	wcel	⊢ ( 𝐴 / 𝑥 ) ∈ ℕ
9	1 6 5	co	⊢ ( 𝐵 / 𝑥 )
10	9 4	wcel	⊢ ( 𝐵 / 𝑥 ) ∈ ℕ
11	8 10	wa	⊢ ( ( 𝐴 / 𝑥 ) ∈ ℕ ∧ ( 𝐵 / 𝑥 ) ∈ ℕ )
12	11 3 4	crab	⊢ { 𝑥 ∈ ℕ ∣ ( ( 𝐴 / 𝑥 ) ∈ ℕ ∧ ( 𝐵 / 𝑥 ) ∈ ℕ ) }
13		clt	⊢ <
14	12 4 13	csup	⊢ sup ( { 𝑥 ∈ ℕ ∣ ( ( 𝐴 / 𝑥 ) ∈ ℕ ∧ ( 𝐵 / 𝑥 ) ∈ ℕ ) } , ℕ , < )
15	2 14	wceq	⊢ gcdOLD ( 𝐴 , 𝐵 ) = sup ( { 𝑥 ∈ ℕ ∣ ( ( 𝐴 / 𝑥 ) ∈ ℕ ∧ ( 𝐵 / 𝑥 ) ∈ ℕ ) } , ℕ , < )