Theorem modaddmod

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

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

Proof

Step	Hyp	Ref	Expression
1		modcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ∈ ℝ )
2		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
3	1 2	jca	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) )
4	3	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) )
5		3simpc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) )
6		modabs2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) mod 𝑀 ) = ( 𝐴 mod 𝑀 ) )
7	6	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 mod 𝑀 ) mod 𝑀 ) = ( 𝐴 mod 𝑀 ) )
8		modadd1	⊢ ( ( ( ( 𝐴 mod 𝑀 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) ∧ ( ( 𝐴 mod 𝑀 ) mod 𝑀 ) = ( 𝐴 mod 𝑀 ) ) → ( ( ( 𝐴 mod 𝑀 ) + 𝐵 ) mod 𝑀 ) = ( ( 𝐴 + 𝐵 ) mod 𝑀 ) )
9	4 5 7 8	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝑀 ) + 𝐵 ) mod 𝑀 ) = ( ( 𝐴 + 𝐵 ) mod 𝑀 ) )