This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mullidd ⊢ ( 𝑀 ∈ ℕ → ( 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 𝑀 ) = 𝐴 )