Definition df-gcdOLD 32459

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

Assertion

Ref	Expression
df-gcdOLD	⊢ gcdOLD (𝐴, 𝐵) = sup({𝑥 ∈ ℕ ∣ ((𝐴 / 𝑥) ∈ ℕ ∧ (𝐵 / 𝑥) ∈ ℕ)}, ℕ, < )

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Detailed syntax breakdown of Definition df-gcdOLD

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

This definition is referenced by:  ee7.2aOLD  32460