MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-numer Structured version   Visualization version   GIF version

Definition df-numer 15227
Description: The canonical numerator of a rational is the numerator of the rational's reduced fraction representation (no common factors, denominator positive). (Contributed by Stefan O'Rear, 13-Sep-2014.)
Assertion
Ref Expression
df-numer numer = (𝑦 ∈ ℚ ↦ (1st ‘(𝑥 ∈ (ℤ × ℕ)(((1st𝑥) gcd (2nd𝑥)) = 1 ∧ 𝑦 = ((1st𝑥) / (2nd𝑥))))))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-numer
StepHypRef Expression
1 cnumer 15225 . 2 class numer
2 vy . . 3 setvar 𝑦
3 cq 11620 . . 3 class
4 vx . . . . . . . . . 10 setvar 𝑥
54cv 1473 . . . . . . . . 9 class 𝑥
6 c1st 7034 . . . . . . . . 9 class 1st
75, 6cfv 5790 . . . . . . . 8 class (1st𝑥)
8 c2nd 7035 . . . . . . . . 9 class 2nd
95, 8cfv 5790 . . . . . . . 8 class (2nd𝑥)
10 cgcd 15000 . . . . . . . 8 class gcd
117, 9, 10co 6527 . . . . . . 7 class ((1st𝑥) gcd (2nd𝑥))
12 c1 9793 . . . . . . 7 class 1
1311, 12wceq 1474 . . . . . 6 wff ((1st𝑥) gcd (2nd𝑥)) = 1
142cv 1473 . . . . . . 7 class 𝑦
15 cdiv 10533 . . . . . . . 8 class /
167, 9, 15co 6527 . . . . . . 7 class ((1st𝑥) / (2nd𝑥))
1714, 16wceq 1474 . . . . . 6 wff 𝑦 = ((1st𝑥) / (2nd𝑥))
1813, 17wa 382 . . . . 5 wff (((1st𝑥) gcd (2nd𝑥)) = 1 ∧ 𝑦 = ((1st𝑥) / (2nd𝑥)))
19 cz 11210 . . . . . 6 class
20 cn 10867 . . . . . 6 class
2119, 20cxp 5026 . . . . 5 class (ℤ × ℕ)
2218, 4, 21crio 6488 . . . 4 class (𝑥 ∈ (ℤ × ℕ)(((1st𝑥) gcd (2nd𝑥)) = 1 ∧ 𝑦 = ((1st𝑥) / (2nd𝑥))))
2322, 6cfv 5790 . . 3 class (1st ‘(𝑥 ∈ (ℤ × ℕ)(((1st𝑥) gcd (2nd𝑥)) = 1 ∧ 𝑦 = ((1st𝑥) / (2nd𝑥)))))
242, 3, 23cmpt 4637 . 2 class (𝑦 ∈ ℚ ↦ (1st ‘(𝑥 ∈ (ℤ × ℕ)(((1st𝑥) gcd (2nd𝑥)) = 1 ∧ 𝑦 = ((1st𝑥) / (2nd𝑥))))))
251, 24wceq 1474 1 wff numer = (𝑦 ∈ ℚ ↦ (1st ‘(𝑥 ∈ (ℤ × ℕ)(((1st𝑥) gcd (2nd𝑥)) = 1 ∧ 𝑦 = ((1st𝑥) / (2nd𝑥))))))
Colors of variables: wff setvar class
This definition is referenced by:  qnumval  15229  fnum  15234
  Copyright terms: Public domain W3C validator