# Metamath Proof Explorer

## Theorem modsub12d

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

Ref Expression
Hypotheses modadd12d.1 ${⊢}{\phi }\to {A}\in ℝ$
modadd12d.2 ${⊢}{\phi }\to {B}\in ℝ$
modadd12d.3 ${⊢}{\phi }\to {C}\in ℝ$
modadd12d.4 ${⊢}{\phi }\to {D}\in ℝ$
modadd12d.5 ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
modadd12d.6 ${⊢}{\phi }\to {A}\mathrm{mod}{E}={B}\mathrm{mod}{E}$
modadd12d.7 ${⊢}{\phi }\to {C}\mathrm{mod}{E}={D}\mathrm{mod}{E}$
Assertion modsub12d ${⊢}{\phi }\to \left({A}-{C}\right)\mathrm{mod}{E}=\left({B}-{D}\right)\mathrm{mod}{E}$

### Proof

Step Hyp Ref Expression
1 modadd12d.1 ${⊢}{\phi }\to {A}\in ℝ$
2 modadd12d.2 ${⊢}{\phi }\to {B}\in ℝ$
3 modadd12d.3 ${⊢}{\phi }\to {C}\in ℝ$
4 modadd12d.4 ${⊢}{\phi }\to {D}\in ℝ$
5 modadd12d.5 ${⊢}{\phi }\to {E}\in {ℝ}^{+}$
6 modadd12d.6 ${⊢}{\phi }\to {A}\mathrm{mod}{E}={B}\mathrm{mod}{E}$
7 modadd12d.7 ${⊢}{\phi }\to {C}\mathrm{mod}{E}={D}\mathrm{mod}{E}$
8 3 renegcld ${⊢}{\phi }\to -{C}\in ℝ$
9 4 renegcld ${⊢}{\phi }\to -{D}\in ℝ$
10 3 4 5 7 modnegd ${⊢}{\phi }\to \left(-{C}\right)\mathrm{mod}{E}=\left(-{D}\right)\mathrm{mod}{E}$
11 1 2 8 9 5 6 10 modadd12d ${⊢}{\phi }\to \left({A}+\left(-{C}\right)\right)\mathrm{mod}{E}=\left({B}+\left(-{D}\right)\right)\mathrm{mod}{E}$
12 1 recnd ${⊢}{\phi }\to {A}\in ℂ$
13 3 recnd ${⊢}{\phi }\to {C}\in ℂ$
14 12 13 negsubd ${⊢}{\phi }\to {A}+\left(-{C}\right)={A}-{C}$
15 14 oveq1d ${⊢}{\phi }\to \left({A}+\left(-{C}\right)\right)\mathrm{mod}{E}=\left({A}-{C}\right)\mathrm{mod}{E}$
16 2 recnd ${⊢}{\phi }\to {B}\in ℂ$
17 4 recnd ${⊢}{\phi }\to {D}\in ℂ$
18 16 17 negsubd ${⊢}{\phi }\to {B}+\left(-{D}\right)={B}-{D}$
19 18 oveq1d ${⊢}{\phi }\to \left({B}+\left(-{D}\right)\right)\mathrm{mod}{E}=\left({B}-{D}\right)\mathrm{mod}{E}$
20 11 15 19 3eqtr3d ${⊢}{\phi }\to \left({A}-{C}\right)\mathrm{mod}{E}=\left({B}-{D}\right)\mathrm{mod}{E}$