Theorem fden

Description: Canonical denominator defines a function. (Contributed by Stefan O'Rear, 13-Sep-2014)

	Ref	Expression
Assertion	fden	$$⊢\mathrm{denom}:\mathbb{Q}⟶\mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		df-denom	$$⊢\mathrm{denom}=\left(a\in \mathbb{Q}⟼2^{nd}\left(\left(\iota b\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(b\right)\gcd 2^{nd}\left(b\right)=1\wedge a=\frac{1^{st}\left(b\right)}{2^{nd}\left(b\right)}\right)\right)\right)\right)$$
2		qdenval	$$⊢a\in \mathbb{Q}\to \mathrm{denom}\left(a\right)=2^{nd}\left(\left(\iota b\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(b\right)\gcd 2^{nd}\left(b\right)=1\wedge a=\frac{1^{st}\left(b\right)}{2^{nd}\left(b\right)}\right)\right)\right)$$
3		qdencl	$$⊢a\in \mathbb{Q}\to \mathrm{denom}\left(a\right)\in \mathbb{N}$$
4	2 3	eqeltrrd	$$⊢a\in \mathbb{Q}\to 2^{nd}\left(\left(\iota b\in \left(\mathbb{Z}\times \mathbb{N}\right)|\left(1^{st}\left(b\right)\gcd 2^{nd}\left(b\right)=1\wedge a=\frac{1^{st}\left(b\right)}{2^{nd}\left(b\right)}\right)\right)\right)\in \mathbb{N}$$
5	1 4	fmpti	$$⊢\mathrm{denom}:\mathbb{Q}⟶\mathbb{N}$$