Theorem fnum

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

	Ref	Expression
Assertion	fnum	|- numer : QQ --> ZZ

Proof

Step	Hyp	Ref	Expression
1		df-numer	|- numer = ( a e. QQ |-> ( 1st ` ( iota_ b e. ( ZZ X. NN ) ( ( ( 1st ` b ) gcd ( 2nd ` b ) ) = 1 /\ a = ( ( 1st ` b ) / ( 2nd ` b ) ) ) ) ) )
2		qnumval	|- ( a e. QQ -> ( numer ` a ) = ( 1st ` ( iota_ b e. ( ZZ X. NN ) ( ( ( 1st ` b ) gcd ( 2nd ` b ) ) = 1 /\ a = ( ( 1st ` b ) / ( 2nd ` b ) ) ) ) ) )
3		qnumcl	|- ( a e. QQ -> ( numer ` a ) e. ZZ )
4	2 3	eqeltrrd	|- ( a e. QQ -> ( 1st ` ( iota_ b e. ( ZZ X. NN ) ( ( ( 1st ` b ) gcd ( 2nd ` b ) ) = 1 /\ a = ( ( 1st ` b ) / ( 2nd ` b ) ) ) ) ) e. ZZ )
5	1 4	fmpti	|- numer : QQ --> ZZ