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 ‘ 𝐴 ) ) )