Definition df-numer

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)

	Ref	Expression
Assertion	df-numer	$$⊢\mathrm{numer}=\left(y\in \mathbb{Q}⟼1^{st}\left(\left(\iota x\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(x\right)\gcd 2^{nd}\left(x\right)=1\wedge y=\frac{1^{st}\left(x\right)}{2^{nd}\left(x\right)}\right)\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnumer	$$class\mathrm{numer}$$
1		vy	$$setvary$$
2		cq	$$class\mathbb{Q}$$
3		c1st	$$class{1}^{st}$$
4		vx	$$setvarx$$
5		cz	$$class\mathbb{Z}$$
6		cn	$$class\mathbb{N}$$
7	5 6	cxp	$$class\left(\mathbb{Z}\times \mathbb{N}\right)$$
8	4	cv	$$setvarx$$
9	8 3	cfv	$$class{1}^{st}\left(x\right)$$
10		cgcd	$$class\gcd$$
11		c2nd	$$class{2}^{nd}$$
12	8 11	cfv	$$class{2}^{nd}\left(x\right)$$
13	9 12 10	co	$$class\left(1^{st}\left(x\right)\gcd 2^{nd}\left(x\right)\right)$$
14		c1	$$class1$$
15	13 14	wceq	$$wff{1}^{st}\left(x\right)\gcd 2^{nd}\left(x\right)=1$$
16	1	cv	$$setvary$$
17		cdiv	$$class÷$$
18	9 12 17	co	$$class\left(\frac{1^{st}\left(x\right)}{2^{nd}\left(x\right)}\right)$$
19	16 18	wceq	$$wffy=\frac{1^{st}\left(x\right)}{2^{nd}\left(x\right)}$$
20	15 19	wa	$$wff\left(1^{st}\left(x\right)\gcd 2^{nd}\left(x\right)=1\wedge y=\frac{1^{st}\left(x\right)}{2^{nd}\left(x\right)}\right)$$
21	20 4 7	crio	$$class\left(\iota x\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(x\right)\gcd 2^{nd}\left(x\right)=1\wedge y=\frac{1^{st}\left(x\right)}{2^{nd}\left(x\right)}\right)\right)$$
22	21 3	cfv	$$class{1}^{st}\left(\left(\iota x\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(x\right)\gcd 2^{nd}\left(x\right)=1\wedge y=\frac{1^{st}\left(x\right)}{2^{nd}\left(x\right)}\right)\right)\right)$$
23	1 2 22	cmpt	$$class\left(y\in \mathbb{Q}⟼1^{st}\left(\left(\iota x\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(x\right)\gcd 2^{nd}\left(x\right)=1\wedge y=\frac{1^{st}\left(x\right)}{2^{nd}\left(x\right)}\right)\right)\right)\right)$$
24	0 23	wceq	$$wff\mathrm{numer}=\left(y\in \mathbb{Q}⟼1^{st}\left(\left(\iota x\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(x\right)\gcd 2^{nd}\left(x\right)=1\wedge y=\frac{1^{st}\left(x\right)}{2^{nd}\left(x\right)}\right)\right)\right)\right)$$