# Metamath Proof Explorer

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 ${⊢}\left({A}\in ℤ\wedge {M}\in ℕ\right)\to \left({B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\to {B}+\left({A}\mathrm{mod}{M}\right)=\left({B}+{A}\right)\mathrm{mod}{M}\right)$

### Proof

Step Hyp Ref Expression
1 elfzoelz ${⊢}{B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\to {B}\in ℤ$
2 1 zred ${⊢}{B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\to {B}\in ℝ$
3 2 adantr ${⊢}\left({B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\wedge \left({A}\in ℤ\wedge {M}\in ℕ\right)\right)\to {B}\in ℝ$
4 zmodcl ${⊢}\left({A}\in ℤ\wedge {M}\in ℕ\right)\to {A}\mathrm{mod}{M}\in {ℕ}_{0}$
5 4 nn0red ${⊢}\left({A}\in ℤ\wedge {M}\in ℕ\right)\to {A}\mathrm{mod}{M}\in ℝ$
6 5 adantl ${⊢}\left({B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\wedge \left({A}\in ℤ\wedge {M}\in ℕ\right)\right)\to {A}\mathrm{mod}{M}\in ℝ$
7 3 6 readdcld ${⊢}\left({B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\wedge \left({A}\in ℤ\wedge {M}\in ℕ\right)\right)\to {B}+\left({A}\mathrm{mod}{M}\right)\in ℝ$
8 7 ancoms ${⊢}\left(\left({A}\in ℤ\wedge {M}\in ℕ\right)\wedge {B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\right)\to {B}+\left({A}\mathrm{mod}{M}\right)\in ℝ$
9 nnrp ${⊢}{M}\in ℕ\to {M}\in {ℝ}^{+}$
10 9 ad2antlr ${⊢}\left(\left({A}\in ℤ\wedge {M}\in ℕ\right)\wedge {B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\right)\to {M}\in {ℝ}^{+}$
11 2 adantl ${⊢}\left(\left({A}\in ℤ\wedge {M}\in ℕ\right)\wedge {B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\right)\to {B}\in ℝ$
12 5 adantr ${⊢}\left(\left({A}\in ℤ\wedge {M}\in ℕ\right)\wedge {B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\right)\to {A}\mathrm{mod}{M}\in ℝ$
13 elfzole1 ${⊢}{B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\to 0\le {B}$
14 13 adantl ${⊢}\left(\left({A}\in ℤ\wedge {M}\in ℕ\right)\wedge {B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\right)\to 0\le {B}$
15 4 nn0ge0d ${⊢}\left({A}\in ℤ\wedge {M}\in ℕ\right)\to 0\le {A}\mathrm{mod}{M}$
16 15 adantr ${⊢}\left(\left({A}\in ℤ\wedge {M}\in ℕ\right)\wedge {B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\right)\to 0\le {A}\mathrm{mod}{M}$
17 11 12 14 16 addge0d ${⊢}\left(\left({A}\in ℤ\wedge {M}\in ℕ\right)\wedge {B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\right)\to 0\le {B}+\left({A}\mathrm{mod}{M}\right)$
18 elfzolt2 ${⊢}{B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\to {B}<{M}-\left({A}\mathrm{mod}{M}\right)$
19 18 adantl ${⊢}\left(\left({A}\in ℤ\wedge {M}\in ℕ\right)\wedge {B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\right)\to {B}<{M}-\left({A}\mathrm{mod}{M}\right)$
20 nnre ${⊢}{M}\in ℕ\to {M}\in ℝ$
21 20 ad2antlr ${⊢}\left(\left({A}\in ℤ\wedge {M}\in ℕ\right)\wedge {B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\right)\to {M}\in ℝ$
22 11 12 21 ltaddsubd ${⊢}\left(\left({A}\in ℤ\wedge {M}\in ℕ\right)\wedge {B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\right)\to \left({B}+\left({A}\mathrm{mod}{M}\right)<{M}↔{B}<{M}-\left({A}\mathrm{mod}{M}\right)\right)$
23 19 22 mpbird ${⊢}\left(\left({A}\in ℤ\wedge {M}\in ℕ\right)\wedge {B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\right)\to {B}+\left({A}\mathrm{mod}{M}\right)<{M}$
24 modid ${⊢}\left(\left({B}+\left({A}\mathrm{mod}{M}\right)\in ℝ\wedge {M}\in {ℝ}^{+}\right)\wedge \left(0\le {B}+\left({A}\mathrm{mod}{M}\right)\wedge {B}+\left({A}\mathrm{mod}{M}\right)<{M}\right)\right)\to \left({B}+\left({A}\mathrm{mod}{M}\right)\right)\mathrm{mod}{M}={B}+\left({A}\mathrm{mod}{M}\right)$
25 8 10 17 23 24 syl22anc ${⊢}\left(\left({A}\in ℤ\wedge {M}\in ℕ\right)\wedge {B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\right)\to \left({B}+\left({A}\mathrm{mod}{M}\right)\right)\mathrm{mod}{M}={B}+\left({A}\mathrm{mod}{M}\right)$
26 zre ${⊢}{A}\in ℤ\to {A}\in ℝ$
27 26 adantr ${⊢}\left({A}\in ℤ\wedge {M}\in ℕ\right)\to {A}\in ℝ$
28 27 adantr ${⊢}\left(\left({A}\in ℤ\wedge {M}\in ℕ\right)\wedge {B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\right)\to {A}\in ℝ$
29 modadd2mod ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to \left({B}+\left({A}\mathrm{mod}{M}\right)\right)\mathrm{mod}{M}=\left({B}+{A}\right)\mathrm{mod}{M}$
30 28 11 10 29 syl3anc ${⊢}\left(\left({A}\in ℤ\wedge {M}\in ℕ\right)\wedge {B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\right)\to \left({B}+\left({A}\mathrm{mod}{M}\right)\right)\mathrm{mod}{M}=\left({B}+{A}\right)\mathrm{mod}{M}$
31 25 30 eqtr3d ${⊢}\left(\left({A}\in ℤ\wedge {M}\in ℕ\right)\wedge {B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\right)\to {B}+\left({A}\mathrm{mod}{M}\right)=\left({B}+{A}\right)\mathrm{mod}{M}$
32 31 ex ${⊢}\left({A}\in ℤ\wedge {M}\in ℕ\right)\to \left({B}\in \left(0..^{M}-\left({A}\mathrm{mod}{M}\right)\right)\to {B}+\left({A}\mathrm{mod}{M}\right)=\left({B}+{A}\right)\mathrm{mod}{M}\right)$