df-numer - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > df-numer		Unicode version

Definition df-numer 12961

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

**Assertion**
Ref	Expression
df-numer	numer $/\$

Distinct variable group:

**Detailed syntax breakdown of Definition df-numer**
Step	Hyp	Ref	Expression
1		cnumer 12959	. 2 numer
2		vy	. . 3
3		cq 10019	. . 3
4		vx	. . . . . . . . . 10
5	4	cv 1401	. . . . . . . . 9
6		c1st 6372	. . . . . . . . 9
7	5, 6	cfv 5377	. . . . . . . 8
8		c2nd 6373	. . . . . . . . 9
9	5, 8	cfv 5377	. . . . . . . 8
10		cgcd 12730	. . . . . . . 8
11	7, 9, 10	co 6085	. . . . . . 7
12		c1 8180	. . . . . . 7
13	11, 12	wceq 1402	. . . . . 6
14	2	cv 1401	. . . . . . 7
15		cdiv 9002	. . . . . . . 8
16	7, 9, 15	co 6085	. . . . . . 7
17	14, 16	wceq 1402	. . . . . 6
18	13, 17	wa 104	. . . . 5 $/\$
19		cz 9644	. . . . . 6
20		cn 9304	. . . . . 6
21	19, 20	cxp 4772	. . . . 5
22	18, 4, 21	crio 6037	. . . 4 $/\$
23	22, 6	cfv 5377	. . 3 $/\$
24	2, 3, 23	cmpt 4192	. 2 $/\$
25	1, 24	wceq 1402	1 numer $/\$

Colors of variables: wff set class

This definition is used by: qnumval 12963 fnum 12968

W3C validator