Mathbox for Jeff Hoffman < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-gcdOLD Structured version   Visualization version   GIF version

Definition df-gcdOLD 31629
 Description: gcdOLD (𝐴, 𝐵) 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
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cgcdOLD 31628 . 2 class gcdOLD (𝐴, 𝐵)
4 vx . . . . . . . 8 setvar 𝑥
54cv 1474 . . . . . . 7 class 𝑥
6 cdiv 10563 . . . . . . 7 class /
71, 5, 6co 6549 . . . . . 6 class (𝐴 / 𝑥)
8 cn 10897 . . . . . 6 class
97, 8wcel 1977 . . . . 5 wff (𝐴 / 𝑥) ∈ ℕ
102, 5, 6co 6549 . . . . . 6 class (𝐵 / 𝑥)
1110, 8wcel 1977 . . . . 5 wff (𝐵 / 𝑥) ∈ ℕ
129, 11wa 383 . . . 4 wff ((𝐴 / 𝑥) ∈ ℕ ∧ (𝐵 / 𝑥) ∈ ℕ)
1312, 4, 8crab 2900 . . 3 class {𝑥 ∈ ℕ ∣ ((𝐴 / 𝑥) ∈ ℕ ∧ (𝐵 / 𝑥) ∈ ℕ)}
14 clt 9953 . . 3 class <
1513, 8, 14csup 8229 . 2 class sup({𝑥 ∈ ℕ ∣ ((𝐴 / 𝑥) ∈ ℕ ∧ (𝐵 / 𝑥) ∈ ℕ)}, ℕ, < )
163, 15wceq 1475 1 wff gcdOLD (𝐴, 𝐵) = sup({𝑥 ∈ ℕ ∣ ((𝐴 / 𝑥) ∈ ℕ ∧ (𝐵 / 𝑥) ∈ ℕ)}, ℕ, < )
 Colors of variables: wff setvar class This definition is referenced by:  ee7.2aOLD  31630
 Copyright terms: Public domain W3C validator