Theorem addmodid

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	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → ( ( 𝑀 + 𝐴 ) mod 𝑀 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nncn	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
2	1	mulid2d	⊢ ( 𝑀 ∈ ℕ → ( 1 · 𝑀 ) = 𝑀 )
3	2	3ad2ant2	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → ( 1 · 𝑀 ) = 𝑀 )
4	3	eqcomd	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → 𝑀 = ( 1 · 𝑀 ) )
5	4	oveq1d	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → ( 𝑀 + 𝐴 ) = ( ( 1 · 𝑀 ) + 𝐴 ) )
6	5	oveq1d	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → ( ( 𝑀 + 𝐴 ) mod 𝑀 ) = ( ( ( 1 · 𝑀 ) + 𝐴 ) mod 𝑀 ) )
7		1zzd	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → 1 ∈ ℤ )
8		nnrp	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ+ )
9	8	3ad2ant2	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → 𝑀 ∈ ℝ+ )
10		nn0re	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ )
11	10	rexrd	⊢ ( 𝐴 ∈ ℕ0 → 𝐴 ∈ ℝ* )
12	11	3ad2ant1	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → 𝐴 ∈ ℝ* )
13		nn0ge0	⊢ ( 𝐴 ∈ ℕ0 → 0 ≤ 𝐴 )
14	13	3ad2ant1	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → 0 ≤ 𝐴 )
15		simp3	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → 𝐴 < 𝑀 )
16		0xr	⊢ 0 ∈ ℝ*
17		nnre	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
18	17	rexrd	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ* )
19	18	3ad2ant2	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → 𝑀 ∈ ℝ* )
20		elico1	⊢ ( ( 0 ∈ ℝ* ∧ 𝑀 ∈ ℝ* ) → ( 𝐴 ∈ ( 0 [,) 𝑀 ) ↔ ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) )
21	16 19 20	sylancr	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → ( 𝐴 ∈ ( 0 [,) 𝑀 ) ↔ ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ∧ 𝐴 < 𝑀 ) ) )
22	12 14 15 21	mpbir3and	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → 𝐴 ∈ ( 0 [,) 𝑀 ) )
23		muladdmodid	⊢ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℝ+ ∧ 𝐴 ∈ ( 0 [,) 𝑀 ) ) → ( ( ( 1 · 𝑀 ) + 𝐴 ) mod 𝑀 ) = 𝐴 )
24	7 9 22 23	syl3anc	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → ( ( ( 1 · 𝑀 ) + 𝐴 ) mod 𝑀 ) = 𝐴 )
25	6 24	eqtrd	⊢ ( ( 𝐴 ∈ ℕ0 ∧ 𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → ( ( 𝑀 + 𝐴 ) mod 𝑀 ) = 𝐴 )