Metamath Proof Explorer


Theorem modsub12d

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

Ref Expression
Hypotheses modadd12d.1 φA
modadd12d.2 φB
modadd12d.3 φC
modadd12d.4 φD
modadd12d.5 φE+
modadd12d.6 φAmodE=BmodE
modadd12d.7 φCmodE=DmodE
Assertion modsub12d φACmodE=BDmodE

Proof

Step Hyp Ref Expression
1 modadd12d.1 φA
2 modadd12d.2 φB
3 modadd12d.3 φC
4 modadd12d.4 φD
5 modadd12d.5 φE+
6 modadd12d.6 φAmodE=BmodE
7 modadd12d.7 φCmodE=DmodE
8 3 renegcld φC
9 4 renegcld φD
10 3 4 5 7 modnegd φCmodE=DmodE
11 1 2 8 9 5 6 10 modadd12d φA+CmodE=B+DmodE
12 1 recnd φA
13 3 recnd φC
14 12 13 negsubd φA+C=AC
15 14 oveq1d φA+CmodE=ACmodE
16 2 recnd φB
17 4 recnd φD
18 16 17 negsubd φB+D=BD
19 18 oveq1d φB+DmodE=BDmodE
20 11 15 19 3eqtr3d φACmodE=BDmodE