This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐶 ) )