Metamath Proof Explorer

Theorem qnegcl

Description: Closure law for the negative of a rational. (Contributed by NM, 2-Aug-2004) (Revised by Mario Carneiro, 15-Sep-2014)

Ref Expression
Assertion qnegcl ⊢ A ∈ ℚ → − A ∈ ℚ

Proof

Step Hyp Ref Expression
1 elq ⊢ A ∈ ℚ ↔ ∃ x ∈ ℤ ∃ y ∈ ℕ A = x y
2 zcn ⊢ x ∈ ℤ → x ∈ ℂ
3 2 adantr ⊢ x ∈ ℤ ∧ y ∈ ℕ → x ∈ ℂ
4 nncn ⊢ y ∈ ℕ → y ∈ ℂ
5 4 adantl ⊢ x ∈ ℤ ∧ y ∈ ℕ → y ∈ ℂ
6 nnne0 ⊢ y ∈ ℕ → y ≠ 0
7 6 adantl ⊢ x ∈ ℤ ∧ y ∈ ℕ → y ≠ 0
8 3 5 7 divnegd ⊢ x ∈ ℤ ∧ y ∈ ℕ → − x y = − x y
9 znegcl ⊢ x ∈ ℤ → − x ∈ ℤ
10 znq ⊢ − x ∈ ℤ ∧ y ∈ ℕ → − x y ∈ ℚ
11 9 10 sylan ⊢ x ∈ ℤ ∧ y ∈ ℕ → − x y ∈ ℚ
12 8 11 eqeltrd ⊢ x ∈ ℤ ∧ y ∈ ℕ → − x y ∈ ℚ
13 negeq ⊢ A = x y → − A = − x y
14 13 eleq1d ⊢ A = x y → − A ∈ ℚ ↔ − x y ∈ ℚ
15 12 14 syl5ibrcom ⊢ x ∈ ℤ ∧ y ∈ ℕ → A = x y → − A ∈ ℚ
16 15 rexlimivv ⊢ ∃ x ∈ ℤ ∃ y ∈ ℕ A = x y → − A ∈ ℚ
17 1 16 sylbi ⊢ A ∈ ℚ → − A ∈ ℚ