Theorem modsub12d

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

	Ref	Expression
Hypotheses	modadd12d.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	modadd12d.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	modadd12d.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	modadd12d.4	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
	modadd12d.5	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
	modadd12d.6	⊢ ( 𝜑 → ( 𝐴 mod 𝐸 ) = ( 𝐵 mod 𝐸 ) )
	modadd12d.7	⊢ ( 𝜑 → ( 𝐶 mod 𝐸 ) = ( 𝐷 mod 𝐸 ) )
Assertion	modsub12d	⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) mod 𝐸 ) = ( ( 𝐵 − 𝐷 ) mod 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		modadd12d.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		modadd12d.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		modadd12d.3	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		modadd12d.4	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
5		modadd12d.5	⊢ ( 𝜑 → 𝐸 ∈ ℝ+ )
6		modadd12d.6	⊢ ( 𝜑 → ( 𝐴 mod 𝐸 ) = ( 𝐵 mod 𝐸 ) )
7		modadd12d.7	⊢ ( 𝜑 → ( 𝐶 mod 𝐸 ) = ( 𝐷 mod 𝐸 ) )
8	3	renegcld	⊢ ( 𝜑 → - 𝐶 ∈ ℝ )
9	4	renegcld	⊢ ( 𝜑 → - 𝐷 ∈ ℝ )
10	3 4 5 7	modnegd	⊢ ( 𝜑 → ( - 𝐶 mod 𝐸 ) = ( - 𝐷 mod 𝐸 ) )
11	1 2 8 9 5 6 10	modadd12d	⊢ ( 𝜑 → ( ( 𝐴 + - 𝐶 ) mod 𝐸 ) = ( ( 𝐵 + - 𝐷 ) mod 𝐸 ) )
12	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
13	3	recnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
14	12 13	negsubd	⊢ ( 𝜑 → ( 𝐴 + - 𝐶 ) = ( 𝐴 − 𝐶 ) )
15	14	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 + - 𝐶 ) mod 𝐸 ) = ( ( 𝐴 − 𝐶 ) mod 𝐸 ) )
16	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
17	4	recnd	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
18	16 17	negsubd	⊢ ( 𝜑 → ( 𝐵 + - 𝐷 ) = ( 𝐵 − 𝐷 ) )
19	18	oveq1d	⊢ ( 𝜑 → ( ( 𝐵 + - 𝐷 ) mod 𝐸 ) = ( ( 𝐵 − 𝐷 ) mod 𝐸 ) )
20	11 15 19	3eqtr3d	⊢ ( 𝜑 → ( ( 𝐴 − 𝐶 ) mod 𝐸 ) = ( ( 𝐵 − 𝐷 ) mod 𝐸 ) )