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 ⁡ Q gcd denom ⁡ Q = numer ⁡ Q gcd denom ⁡ Q
7 2 5 6 syl2anc ⊢ Q ∈ ℚ → − numer ⁡ Q gcd denom ⁡ Q = numer ⁡ Q gcd denom ⁡ Q
8 qnumdencoprm ⊢ Q ∈ ℚ → numer ⁡ Q gcd denom ⁡ Q = 1
9 7 8 eqtrd ⊢ Q ∈ ℚ → − numer ⁡ Q gcd denom ⁡ Q = 1
10 qeqnumdivden ⊢ Q ∈ ℚ → Q = numer ⁡ Q denom ⁡ Q
11 10 negeqd ⊢ Q ∈ ℚ → − Q = − numer ⁡ Q denom ⁡ 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 ⁡ Q denom ⁡ Q = − numer ⁡ Q denom ⁡ Q
16 11 15 eqtrd ⊢ Q ∈ ℚ → − Q = − numer ⁡ Q denom ⁡ Q
17 qnumdenbi ⊢ − Q ∈ ℚ ∧ − numer ⁡ Q ∈ ℤ ∧ denom ⁡ Q ∈ ℕ → − numer ⁡ Q gcd denom ⁡ Q = 1 ∧ − Q = − numer ⁡ Q denom ⁡ Q ↔ numer ⁡ − Q = − numer ⁡ Q ∧ denom ⁡ − Q = denom ⁡ Q
18 17 biimpa ⊢ − Q ∈ ℚ ∧ − numer ⁡ Q ∈ ℤ ∧ denom ⁡ Q ∈ ℕ ∧ − numer ⁡ Q gcd denom ⁡ Q = 1 ∧ − Q = − numer ⁡ Q denom ⁡ 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