Theorem modaddabs

Description: Absorption law for modulo. (Contributed by Paul Chapman, 22-Jun-2011)

	Ref	Expression
Assertion	modaddabs	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝐶 ) + ( 𝐵 mod 𝐶 ) ) mod 𝐶 ) = ( ( 𝐴 + 𝐵 ) mod 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		modcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 mod 𝐶 ) ∈ ℝ )
2	1	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 mod 𝐶 ) ∈ ℂ )
3	2	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐴 mod 𝐶 ) ∈ ℂ )
4		modcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 mod 𝐶 ) ∈ ℝ )
5	4	recnd	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 mod 𝐶 ) ∈ ℂ )
6	5	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 mod 𝐶 ) ∈ ℂ )
7	3 6	addcomd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) + ( 𝐵 mod 𝐶 ) ) = ( ( 𝐵 mod 𝐶 ) + ( 𝐴 mod 𝐶 ) ) )
8	7	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝐶 ) + ( 𝐵 mod 𝐶 ) ) mod 𝐶 ) = ( ( ( 𝐵 mod 𝐶 ) + ( 𝐴 mod 𝐶 ) ) mod 𝐶 ) )
9		simpl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
10	4 9	jca	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐵 mod 𝐶 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
11	10	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐵 mod 𝐶 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) )
12		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐶 ∈ ℝ+ )
13	1 12	jca	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) )
14	13	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) )
15		modabs2	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐵 mod 𝐶 ) mod 𝐶 ) = ( 𝐵 mod 𝐶 ) )
16	15	3adant1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐵 mod 𝐶 ) mod 𝐶 ) = ( 𝐵 mod 𝐶 ) )
17		modadd1	⊢ ( ( ( ( 𝐵 mod 𝐶 ) ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐴 mod 𝐶 ) ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ ( ( 𝐵 mod 𝐶 ) mod 𝐶 ) = ( 𝐵 mod 𝐶 ) ) → ( ( ( 𝐵 mod 𝐶 ) + ( 𝐴 mod 𝐶 ) ) mod 𝐶 ) = ( ( 𝐵 + ( 𝐴 mod 𝐶 ) ) mod 𝐶 ) )
18	11 14 16 17	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐵 mod 𝐶 ) + ( 𝐴 mod 𝐶 ) ) mod 𝐶 ) = ( ( 𝐵 + ( 𝐴 mod 𝐶 ) ) mod 𝐶 ) )
19		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
20	19	3ad2ant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐵 ∈ ℂ )
21	3 20	addcomd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) + 𝐵 ) = ( 𝐵 + ( 𝐴 mod 𝐶 ) ) )
22	21	oveq1d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝐶 ) + 𝐵 ) mod 𝐶 ) = ( ( 𝐵 + ( 𝐴 mod 𝐶 ) ) mod 𝐶 ) )
23	18 22	eqtr4d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐵 mod 𝐶 ) + ( 𝐴 mod 𝐶 ) ) mod 𝐶 ) = ( ( ( 𝐴 mod 𝐶 ) + 𝐵 ) mod 𝐶 ) )
24		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → 𝐴 ∈ ℝ )
25	1 24	jca	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) )
26	25	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) )
27		3simpc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) )
28		modabs2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) mod 𝐶 ) = ( 𝐴 mod 𝐶 ) )
29	28	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐶 ) mod 𝐶 ) = ( 𝐴 mod 𝐶 ) )
30		modadd1	⊢ ( ( ( ( 𝐴 mod 𝐶 ) ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) ∧ ( ( 𝐴 mod 𝐶 ) mod 𝐶 ) = ( 𝐴 mod 𝐶 ) ) → ( ( ( 𝐴 mod 𝐶 ) + 𝐵 ) mod 𝐶 ) = ( ( 𝐴 + 𝐵 ) mod 𝐶 ) )
31	26 27 29 30	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝐶 ) + 𝐵 ) mod 𝐶 ) = ( ( 𝐴 + 𝐵 ) mod 𝐶 ) )
32	8 23 31	3eqtrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ+ ) → ( ( ( 𝐴 mod 𝐶 ) + ( 𝐵 mod 𝐶 ) ) mod 𝐶 ) = ( ( 𝐴 + 𝐵 ) mod 𝐶 ) )