negmod0

Description: A is divisible by B iff its negative is. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Fan Zheng, 7-Jun-2016)

		Ref	Expression
	Assertion	negmod0	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (A \mod B = 0 \leftrightarrow (- A) \mod B = 0)$

Step	Hyp	Ref	Expression
1		rerpdivcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{A}{B} \in ℝ$
2		recn	$⊢ \frac{A}{B} \in ℝ \to \frac{A}{B} \in ℂ$
3		znegclb	$⊢ \frac{A}{B} \in ℂ \to (\frac{A}{B} \in ℤ \leftrightarrow - \frac{A}{B} \in ℤ)$
4	1 2 3	3syl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (\frac{A}{B} \in ℤ \leftrightarrow - \frac{A}{B} \in ℤ)$
5		recn	$⊢ A \in ℝ \to A \in ℂ$
6	5	adantr	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \in ℂ$
7		rpcn	$⊢ B \in ℝ^{+} \to B \in ℂ$
8	7	adantl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B \in ℂ$
9		rpne0	$⊢ B \in ℝ^{+} \to B \neq 0$
10	9	adantl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B \neq 0$
11	6 8 10	divnegd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to - \frac{A}{B} = \frac{- A}{B}$
12	11	eleq1d	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (- \frac{A}{B} \in ℤ \leftrightarrow \frac{- A}{B} \in ℤ)$
13	4 12	bitrd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (\frac{A}{B} \in ℤ \leftrightarrow \frac{- A}{B} \in ℤ)$
14		mod0	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (A \mod B = 0 \leftrightarrow \frac{A}{B} \in ℤ)$
15		renegcl	$⊢ A \in ℝ \to - A \in ℝ$
16		mod0	$⊢ (- A \in ℝ \land B \in ℝ^{+}) \to ((- A) \mod B = 0 \leftrightarrow \frac{- A}{B} \in ℤ)$
17	15 16	sylan	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ((- A) \mod B = 0 \leftrightarrow \frac{- A}{B} \in ℤ)$
18	13 14 17	3bitr4d	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (A \mod B = 0 \leftrightarrow (- A) \mod B = 0)$

Metamath Proof Explorer