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

Definition df-denom 14269
 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
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-denom
StepHypRef Expression
1 cdenom 14267 . 2
2 vy . . 3
3 cq 11211 . . 3
4 vx . . . . . . . . . 10
54cv 1394 . . . . . . . . 9
6 c1st 6798 . . . . . . . . 9
75, 6cfv 5593 . . . . . . . 8
8 c2nd 6799 . . . . . . . . 9
95, 8cfv 5593 . . . . . . . 8
10 cgcd 14144 . . . . . . . 8
117, 9, 10co 6296 . . . . . . 7
12 c1 9514 . . . . . . 7
1311, 12wceq 1395 . . . . . 6
142cv 1394 . . . . . . 7
15 cdiv 10231 . . . . . . . 8
167, 9, 15co 6296 . . . . . . 7
1714, 16wceq 1395 . . . . . 6
1813, 17wa 369 . . . . 5
19 cz 10889 . . . . . 6
20 cn 10561 . . . . . 6
2119, 20cxp 5002 . . . . 5
2218, 4, 21crio 6256 . . . 4
2322, 8cfv 5593 . . 3
242, 3, 23cmpt 4510 . 2
251, 24wceq 1395 1
 Colors of variables: wff setvar class This definition is referenced by:  qdenval  14271  fden  14276
 Copyright terms: Public domain W3C validator