fnum

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

		Ref	Expression
	Assertion	fnum	⊢ numer : ℚ ⟶ ℤ

Step	Hyp	Ref	Expression
1		df-numer	⊢ numer = ( 𝑎 ∈ ℚ ↦ ( 1^st ‘ ( ℩ 𝑏 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑏 ) gcd ( 2^nd ‘ 𝑏 ) ) = 1 ∧ 𝑎 = ( ( 1^st ‘ 𝑏 ) / ( 2^nd ‘ 𝑏 ) ) ) ) ) )
2		qnumval	⊢ ( 𝑎 ∈ ℚ → ( numer ‘ 𝑎 ) = ( 1^st ‘ ( ℩ 𝑏 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑏 ) gcd ( 2^nd ‘ 𝑏 ) ) = 1 ∧ 𝑎 = ( ( 1^st ‘ 𝑏 ) / ( 2^nd ‘ 𝑏 ) ) ) ) ) )
3		qnumcl	⊢ ( 𝑎 ∈ ℚ → ( numer ‘ 𝑎 ) ∈ ℤ )
4	2 3	eqeltrrd	⊢ ( 𝑎 ∈ ℚ → ( 1^st ‘ ( ℩ 𝑏 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑏 ) gcd ( 2^nd ‘ 𝑏 ) ) = 1 ∧ 𝑎 = ( ( 1^st ‘ 𝑏 ) / ( 2^nd ‘ 𝑏 ) ) ) ) ) ∈ ℤ )
5	1 4	fmpti	⊢ numer : ℚ ⟶ ℤ

Metamath Proof Explorer