Theorem modadd1

Description: Addition property of the modulo operation. (Contributed by NM, 12-Nov-2008)

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

Proof

Step	Hyp	Ref	Expression
1		modval	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝐴 mod 𝐷 ) = ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) )
2		modval	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝐵 mod 𝐷 ) = ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) )
3	1 2	eqeqan12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ↔ ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) = ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) )
4	3	anandirs	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐷 ∈ ℝ+ ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ↔ ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) = ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) )
5	4	adantrl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ↔ ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) = ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) )
6		oveq1	⊢ ( ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) = ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) → ( ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) + 𝐶 ) = ( ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) + 𝐶 ) )
7	5 6	syl6bi	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) → ( ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) + 𝐶 ) = ( ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) + 𝐶 ) ) )
8		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
9	8	adantr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐴 ∈ ℂ )
10		recn	⊢ ( 𝐶 ∈ ℝ → 𝐶 ∈ ℂ )
11	10	ad2antrl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐶 ∈ ℂ )
12		rpcn	⊢ ( 𝐷 ∈ ℝ+ → 𝐷 ∈ ℂ )
13	12	adantl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 𝐷 ∈ ℂ )
14		rerpdivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝐴 / 𝐷 ) ∈ ℝ )
15		reflcl	⊢ ( ( 𝐴 / 𝐷 ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ∈ ℝ )
16	15	recnd	⊢ ( ( 𝐴 / 𝐷 ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ∈ ℂ )
17	14 16	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ∈ ℂ )
18	13 17	mulcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ∈ ℂ )
19	18	adantrl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ∈ ℂ )
20	9 11 19	addsubd	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) = ( ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) + 𝐶 ) )
21	20	adantlr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) = ( ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) + 𝐶 ) )
22		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
23	22	adantr	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐵 ∈ ℂ )
24	10	ad2antrl	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐶 ∈ ℂ )
25	12	adantl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → 𝐷 ∈ ℂ )
26		rerpdivcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝐵 / 𝐷 ) ∈ ℝ )
27		reflcl	⊢ ( ( 𝐵 / 𝐷 ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ∈ ℝ )
28	27	recnd	⊢ ( ( 𝐵 / 𝐷 ) ∈ ℝ → ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ∈ ℂ )
29	26 28	syl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ∈ ℂ )
30	25 29	mulcld	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ∈ ℂ )
31	30	adantrl	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ∈ ℂ )
32	23 24 31	addsubd	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐵 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) = ( ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) + 𝐶 ) )
33	32	adantll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐵 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) = ( ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) + 𝐶 ) )
34	21 33	eqeq12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( ( 𝐴 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) = ( ( 𝐵 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ↔ ( ( 𝐴 − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) + 𝐶 ) = ( ( 𝐵 − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) + 𝐶 ) ) )
35	7 34	sylibrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) → ( ( 𝐴 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) = ( ( 𝐵 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) ) )
36		oveq1	⊢ ( ( ( 𝐴 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) = ( ( 𝐵 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) → ( ( ( 𝐴 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) mod 𝐷 ) = ( ( ( 𝐵 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) mod 𝐷 ) )
37		readdcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 + 𝐶 ) ∈ ℝ )
38	37	adantrr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐴 + 𝐶 ) ∈ ℝ )
39		simprr	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐷 ∈ ℝ+ )
40	14	flcld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ∈ ℤ )
41	40	adantrl	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ∈ ℤ )
42		modcyc2	⊢ ( ( ( 𝐴 + 𝐶 ) ∈ ℝ ∧ 𝐷 ∈ ℝ+ ∧ ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ∈ ℤ ) → ( ( ( 𝐴 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) mod 𝐷 ) = ( ( 𝐴 + 𝐶 ) mod 𝐷 ) )
43	38 39 41 42	syl3anc	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( ( 𝐴 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) mod 𝐷 ) = ( ( 𝐴 + 𝐶 ) mod 𝐷 ) )
44	43	adantlr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( ( 𝐴 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) mod 𝐷 ) = ( ( 𝐴 + 𝐶 ) mod 𝐷 ) )
45		readdcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
46	45	adantrr	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
47		simprr	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → 𝐷 ∈ ℝ+ )
48	26	flcld	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) → ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ∈ ℤ )
49	48	adantrl	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ∈ ℤ )
50		modcyc2	⊢ ( ( ( 𝐵 + 𝐶 ) ∈ ℝ ∧ 𝐷 ∈ ℝ+ ∧ ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ∈ ℤ ) → ( ( ( 𝐵 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) )
51	46 47 49 50	syl3anc	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( ( 𝐵 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) )
52	51	adantll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( ( 𝐵 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) )
53	44 52	eqeq12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( ( ( 𝐴 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) mod 𝐷 ) = ( ( ( 𝐵 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) mod 𝐷 ) ↔ ( ( 𝐴 + 𝐶 ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) ) )
54	36 53	imbitrid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( ( 𝐴 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐴 / 𝐷 ) ) ) ) = ( ( 𝐵 + 𝐶 ) − ( 𝐷 · ( ⌊ ‘ ( 𝐵 / 𝐷 ) ) ) ) → ( ( 𝐴 + 𝐶 ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) ) )
55	35 54	syld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) → ( ( 𝐴 + 𝐶 ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) ) )
56	55	3impia	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ∧ ( 𝐴 mod 𝐷 ) = ( 𝐵 mod 𝐷 ) ) → ( ( 𝐴 + 𝐶 ) mod 𝐷 ) = ( ( 𝐵 + 𝐶 ) mod 𝐷 ) )