This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 biimtrdi ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ+ ) ) → ( ( 𝐴 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 𝐷 ) )