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

Step	Hyp	Ref	Expression
1		cdenom 14267	. 2
2		vy	. . 3
3		cq 11211	. . 3
4		vx	. . . . . . . . . 10
5	4	cv 1394	. . . . . . . . 9
6		c1st 6798	. . . . . . . . 9
7	5, 6	cfv 5593	. . . . . . . 8
8		c2nd 6799	. . . . . . . . 9
9	5, 8	cfv 5593	. . . . . . . 8
10		cgcd 14144	. . . . . . . 8
11	7, 9, 10	co 6296	. . . . . . 7
12		c1 9514	. . . . . . 7
13	11, 12	wceq 1395	. . . . . 6
14	2	cv 1394	. . . . . . 7
15		cdiv 10231	. . . . . . . 8
16	7, 9, 15	co 6296	. . . . . . 7
17	14, 16	wceq 1395	. . . . . 6
18	13, 17	wa 369	. . . . 5
19		cz 10889	. . . . . 6
20		cn 10561	. . . . . 6
21	19, 20	cxp 5002	. . . . 5
22	18, 4, 21	crio 6256	. . . 4
23	22, 8	cfv 5593	. . 3
24	2, 3, 23	cmpt 4510	. 2
25	1, 24	wceq 1395	1

This definition is referenced by:  qdenval  14271  fden  14276