Theorem modadd2mod

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, 17-May-2018)

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

Proof

Step	Hyp	Ref	Expression
1		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
2	1	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
3		modcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ∈ ℝ )
4	3	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ∈ ℂ )
5	4	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) ∈ ℂ )
6	2 5	addcomd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) = ( ( 𝐴 mod 𝑀 ) + 𝐵 ) )
7	6	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) mod 𝑀 ) = ( ( ( 𝐴 mod 𝑀 ) + 𝐵 ) mod 𝑀 ) )
8		modaddmod	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝑀 ) + 𝐵 ) mod 𝑀 ) = ( ( 𝐴 + 𝐵 ) mod 𝑀 ) )
9		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
10		addcom	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
11	9 1 10	syl2an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) = ( 𝐵 + 𝐴 ) )
12	11	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐴 + 𝐵 ) mod 𝑀 ) = ( ( 𝐵 + 𝐴 ) mod 𝑀 ) )
13	12	3adant3	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐴 + 𝐵 ) mod 𝑀 ) = ( ( 𝐵 + 𝐴 ) mod 𝑀 ) )
14	7 8 13	3eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) mod 𝑀 ) = ( ( 𝐵 + 𝐴 ) mod 𝑀 ) )