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

Definition df-denom 13159
 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 13157 . 2 denom
2 vy . . 3
3 cq 10605 . . 3
4 vx . . . . . . . . . 10
54cv 1652 . . . . . . . . 9
6 c1st 6376 . . . . . . . . 9
75, 6cfv 5483 . . . . . . . 8
8 c2nd 6377 . . . . . . . . 9
95, 8cfv 5483 . . . . . . . 8
10 cgcd 13037 . . . . . . . 8
117, 9, 10co 6110 . . . . . . 7
12 c1 9022 . . . . . . 7
1311, 12wceq 1653 . . . . . 6
142cv 1652 . . . . . . 7
15 cdiv 9708 . . . . . . . 8
167, 9, 15co 6110 . . . . . . 7
1714, 16wceq 1653 . . . . . 6
1813, 17wa 360 . . . . 5
19 cz 10313 . . . . . 6
20 cn 10031 . . . . . 6
2119, 20cxp 4905 . . . . 5
2218, 4, 21crio 6571 . . . 4
2322, 8cfv 5483 . . 3
242, 3, 23cmpt 4291 . 2
251, 24wceq 1653 1 denom
 Colors of variables: wff set class This definition is referenced by:  qdenval  13161  fden  13166
 Copyright terms: Public domain W3C validator