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 e. QQ -> ( ( numer ` A ) gcd ( denom ` A ) ) = 1 )

Proof

Step Hyp Ref Expression
1 eqidd 
 |-  ( A e. QQ -> ( numer ` A ) = ( numer ` A ) )
2 eqid 
 |-  ( denom ` A ) = ( denom ` A )
3 1 2 jctir 
 |-  ( A e. QQ -> ( ( numer ` A ) = ( numer ` A ) /\ ( denom ` A ) = ( denom ` A ) ) )
4 qnumcl 
 |-  ( A e. QQ -> ( numer ` A ) e. ZZ )
5 qdencl 
 |-  ( A e. QQ -> ( denom ` A ) e. NN )
6 qnumdenbi 
 |-  ( ( A e. QQ /\ ( numer ` A ) e. ZZ /\ ( denom ` A ) e. NN ) -> ( ( ( ( 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 e. QQ -> ( ( ( ( numer ` A ) gcd ( denom ` A ) ) = 1 /\ A = ( ( numer ` A ) / ( denom ` A ) ) ) <-> ( ( numer ` A ) = ( numer ` A ) /\ ( denom ` A ) = ( denom ` A ) ) ) )
8 3 7 mpbird 
 |-  ( A e. QQ -> ( ( ( numer ` A ) gcd ( denom ` A ) ) = 1 /\ A = ( ( numer ` A ) / ( denom ` A ) ) ) )
9 8 simpld 
 |-  ( A e. QQ -> ( ( numer ` A ) gcd ( denom ` A ) ) = 1 )