Theorem modsubmodmod

Description: The difference of a real number modulo a positive real number and another real number modulo this positive real number equals the difference of the two real numbers modulo the positive real number. (Contributed by Alexander van der Vekens, 17-May-2018)

	Ref	Expression
Assertion	modsubmodmod	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝑀 ) − ( 𝐵 mod 𝑀 ) ) mod 𝑀 ) = ( ( 𝐴 − 𝐵 ) mod 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		modcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ∈ ℝ )
2	1	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ∈ ℝ )
3		simp1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
4		modcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐵 mod 𝑀 ) ∈ ℝ )
5	4	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐵 mod 𝑀 ) ∈ ℝ )
6		simp2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
7		simp3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 𝑀 ∈ ℝ+ )
8		modabs2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) mod 𝑀 ) = ( 𝐴 mod 𝑀 ) )
9	8	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) mod 𝑀 ) = ( 𝐴 mod 𝑀 ) )
10		modabs2	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐵 mod 𝑀 ) mod 𝑀 ) = ( 𝐵 mod 𝑀 ) )
11	10	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐵 mod 𝑀 ) mod 𝑀 ) = ( 𝐵 mod 𝑀 ) )
12	2 3 5 6 7 9 11	modsub12d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝑀 ) − ( 𝐵 mod 𝑀 ) ) mod 𝑀 ) = ( ( 𝐴 − 𝐵 ) mod 𝑀 ) )