Metamath Proof Explorer

Definition df-numer

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)

Ref Expression
Assertion df-numer 
|- numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnumer 
 |-  numer
1 vy 
 |-  y
2 cq 
 |-  QQ
3 c1st 
 |-  1st
4 vx 
 |-  x
5 cz 
 |-  ZZ
6 cn 
 |-  NN
7 5 6 cxp 
 |-  ( ZZ X. NN )
8 4 cv 
 |-  x
9 8 3 cfv 
 |-  ( 1st ` x )
10 cgcd 
 |-  gcd
11 c2nd 
 |-  2nd
12 8 11 cfv 
 |-  ( 2nd ` x )
13 9 12 10 co 
 |-  ( ( 1st ` x ) gcd ( 2nd ` x ) )
14 c1 
 |-  1
15 13 14 wceq 
 |-  ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1
16 1 cv 
 |-  y
17 cdiv 
 |-  /
18 9 12 17 co 
 |-  ( ( 1st ` x ) / ( 2nd ` x ) )
19 16 18 wceq 
 |-  y = ( ( 1st ` x ) / ( 2nd ` x ) )
20 15 19 wa 
 |-  ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) )
21 20 4 7 crio 
 |-  ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) )
22 21 3 cfv 
 |-  ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) )
23 1 2 22 cmpt 
 |-  ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
24 0 23 wceq 
 |-  numer = ( y e. QQ |-> ( 1st ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )