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 ( 𝐴 ∈ ℚ → - 𝐴 ∈ ℚ )

Proof

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