fden

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

		Ref	Expression
	Assertion	fden	⊢ denom : ℚ ⟶ ℕ

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

Metamath Proof Explorer