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 ⊢ φ → A ∈ ℝ
modnegd.2 ⊢ φ → B ∈ ℝ
modnegd.3 ⊢ φ → C ∈ ℝ +
modnegd.4 ⊢ φ → A mod C = B mod C
Assertion modnegd ⊢ φ → − A mod C = − B mod C

Proof

Step Hyp Ref Expression
1 modnegd.1 ⊢ φ → A ∈ ℝ
2 modnegd.2 ⊢ φ → B ∈ ℝ
3 modnegd.3 ⊢ φ → C ∈ ℝ +
4 modnegd.4 ⊢ φ → A mod C = B mod C
5 1zzd ⊢ φ → 1 ∈ ℤ
6 5 znegcld ⊢ φ → − 1 ∈ ℤ
7 modmul1 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ − 1 ∈ ℤ ∧ C ∈ ℝ + ∧ A mod C = B mod C → A ⁢ -1 mod C = B ⁢ -1 mod C
8 1 2 6 3 4 7 syl221anc ⊢ φ → A ⁢ -1 mod C = B ⁢ -1 mod C
9 1 recnd ⊢ φ → A ∈ ℂ
10 1cnd ⊢ φ → 1 ∈ ℂ
11 10 negcld ⊢ φ → − 1 ∈ ℂ
12 9 11 mulcomd ⊢ φ → A ⁢ -1 = -1 ⁢ A
13 9 mulm1d ⊢ φ → -1 ⁢ A = − A
14 12 13 eqtrd ⊢ φ → A ⁢ -1 = − A
15 14 oveq1d ⊢ φ → A ⁢ -1 mod C = − A mod C
16 2 recnd ⊢ φ → B ∈ ℂ
17 16 11 mulcomd ⊢ φ → B ⁢ -1 = -1 ⁢ B
18 16 mulm1d ⊢ φ → -1 ⁢ B = − B
19 17 18 eqtrd ⊢ φ → B ⁢ -1 = − B
20 19 oveq1d ⊢ φ → B ⁢ -1 mod C = − B mod C
21 8 15 20 3eqtr3d ⊢ φ → − A mod C = − B mod C