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