Metamath Proof Explorer

Theorem modaddmodlo

Description: The sum of an integer modulo a positive integer and another integer equals the sum of the two integers modulo the positive integer if the other integer is in the lower part of the range between 0 and the positive integer. (Contributed by AV, 30-Oct-2018)

Ref Expression
Assertion modaddmodlo ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) = ( ( 𝐵 + 𝐴 ) mod 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 elfzoelz ⊢ ( 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) → 𝐵 ∈ ℤ )
2 1 zred ⊢ ( 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) → 𝐵 ∈ ℝ )
3 2 adantr ⊢ ( ( 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) → 𝐵 ∈ ℝ )
4 zmodcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝐴 mod 𝑀 ) ∈ ℕ0 )
5 4 nn0red ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝐴 mod 𝑀 ) ∈ ℝ )
6 5 adantl ⊢ ( ( 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) → ( 𝐴 mod 𝑀 ) ∈ ℝ )
7 3 6 readdcld ⊢ ( ( 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ∈ ℝ )
8 7 ancoms ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ∈ ℝ )
9 nnrp ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ+ )
10 9 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ) → 𝑀 ∈ ℝ+ )
11 2 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ) → 𝐵 ∈ ℝ )
12 5 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ) → ( 𝐴 mod 𝑀 ) ∈ ℝ )
13 elfzole1 ⊢ ( 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) → 0 ≤ 𝐵 )
14 13 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ) → 0 ≤ 𝐵 )
15 4 nn0ge0d ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → 0 ≤ ( 𝐴 mod 𝑀 ) )
16 15 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ) → 0 ≤ ( 𝐴 mod 𝑀 ) )
17 11 12 14 16 addge0d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ) → 0 ≤ ( 𝐵 + ( 𝐴 mod 𝑀 ) ) )
18 elfzolt2 ⊢ ( 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) → 𝐵 < ( 𝑀 − ( 𝐴 mod 𝑀 ) ) )
19 18 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ) → 𝐵 < ( 𝑀 − ( 𝐴 mod 𝑀 ) ) )
20 nnre ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
21 20 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ) → 𝑀 ∈ ℝ )
22 11 12 21 ltaddsubd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) < 𝑀 ↔ 𝐵 < ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) )
23 19 22 mpbird ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) < 𝑀 )
24 modid ⊢ ( ( ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ∧ ( 𝐵 + ( 𝐴 mod 𝑀 ) ) < 𝑀 ) ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) mod 𝑀 ) = ( 𝐵 + ( 𝐴 mod 𝑀 ) ) )
25 8 10 17 23 24 syl22anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) mod 𝑀 ) = ( 𝐵 + ( 𝐴 mod 𝑀 ) ) )
26 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
27 26 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → 𝐴 ∈ ℝ )
28 27 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ) → 𝐴 ∈ ℝ )
29 modadd2mod ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) mod 𝑀 ) = ( ( 𝐵 + 𝐴 ) mod 𝑀 ) )
30 28 11 10 29 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) mod 𝑀 ) = ( ( 𝐵 + 𝐴 ) mod 𝑀 ) )
31 25 30 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) = ( ( 𝐵 + 𝐴 ) mod 𝑀 ) )
32 31 ex ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝐵 ∈ ( 0 ..^ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) = ( ( 𝐵 + 𝐴 ) mod 𝑀 ) ) )