Metamath Proof Explorer

Theorem modaddmodup

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

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

Proof

Step Hyp Ref Expression
1 elfzoelz ⊢ ( 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) → 𝐵 ∈ ℤ )
2 1 zred ⊢ ( 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) → 𝐵 ∈ ℝ )
3 2 adantr ⊢ ( ( 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) → 𝐵 ∈ ℝ )
4 zmodcl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝐴 mod 𝑀 ) ∈ ℕ0 )
5 4 nn0red ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝐴 mod 𝑀 ) ∈ ℝ )
6 5 adantl ⊢ ( ( 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) → ( 𝐴 mod 𝑀 ) ∈ ℝ )
7 3 6 readdcld ⊢ ( ( 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ∈ ℝ )
8 7 ancoms ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ∈ ℝ )
9 nnrp ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ+ )
10 9 ad2antlr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) ) → 𝑀 ∈ ℝ+ )
11 elfzo2 ⊢ ( 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) ↔ ( 𝐵 ∈ ( ℤ≥ ‘ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ∧ 𝑀 ∈ ℤ ∧ 𝐵 < 𝑀 ) )
12 eluz2 ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ↔ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ≤ 𝐵 ) )
13 nnre ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
14 13 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → 𝑀 ∈ ℝ )
15 14 adantl ⊢ ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) → 𝑀 ∈ ℝ )
16 5 adantl ⊢ ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) → ( 𝐴 mod 𝑀 ) ∈ ℝ )
17 zre ⊢ ( 𝐵 ∈ ℤ → 𝐵 ∈ ℝ )
18 17 adantr ⊢ ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) → 𝐵 ∈ ℝ )
19 15 16 18 lesubaddd ⊢ ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) → ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ≤ 𝐵 ↔ 𝑀 ≤ ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ) )
20 19 biimpd ⊢ ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) → ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ≤ 𝐵 → 𝑀 ≤ ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ) )
21 20 impancom ⊢ ( ( 𝐵 ∈ ℤ ∧ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ≤ 𝐵 ) → ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → 𝑀 ≤ ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ) )
22 21 3adant1 ⊢ ( ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ≤ 𝐵 ) → ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → 𝑀 ≤ ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ) )
23 12 22 sylbi ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) → ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → 𝑀 ≤ ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ) )
24 23 3ad2ant1 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ∧ 𝑀 ∈ ℤ ∧ 𝐵 < 𝑀 ) → ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → 𝑀 ≤ ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ) )
25 11 24 sylbi ⊢ ( 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) → ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → 𝑀 ≤ ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ) )
26 25 impcom ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) ) → 𝑀 ≤ ( 𝐵 + ( 𝐴 mod 𝑀 ) ) )
27 eluzelz ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) → 𝐵 ∈ ℤ )
28 17 5 anim12i ⊢ ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) → ( 𝐵 ∈ ℝ ∧ ( 𝐴 mod 𝑀 ) ∈ ℝ ) )
29 13 13 jca ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
30 29 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝑀 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
31 30 adantl ⊢ ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) → ( 𝑀 ∈ ℝ ∧ 𝑀 ∈ ℝ ) )
32 28 31 jca ⊢ ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) → ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 mod 𝑀 ) ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ) )
33 32 adantr ⊢ ( ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) ∧ 𝐵 < 𝑀 ) → ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 mod 𝑀 ) ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ) )
34 simpr ⊢ ( ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) ∧ 𝐵 < 𝑀 ) → 𝐵 < 𝑀 )
35 zre ⊢ ( 𝐴 ∈ ℤ → 𝐴 ∈ ℝ )
36 modlt ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( 𝐴 mod 𝑀 ) < 𝑀 )
37 35 9 36 syl2an ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝐴 mod 𝑀 ) < 𝑀 )
38 5 14 37 ltled ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝐴 mod 𝑀 ) ≤ 𝑀 )
39 38 ad2antlr ⊢ ( ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) ∧ 𝐵 < 𝑀 ) → ( 𝐴 mod 𝑀 ) ≤ 𝑀 )
40 34 39 jca ⊢ ( ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) ∧ 𝐵 < 𝑀 ) → ( 𝐵 < 𝑀 ∧ ( 𝐴 mod 𝑀 ) ≤ 𝑀 ) )
41 ltleadd ⊢ ( ( ( 𝐵 ∈ ℝ ∧ ( 𝐴 mod 𝑀 ) ∈ ℝ ) ∧ ( 𝑀 ∈ ℝ ∧ 𝑀 ∈ ℝ ) ) → ( ( 𝐵 < 𝑀 ∧ ( 𝐴 mod 𝑀 ) ≤ 𝑀 ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) < ( 𝑀 + 𝑀 ) ) )
42 33 40 41 sylc ⊢ ( ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) ∧ 𝐵 < 𝑀 ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) < ( 𝑀 + 𝑀 ) )
43 nncn ⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
44 43 2timesd ⊢ ( 𝑀 ∈ ℕ → ( 2 · 𝑀 ) = ( 𝑀 + 𝑀 ) )
45 44 adantl ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 2 · 𝑀 ) = ( 𝑀 + 𝑀 ) )
46 45 ad2antlr ⊢ ( ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) ∧ 𝐵 < 𝑀 ) → ( 2 · 𝑀 ) = ( 𝑀 + 𝑀 ) )
47 42 46 breqtrrd ⊢ ( ( ( 𝐵 ∈ ℤ ∧ ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ) ∧ 𝐵 < 𝑀 ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) < ( 2 · 𝑀 ) )
48 47 exp31 ⊢ ( 𝐵 ∈ ℤ → ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝐵 < 𝑀 → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) < ( 2 · 𝑀 ) ) ) )
49 48 com23 ⊢ ( 𝐵 ∈ ℤ → ( 𝐵 < 𝑀 → ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) < ( 2 · 𝑀 ) ) ) )
50 27 49 syl ⊢ ( 𝐵 ∈ ( ℤ≥ ‘ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) → ( 𝐵 < 𝑀 → ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) < ( 2 · 𝑀 ) ) ) )
51 50 imp ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ∧ 𝐵 < 𝑀 ) → ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) < ( 2 · 𝑀 ) ) )
52 51 3adant2 ⊢ ( ( 𝐵 ∈ ( ℤ≥ ‘ ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ) ∧ 𝑀 ∈ ℤ ∧ 𝐵 < 𝑀 ) → ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) < ( 2 · 𝑀 ) ) )
53 11 52 sylbi ⊢ ( 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) → ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) < ( 2 · 𝑀 ) ) )
54 53 impcom ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) ) → ( 𝐵 + ( 𝐴 mod 𝑀 ) ) < ( 2 · 𝑀 ) )
55 2submod ⊢ ( ( ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝑀 ≤ ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ∧ ( 𝐵 + ( 𝐴 mod 𝑀 ) ) < ( 2 · 𝑀 ) ) ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) mod 𝑀 ) = ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) − 𝑀 ) )
56 55 eqcomd ⊢ ( ( ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 𝑀 ≤ ( 𝐵 + ( 𝐴 mod 𝑀 ) ) ∧ ( 𝐵 + ( 𝐴 mod 𝑀 ) ) < ( 2 · 𝑀 ) ) ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) − 𝑀 ) = ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) mod 𝑀 ) )
57 8 10 26 54 56 syl22anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) − 𝑀 ) = ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) mod 𝑀 ) )
58 35 adantr ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → 𝐴 ∈ ℝ )
59 58 adantr ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) ) → 𝐴 ∈ ℝ )
60 2 adantl ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) ) → 𝐵 ∈ ℝ )
61 modadd2mod ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) mod 𝑀 ) = ( ( 𝐵 + 𝐴 ) mod 𝑀 ) )
62 59 60 10 61 syl3anc ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) mod 𝑀 ) = ( ( 𝐵 + 𝐴 ) mod 𝑀 ) )
63 57 62 eqtrd ⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) ∧ 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) − 𝑀 ) = ( ( 𝐵 + 𝐴 ) mod 𝑀 ) )
64 63 ex ⊢ ( ( 𝐴 ∈ ℤ ∧ 𝑀 ∈ ℕ ) → ( 𝐵 ∈ ( ( 𝑀 − ( 𝐴 mod 𝑀 ) ) ..^ 𝑀 ) → ( ( 𝐵 + ( 𝐴 mod 𝑀 ) ) − 𝑀 ) = ( ( 𝐵 + 𝐴 ) mod 𝑀 ) ) )