This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qeqnumdivden

Description: Recover a rational number from its canonical representation. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion qeqnumdivden ( 𝐴 ∈ ℚ → 𝐴 = ( ( numer ‘ 𝐴 ) / ( denom ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 eqidd ⊢ ( 𝐴 ∈ ℚ → ( numer ‘ 𝐴 ) = ( numer ‘ 𝐴 ) )
2 eqid ⊢ ( denom ‘ 𝐴 ) = ( denom ‘ 𝐴 )
3 1 2 jctir ⊢ ( 𝐴 ∈ ℚ → ( ( numer ‘ 𝐴 ) = ( numer ‘ 𝐴 ) ∧ ( denom ‘ 𝐴 ) = ( denom ‘ 𝐴 ) ) )
4 qnumcl ⊢ ( 𝐴 ∈ ℚ → ( numer ‘ 𝐴 ) ∈ ℤ )
5 qdencl ⊢ ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) ∈ ℕ )
6 qnumdenbi ⊢ ( ( 𝐴 ∈ ℚ ∧ ( numer ‘ 𝐴 ) ∈ ℤ ∧ ( denom ‘ 𝐴 ) ∈ ℕ ) → ( ( ( ( numer ‘ 𝐴 ) gcd ( denom ‘ 𝐴 ) ) = 1 ∧ 𝐴 = ( ( numer ‘ 𝐴 ) / ( denom ‘ 𝐴 ) ) ) ↔ ( ( numer ‘ 𝐴 ) = ( numer ‘ 𝐴 ) ∧ ( denom ‘ 𝐴 ) = ( denom ‘ 𝐴 ) ) ) )
7 4 5 6 mpd3an23 ⊢ ( 𝐴 ∈ ℚ → ( ( ( ( numer ‘ 𝐴 ) gcd ( denom ‘ 𝐴 ) ) = 1 ∧ 𝐴 = ( ( numer ‘ 𝐴 ) / ( denom ‘ 𝐴 ) ) ) ↔ ( ( numer ‘ 𝐴 ) = ( numer ‘ 𝐴 ) ∧ ( denom ‘ 𝐴 ) = ( denom ‘ 𝐴 ) ) ) )
8 3 7 mpbird ⊢ ( 𝐴 ∈ ℚ → ( ( ( numer ‘ 𝐴 ) gcd ( denom ‘ 𝐴 ) ) = 1 ∧ 𝐴 = ( ( numer ‘ 𝐴 ) / ( denom ‘ 𝐴 ) ) ) )
9 8 simprd ⊢ ( 𝐴 ∈ ℚ → 𝐴 = ( ( numer ‘ 𝐴 ) / ( denom ‘ 𝐴 ) ) )