Theorem numdenneg

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

	Ref	Expression
Assertion	numdenneg	⊢ ( 𝑄 ∈ ℚ → ( ( numer ‘ - 𝑄 ) = - ( numer ‘ 𝑄 ) ∧ ( denom ‘ - 𝑄 ) = ( denom ‘ 𝑄 ) ) )

Proof

Step	Hyp	Ref	Expression
1		qnegcl	⊢ ( 𝑄 ∈ ℚ → - 𝑄 ∈ ℚ )
2		qnumcl	⊢ ( 𝑄 ∈ ℚ → ( numer ‘ 𝑄 ) ∈ ℤ )
3	2	znegcld	⊢ ( 𝑄 ∈ ℚ → - ( numer ‘ 𝑄 ) ∈ ℤ )
4		qdencl	⊢ ( 𝑄 ∈ ℚ → ( denom ‘ 𝑄 ) ∈ ℕ )
5	4	nnzd	⊢ ( 𝑄 ∈ ℚ → ( denom ‘ 𝑄 ) ∈ ℤ )
6		neggcd	⊢ ( ( ( numer ‘ 𝑄 ) ∈ ℤ ∧ ( denom ‘ 𝑄 ) ∈ ℤ ) → ( - ( numer ‘ 𝑄 ) gcd ( denom ‘ 𝑄 ) ) = ( ( numer ‘ 𝑄 ) gcd ( denom ‘ 𝑄 ) ) )
7	2 5 6	syl2anc	⊢ ( 𝑄 ∈ ℚ → ( - ( numer ‘ 𝑄 ) gcd ( denom ‘ 𝑄 ) ) = ( ( numer ‘ 𝑄 ) gcd ( denom ‘ 𝑄 ) ) )
8		qnumdencoprm	⊢ ( 𝑄 ∈ ℚ → ( ( numer ‘ 𝑄 ) gcd ( denom ‘ 𝑄 ) ) = 1 )
9	7 8	eqtrd	⊢ ( 𝑄 ∈ ℚ → ( - ( numer ‘ 𝑄 ) gcd ( denom ‘ 𝑄 ) ) = 1 )
10		qeqnumdivden	⊢ ( 𝑄 ∈ ℚ → 𝑄 = ( ( numer ‘ 𝑄 ) / ( denom ‘ 𝑄 ) ) )
11	10	negeqd	⊢ ( 𝑄 ∈ ℚ → - 𝑄 = - ( ( numer ‘ 𝑄 ) / ( denom ‘ 𝑄 ) ) )
12	2	zcnd	⊢ ( 𝑄 ∈ ℚ → ( numer ‘ 𝑄 ) ∈ ℂ )
13	4	nncnd	⊢ ( 𝑄 ∈ ℚ → ( denom ‘ 𝑄 ) ∈ ℂ )
14	4	nnne0d	⊢ ( 𝑄 ∈ ℚ → ( denom ‘ 𝑄 ) ≠ 0 )
15	12 13 14	divnegd	⊢ ( 𝑄 ∈ ℚ → - ( ( numer ‘ 𝑄 ) / ( denom ‘ 𝑄 ) ) = ( - ( numer ‘ 𝑄 ) / ( denom ‘ 𝑄 ) ) )
16	11 15	eqtrd	⊢ ( 𝑄 ∈ ℚ → - 𝑄 = ( - ( numer ‘ 𝑄 ) / ( denom ‘ 𝑄 ) ) )
17		qnumdenbi	⊢ ( ( - 𝑄 ∈ ℚ ∧ - ( numer ‘ 𝑄 ) ∈ ℤ ∧ ( denom ‘ 𝑄 ) ∈ ℕ ) → ( ( ( - ( numer ‘ 𝑄 ) gcd ( denom ‘ 𝑄 ) ) = 1 ∧ - 𝑄 = ( - ( numer ‘ 𝑄 ) / ( denom ‘ 𝑄 ) ) ) ↔ ( ( numer ‘ - 𝑄 ) = - ( numer ‘ 𝑄 ) ∧ ( denom ‘ - 𝑄 ) = ( denom ‘ 𝑄 ) ) ) )
18	17	biimpa	⊢ ( ( ( - 𝑄 ∈ ℚ ∧ - ( numer ‘ 𝑄 ) ∈ ℤ ∧ ( denom ‘ 𝑄 ) ∈ ℕ ) ∧ ( ( - ( numer ‘ 𝑄 ) gcd ( denom ‘ 𝑄 ) ) = 1 ∧ - 𝑄 = ( - ( numer ‘ 𝑄 ) / ( denom ‘ 𝑄 ) ) ) ) → ( ( numer ‘ - 𝑄 ) = - ( numer ‘ 𝑄 ) ∧ ( denom ‘ - 𝑄 ) = ( denom ‘ 𝑄 ) ) )
19	1 3 4 9 16 18	syl32anc	⊢ ( 𝑄 ∈ ℚ → ( ( numer ‘ - 𝑄 ) = - ( numer ‘ 𝑄 ) ∧ ( denom ‘ - 𝑄 ) = ( denom ‘ 𝑄 ) ) )