Theorem 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	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \left(A\mathrm{mod}B=0\leftrightarrow \left(-A\right)\mathrm{mod}B=0\right)$$

Proof

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