Definition df-numer 11850

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 = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-numer

Step	Hyp	Ref	Expression
1		cnumer 11848	. 2 class numer
2		vy	. . 3 setvar y
3		cq 9404	. . 3 class QQ
4		vx	. . . . . . . . . 10 setvar x
5	4	cv 1330	. . . . . . . . 9 class x
6		c1st 6029	. . . . . . . . 9 class 1st
7	5, 6	cfv 5118	. . . . . . . 8 class ( 1st ` x )
8		c2nd 6030	. . . . . . . . 9 class 2nd
9	5, 8	cfv 5118	. . . . . . . 8 class ( 2nd ` x )
10		cgcd 11624	. . . . . . . 8 class gcd
11	7, 9, 10	co 5767	. . . . . . 7 class ( ( 1st ` x ) gcd ( 2nd ` x ) )
12		c1 7614	. . . . . . 7 class 1
13	11, 12	wceq 1331	. . . . . 6 wff ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1
14	2	cv 1330	. . . . . . 7 class y
15		cdiv 8425	. . . . . . . 8 class /
16	7, 9, 15	co 5767	. . . . . . 7 class ( ( 1st ` x ) / ( 2nd ` x ) )
17	14, 16	wceq 1331	. . . . . 6 wff y = ( ( 1st ` x ) / ( 2nd ` x ) )
18	13, 17	wa 103	. . . . 5 wff ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) )
19		cz 9047	. . . . . 6 class ZZ
20		cn 8713	. . . . . 6 class NN
21	19, 20	cxp 4532	. . . . 5 class ( ZZ X. NN )
22	18, 4, 21	crio 5722	. . . 4 class ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) )
23	22, 6	cfv 5118	. . 3 class ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) )
24	2, 3, 23	cmpt 3984	. 2 class ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
25	1, 24	wceq 1331	1 wff numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )

This definition is referenced by:  qnumval  11852  fnum  11857