This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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