Theorem fnum

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

	Ref	Expression
Assertion	fnum	$$⊢\mathrm{numer}:\mathbb{Q}⟶\mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		df-numer	$$⊢\mathrm{numer}=\left(a\in \mathbb{Q}⟼1^{st}\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		qnumval	$$⊢a\in \mathbb{Q}\to \mathrm{numer}\left(a\right)=1^{st}\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		qnumcl	$$⊢a\in \mathbb{Q}\to \mathrm{numer}\left(a\right)\in \mathbb{Z}$$
4	2 3	eqeltrrd	$$⊢a\in \mathbb{Q}\to 1^{st}\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{Z}$$
5	1 4	fmpti	$$⊢\mathrm{numer}:\mathbb{Q}⟶\mathbb{Z}$$