Metamath Proof Explorer

Theorem qdenval

Description: Value of the canonical denominator function. (Contributed by Stefan O'Rear, 13-Sep-2014)

		Ref	Expression
	Assertion	qdenval	⊢ ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) = ( 2^nd ‘ ( ℩ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqeq1	⊢ ( 𝑎 = 𝐴 → ( 𝑎 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ↔ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) )
2	1	anbi2d	⊢ ( 𝑎 = 𝐴 → ( ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝑎 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ↔ ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ) )
3	2	riotabidv	⊢ ( 𝑎 = 𝐴 → ( ℩ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝑎 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ) = ( ℩ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ) )
4	3	fveq2d	⊢ ( 𝑎 = 𝐴 → ( 2^nd ‘ ( ℩ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝑎 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ) ) = ( 2^nd ‘ ( ℩ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ) ) )
5		df-denom	⊢ denom = ( 𝑎 ∈ ℚ ↦ ( 2^nd ‘ ( ℩ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝑎 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ) ) )
6		fvex	⊢ ( 2^nd ‘ ( ℩ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ) ) ∈ V
7	4 5 6	fvmpt	⊢ ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) = ( 2^nd ‘ ( ℩ 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑥 ) gcd ( 2^nd ‘ 𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑥 ) / ( 2^nd ‘ 𝑥 ) ) ) ) ) )