Metamath Proof Explorer


Theorem qnumval

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

Ref Expression
Assertion qnumval ( 𝐴 ∈ ℚ → ( numer ‘ 𝐴 ) = ( 1st ‘ ( 𝑥 ∈ ( ℤ × ℕ ) ( ( ( 1st𝑥 ) gcd ( 2nd𝑥 ) ) = 1 ∧ 𝐴 = ( ( 1st𝑥 ) / ( 2nd𝑥 ) ) ) ) ) )

Proof

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