Definition df-denom

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)

	Ref	Expression
Assertion	df-denom	$$⊢\mathrm{denom}=\left(y\in \mathbb{Q}⟼2^{nd}\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		cdenom	$$class\mathrm{denom}$$
1		vy	$$setvary$$
2		cq	$$class\mathbb{Q}$$
3		c2nd	$$class{2}^{nd}$$
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		c1st	$$class{1}^{st}$$
9	4	cv	$$setvarx$$
10	9 8	cfv	$$class{1}^{st}\left(x\right)$$
11		cgcd	$$class\gcd$$
12	9 3	cfv	$$class{2}^{nd}\left(x\right)$$
13	10 12 11	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	10 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{2}^{nd}\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}⟼2^{nd}\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{denom}=\left(y\in \mathbb{Q}⟼2^{nd}\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)$$