Metamath Proof Explorer


Theorem qnumdencoprm

Description: The canonical representation of a rational is fully reduced. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion qnumdencoprm A numer A gcd denom A = 1

Proof

Step Hyp Ref Expression
1 eqidd A numer A = numer A
2 eqid denom A = denom A
3 1 2 jctir A numer A = numer A denom A = denom A
4 qnumcl A numer A
5 qdencl A denom A
6 qnumdenbi A numer A denom A numer A gcd denom A = 1 A = numer A denom A numer A = numer A denom A = denom A
7 4 5 6 mpd3an23 A numer A gcd denom A = 1 A = numer A denom A numer A = numer A denom A = denom A
8 3 7 mpbird A numer A gcd denom A = 1 A = numer A denom A
9 8 simpld A numer A gcd denom A = 1