Metamath Proof Explorer


Theorem addmodidr

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 AV, 19-Mar-2021)

Ref Expression
Assertion addmodidr ( ( 𝐴 ∈ ℕ0𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → ( ( 𝐴 + 𝑀 ) mod 𝑀 ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 nn0cn ( 𝐴 ∈ ℕ0𝐴 ∈ ℂ )
2 nncn ( 𝑀 ∈ ℕ → 𝑀 ∈ ℂ )
3 addcom ( ( 𝐴 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝐴 + 𝑀 ) = ( 𝑀 + 𝐴 ) )
4 1 2 3 syl2an ( ( 𝐴 ∈ ℕ0𝑀 ∈ ℕ ) → ( 𝐴 + 𝑀 ) = ( 𝑀 + 𝐴 ) )
5 4 3adant3 ( ( 𝐴 ∈ ℕ0𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → ( 𝐴 + 𝑀 ) = ( 𝑀 + 𝐴 ) )
6 5 oveq1d ( ( 𝐴 ∈ ℕ0𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → ( ( 𝐴 + 𝑀 ) mod 𝑀 ) = ( ( 𝑀 + 𝐴 ) mod 𝑀 ) )
7 addmodid ( ( 𝐴 ∈ ℕ0𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → ( ( 𝑀 + 𝐴 ) mod 𝑀 ) = 𝐴 )
8 6 7 eqtrd ( ( 𝐴 ∈ ℕ0𝑀 ∈ ℕ ∧ 𝐴 < 𝑀 ) → ( ( 𝐴 + 𝑀 ) mod 𝑀 ) = 𝐴 )