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 \in ℚ \to - A \in ℚ$

Step	Hyp	Ref	Expression
1		elq	$⊢ A \in ℚ \leftrightarrow \exists x \in ℤ \exists y \in ℕ A = \frac{x}{y}$
2		zcn	$⊢ x \in ℤ \to x \in ℂ$
3	2	adantr	$⊢ (x \in ℤ \land y \in ℕ) \to x \in ℂ$
4		nncn	$⊢ y \in ℕ \to y \in ℂ$
5	4	adantl	$⊢ (x \in ℤ \land y \in ℕ) \to y \in ℂ$
6		nnne0	$⊢ y \in ℕ \to y \neq 0$
7	6	adantl	$⊢ (x \in ℤ \land y \in ℕ) \to y \neq 0$
8	3 5 7	divnegd	$⊢ (x \in ℤ \land y \in ℕ) \to - \frac{x}{y} = \frac{- x}{y}$
9		znegcl	$⊢ x \in ℤ \to - x \in ℤ$
10		znq	$⊢ (- x \in ℤ \land y \in ℕ) \to \frac{- x}{y} \in ℚ$
11	9 10	sylan	$⊢ (x \in ℤ \land y \in ℕ) \to \frac{- x}{y} \in ℚ$
12	8 11	eqeltrd	$⊢ (x \in ℤ \land y \in ℕ) \to - \frac{x}{y} \in ℚ$
13		negeq	$⊢ A = \frac{x}{y} \to - A = - \frac{x}{y}$
14	13	eleq1d	$⊢ A = \frac{x}{y} \to (- A \in ℚ \leftrightarrow - \frac{x}{y} \in ℚ)$
15	12 14	syl5ibrcom	$⊢ (x \in ℤ \land y \in ℕ) \to (A = \frac{x}{y} \to - A \in ℚ)$
16	15	rexlimivv	$⊢ \exists x \in ℤ \exists y \in ℕ A = \frac{x}{y} \to - A \in ℚ$
17	1 16	sylbi	$⊢ A \in ℚ \to - A \in ℚ$

Metamath Proof Explorer