# Metamath Proof Explorer

Description: The sum of a positive integer and a nonnegative integer less than the positive integer is equal to the nonnegative integer modulo the positive integer. (Contributed by Alexander van der Vekens, 30-Oct-2018) (Proof shortened by AV, 5-Jul-2020)

Ref Expression
Assertion addmodid ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {A}<{M}\right)\to \left({M}+{A}\right)\mathrm{mod}{M}={A}$

### Proof

Step Hyp Ref Expression
1 nncn ${⊢}{M}\in ℕ\to {M}\in ℂ$
2 1 mulid2d ${⊢}{M}\in ℕ\to 1\cdot {M}={M}$
3 2 3ad2ant2 ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {A}<{M}\right)\to 1\cdot {M}={M}$
4 3 eqcomd ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {A}<{M}\right)\to {M}=1\cdot {M}$
5 4 oveq1d ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {A}<{M}\right)\to {M}+{A}=1\cdot {M}+{A}$
6 5 oveq1d ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {A}<{M}\right)\to \left({M}+{A}\right)\mathrm{mod}{M}=\left(1\cdot {M}+{A}\right)\mathrm{mod}{M}$
7 1zzd ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {A}<{M}\right)\to 1\in ℤ$
8 nnrp ${⊢}{M}\in ℕ\to {M}\in {ℝ}^{+}$
9 8 3ad2ant2 ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {A}<{M}\right)\to {M}\in {ℝ}^{+}$
10 nn0re ${⊢}{A}\in {ℕ}_{0}\to {A}\in ℝ$
11 10 rexrd ${⊢}{A}\in {ℕ}_{0}\to {A}\in {ℝ}^{*}$
12 11 3ad2ant1 ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {A}<{M}\right)\to {A}\in {ℝ}^{*}$
13 nn0ge0 ${⊢}{A}\in {ℕ}_{0}\to 0\le {A}$
14 13 3ad2ant1 ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {A}<{M}\right)\to 0\le {A}$
15 simp3 ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {A}<{M}\right)\to {A}<{M}$
16 0xr ${⊢}0\in {ℝ}^{*}$
17 nnre ${⊢}{M}\in ℕ\to {M}\in ℝ$
18 17 rexrd ${⊢}{M}\in ℕ\to {M}\in {ℝ}^{*}$
19 18 3ad2ant2 ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {A}<{M}\right)\to {M}\in {ℝ}^{*}$
20 elico1 ${⊢}\left(0\in {ℝ}^{*}\wedge {M}\in {ℝ}^{*}\right)\to \left({A}\in \left[0,{M}\right)↔\left({A}\in {ℝ}^{*}\wedge 0\le {A}\wedge {A}<{M}\right)\right)$
21 16 19 20 sylancr ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {A}<{M}\right)\to \left({A}\in \left[0,{M}\right)↔\left({A}\in {ℝ}^{*}\wedge 0\le {A}\wedge {A}<{M}\right)\right)$
22 12 14 15 21 mpbir3and ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {A}<{M}\right)\to {A}\in \left[0,{M}\right)$
23 muladdmodid ${⊢}\left(1\in ℤ\wedge {M}\in {ℝ}^{+}\wedge {A}\in \left[0,{M}\right)\right)\to \left(1\cdot {M}+{A}\right)\mathrm{mod}{M}={A}$
24 7 9 22 23 syl3anc ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {A}<{M}\right)\to \left(1\cdot {M}+{A}\right)\mathrm{mod}{M}={A}$
25 6 24 eqtrd ${⊢}\left({A}\in {ℕ}_{0}\wedge {M}\in ℕ\wedge {A}<{M}\right)\to \left({M}+{A}\right)\mathrm{mod}{M}={A}$