Definition df-numer 16772

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

Step	Hyp	Ref	Expression
1		cnumer 16770	. 2 class numer
2		vy	. . 3 setvar 𝑦
3		cq 12990	. . 3 class ℚ
4		vx	. . . . . . . . . 10 setvar 𝑥
5	4	cv 1539	. . . . . . . . 9 class 𝑥
6		c1st 8012	. . . . . . . . 9 class 1st
7	5, 6	cfv 6561	. . . . . . . 8 class (1st ‘𝑥)
8		c2nd 8013	. . . . . . . . 9 class 2nd
9	5, 8	cfv 6561	. . . . . . . 8 class (2nd ‘𝑥)
10		cgcd 16531	. . . . . . . 8 class gcd
11	7, 9, 10	co 7431	. . . . . . 7 class ((1st ‘𝑥) gcd (2nd ‘𝑥))
12		c1 11156	. . . . . . 7 class 1
13	11, 12	wceq 1540	. . . . . 6 wff ((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1
14	2	cv 1539	. . . . . . 7 class 𝑦
15		cdiv 11920	. . . . . . . 8 class /
16	7, 9, 15	co 7431	. . . . . . 7 class ((1st ‘𝑥) / (2nd ‘𝑥))
17	14, 16	wceq 1540	. . . . . 6 wff 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥))
18	13, 17	wa 395	. . . . 5 wff (((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥)))
19		cz 12613	. . . . . 6 class ℤ
20		cn 12266	. . . . . 6 class ℕ
21	19, 20	cxp 5683	. . . . 5 class (ℤ × ℕ)
22	18, 4, 21	crio 7387	. . . 4 class (℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥))))
23	22, 6	cfv 6561	. . 3 class (1st ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥)))))
24	2, 3, 23	cmpt 5225	. 2 class (𝑦 ∈ ℚ ↦ (1st ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥))))))
25	1, 24	wceq 1540	1 wff numer = (𝑦 ∈ ℚ ↦ (1st ‘(℩𝑥 ∈ (ℤ × ℕ)(((1st ‘𝑥) gcd (2nd ‘𝑥)) = 1 ∧ 𝑦 = ((1st ‘𝑥) / (2nd ‘𝑥))))))

This definition is referenced by:  qnumval  16774  fnum  16779