Metamath Proof Explorer

Definition df-denom

Description: The canonical denominator of a rational is the denominator of the rational's reduced fraction representation (no common factors, denominator positive). (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion df-denom 
|- denom = ( y e. QQ |-> ( 2nd ` ( 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 cdenom 
 |-  denom
1 vy 
 |-  y
2 cq 
 |-  QQ
3 c2nd 
 |-  2nd
4 vx 
 |-  x
5 cz 
 |-  ZZ
6 cn 
 |-  NN
7 5 6 cxp 
 |-  ( ZZ X. NN )
8 c1st 
 |-  1st
9 4 cv 
 |-  x
10 9 8 cfv 
 |-  ( 1st ` x )
11 cgcd 
 |-  gcd
12 9 3 cfv 
 |-  ( 2nd ` x )
13 10 12 11 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 10 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 
 |-  ( 2nd ` ( 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 |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )
24 0 23 wceq 
 |-  denom = ( y e. QQ |-> ( 2nd ` ( iota_ x e. ( ZZ X. NN ) ( ( ( 1st ` x ) gcd ( 2nd ` x ) ) = 1 /\ y = ( ( 1st ` x ) / ( 2nd ` x ) ) ) ) ) )