Metamath Proof Explorer

Theorem numdenneg

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

Ref Expression
Assertion numdenneg ⊢Q∈ℚ→numer⁡−Q=−numer⁡Q∧denom⁡−Q=denom⁡Q

Proof

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