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	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( - 𝐴 mod 𝐵 ) = 0 ) )

Proof

Step	Hyp	Ref	Expression
1		rerpdivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
2		recn	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℝ → ( 𝐴 / 𝐵 ) ∈ ℂ )
3		znegclb	⊢ ( ( 𝐴 / 𝐵 ) ∈ ℂ → ( ( 𝐴 / 𝐵 ) ∈ ℤ ↔ - ( 𝐴 / 𝐵 ) ∈ ℤ ) )
4	1 2 3	3syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 / 𝐵 ) ∈ ℤ ↔ - ( 𝐴 / 𝐵 ) ∈ ℤ ) )
5		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
6	5	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
7		rpcn	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ∈ ℂ )
8	7	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
9		rpne0	⊢ ( 𝐵 ∈ ℝ+ → 𝐵 ≠ 0 )
10	9	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → 𝐵 ≠ 0 )
11	6 8 10	divnegd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → - ( 𝐴 / 𝐵 ) = ( - 𝐴 / 𝐵 ) )
12	11	eleq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( - ( 𝐴 / 𝐵 ) ∈ ℤ ↔ ( - 𝐴 / 𝐵 ) ∈ ℤ ) )
13	4 12	bitrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 / 𝐵 ) ∈ ℤ ↔ ( - 𝐴 / 𝐵 ) ∈ ℤ ) )
14		mod0	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( 𝐴 / 𝐵 ) ∈ ℤ ) )
15		renegcl	⊢ ( 𝐴 ∈ ℝ → - 𝐴 ∈ ℝ )
16		mod0	⊢ ( ( - 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( - 𝐴 mod 𝐵 ) = 0 ↔ ( - 𝐴 / 𝐵 ) ∈ ℤ ) )
17	15 16	sylan	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( - 𝐴 mod 𝐵 ) = 0 ↔ ( - 𝐴 / 𝐵 ) ∈ ℤ ) )
18	13 14 17	3bitr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐵 ) = 0 ↔ ( - 𝐴 mod 𝐵 ) = 0 ) )