Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-denom Structured version   Unicode version

Definition df-denom 14645
 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.)
Assertion
Ref Expression
df-denom denom
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-denom
StepHypRef Expression
1 cdenom 14643 . 2 denom
2 vy . . 3
3 cq 11253 . . 3
4 vx . . . . . . . . . 10
54cv 1436 . . . . . . . . 9
6 c1st 6796 . . . . . . . . 9
75, 6cfv 5592 . . . . . . . 8
8 c2nd 6797 . . . . . . . . 9
95, 8cfv 5592 . . . . . . . 8
10 cgcd 14431 . . . . . . . 8
117, 9, 10co 6296 . . . . . . 7
12 c1 9529 . . . . . . 7
1311, 12wceq 1437 . . . . . 6
142cv 1436 . . . . . . 7
15 cdiv 10258 . . . . . . . 8
167, 9, 15co 6296 . . . . . . 7
1714, 16wceq 1437 . . . . . 6
1813, 17wa 370 . . . . 5
19 cz 10926 . . . . . 6
20 cn 10598 . . . . . 6
2119, 20cxp 4843 . . . . 5
2218, 4, 21crio 6257 . . . 4
2322, 8cfv 5592 . . 3
242, 3, 23cmpt 4475 . 2
251, 24wceq 1437 1 denom
 Colors of variables: wff setvar class This definition is referenced by:  qdenval  14647  fden  14652
 Copyright terms: Public domain W3C validator