Definition df-gcdOLD 33808

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 33807	. 2 class gcdOLD (𝐴, 𝐵)
4		vx	. . . . . . . 8 setvar 𝑥
5	4	cv 1536	. . . . . . 7 class 𝑥
6		cdiv 11297	. . . . . . 7 class /
7	1, 5, 6	co 7156	. . . . . 6 class (𝐴 / 𝑥)
8		cn 11638	. . . . . 6 class ℕ
9	7, 8	wcel 2114	. . . . 5 wff (𝐴 / 𝑥) ∈ ℕ
10	2, 5, 6	co 7156	. . . . . 6 class (𝐵 / 𝑥)
11	10, 8	wcel 2114	. . . . 5 wff (𝐵 / 𝑥) ∈ ℕ
12	9, 11	wa 398	. . . 4 wff ((𝐴 / 𝑥) ∈ ℕ ∧ (𝐵 / 𝑥) ∈ ℕ)
13	12, 4, 8	crab 3142	. . 3 class {𝑥 ∈ ℕ ∣ ((𝐴 / 𝑥) ∈ ℕ ∧ (𝐵 / 𝑥) ∈ ℕ)}
14		clt 10675	. . 3 class <
15	13, 8, 14	csup 8904	. 2 class sup({𝑥 ∈ ℕ ∣ ((𝐴 / 𝑥) ∈ ℕ ∧ (𝐵 / 𝑥) ∈ ℕ)}, ℕ, < )
16	3, 15	wceq 1537	1 wff gcdOLD (𝐴, 𝐵) = sup({𝑥 ∈ ℕ ∣ ((𝐴 / 𝑥) ∈ ℕ ∧ (𝐵 / 𝑥) ∈ ℕ)}, ℕ, < )

This definition is referenced by:  ee7.2aOLD  33809