Theorem modnegd

Description: Negation property of the modulo operation. (Contributed by Mario Carneiro, 9-Sep-2016)

	Ref	Expression
Hypotheses	modnegd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	modnegd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	modnegd.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
	modnegd.4	⊢ ( 𝜑 → ( 𝐴 mod 𝐶 ) = ( 𝐵 mod 𝐶 ) )
Assertion	modnegd	⊢ ( 𝜑 → ( - 𝐴 mod 𝐶 ) = ( - 𝐵 mod 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		modnegd.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		modnegd.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		modnegd.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
4		modnegd.4	⊢ ( 𝜑 → ( 𝐴 mod 𝐶 ) = ( 𝐵 mod 𝐶 ) )
5		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
6	5	znegcld	⊢ ( 𝜑 → - 1 ∈ ℤ )
7		modmul1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( - 1 ∈ ℤ ∧ 𝐶 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝐶 ) = ( 𝐵 mod 𝐶 ) ) → ( ( 𝐴 · - 1 ) mod 𝐶 ) = ( ( 𝐵 · - 1 ) mod 𝐶 ) )
8	1 2 6 3 4 7	syl221anc	⊢ ( 𝜑 → ( ( 𝐴 · - 1 ) mod 𝐶 ) = ( ( 𝐵 · - 1 ) mod 𝐶 ) )
9	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
10		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
11	10	negcld	⊢ ( 𝜑 → - 1 ∈ ℂ )
12	9 11	mulcomd	⊢ ( 𝜑 → ( 𝐴 · - 1 ) = ( - 1 · 𝐴 ) )
13	9	mulm1d	⊢ ( 𝜑 → ( - 1 · 𝐴 ) = - 𝐴 )
14	12 13	eqtrd	⊢ ( 𝜑 → ( 𝐴 · - 1 ) = - 𝐴 )
15	14	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 · - 1 ) mod 𝐶 ) = ( - 𝐴 mod 𝐶 ) )
16	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
17	16 11	mulcomd	⊢ ( 𝜑 → ( 𝐵 · - 1 ) = ( - 1 · 𝐵 ) )
18	16	mulm1d	⊢ ( 𝜑 → ( - 1 · 𝐵 ) = - 𝐵 )
19	17 18	eqtrd	⊢ ( 𝜑 → ( 𝐵 · - 1 ) = - 𝐵 )
20	19	oveq1d	⊢ ( 𝜑 → ( ( 𝐵 · - 1 ) mod 𝐶 ) = ( - 𝐵 mod 𝐶 ) )
21	8 15 20	3eqtr3d	⊢ ( 𝜑 → ( - 𝐴 mod 𝐶 ) = ( - 𝐵 mod 𝐶 ) )