Metamath Proof Explorer

Theorem numdenneg

Description: Numerator and denominator of the negative. (Contributed by Thierry Arnoux, 27-Oct-2017)

Ref Expression
Assertion numdenneg 
|- ( Q e. QQ -> ( ( numer ` -u Q ) = -u ( numer ` Q ) /\ ( denom ` -u Q ) = ( denom ` Q ) ) )

Proof

Step Hyp Ref Expression
1 qnegcl 
 |-  ( Q e. QQ -> -u Q e. QQ )
2 qnumcl 
 |-  ( Q e. QQ -> ( numer ` Q ) e. ZZ )
3 2 znegcld 
 |-  ( Q e. QQ -> -u ( numer ` Q ) e. ZZ )
4 qdencl 
 |-  ( Q e. QQ -> ( denom ` Q ) e. NN )
5 4 nnzd 
 |-  ( Q e. QQ -> ( denom ` Q ) e. ZZ )
6 neggcd 
 |-  ( ( ( numer ` Q ) e. ZZ /\ ( denom ` Q ) e. ZZ ) -> ( -u ( numer ` Q ) gcd ( denom ` Q ) ) = ( ( numer ` Q ) gcd ( denom ` Q ) ) )
7 2 5 6 syl2anc 
 |-  ( Q e. QQ -> ( -u ( numer ` Q ) gcd ( denom ` Q ) ) = ( ( numer ` Q ) gcd ( denom ` Q ) ) )
8 qnumdencoprm 
 |-  ( Q e. QQ -> ( ( numer ` Q ) gcd ( denom ` Q ) ) = 1 )
9 7 8 eqtrd 
 |-  ( Q e. QQ -> ( -u ( numer ` Q ) gcd ( denom ` Q ) ) = 1 )
10 qeqnumdivden 
 |-  ( Q e. QQ -> Q = ( ( numer ` Q ) / ( denom ` Q ) ) )
11 10 negeqd 
 |-  ( Q e. QQ -> -u Q = -u ( ( numer ` Q ) / ( denom ` Q ) ) )
12 2 zcnd 
 |-  ( Q e. QQ -> ( numer ` Q ) e. CC )
13 4 nncnd 
 |-  ( Q e. QQ -> ( denom ` Q ) e. CC )
14 4 nnne0d 
 |-  ( Q e. QQ -> ( denom ` Q ) =/= 0 )
15 12 13 14 divnegd 
 |-  ( Q e. QQ -> -u ( ( numer ` Q ) / ( denom ` Q ) ) = ( -u ( numer ` Q ) / ( denom ` Q ) ) )
16 11 15 eqtrd 
 |-  ( Q e. QQ -> -u Q = ( -u ( numer ` Q ) / ( denom ` Q ) ) )
17 qnumdenbi 
 |-  ( ( -u Q e. QQ /\ -u ( numer ` Q ) e. ZZ /\ ( denom ` Q ) e. NN ) -> ( ( ( -u ( numer ` Q ) gcd ( denom ` Q ) ) = 1 /\ -u Q = ( -u ( numer ` Q ) / ( denom ` Q ) ) ) <-> ( ( numer ` -u Q ) = -u ( numer ` Q ) /\ ( denom ` -u Q ) = ( denom ` Q ) ) ) )
18 17 biimpa 
 |-  ( ( ( -u Q e. QQ /\ -u ( numer ` Q ) e. ZZ /\ ( denom ` Q ) e. NN ) /\ ( ( -u ( numer ` Q ) gcd ( denom ` Q ) ) = 1 /\ -u Q = ( -u ( numer ` Q ) / ( denom ` Q ) ) ) ) -> ( ( numer ` -u Q ) = -u ( numer ` Q ) /\ ( denom ` -u Q ) = ( denom ` Q ) ) )
19 1 3 4 9 16 18 syl32anc 
 |-  ( Q e. QQ -> ( ( numer ` -u Q ) = -u ( numer ` Q ) /\ ( denom ` -u Q ) = ( denom ` Q ) ) )