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 𝑀 ) = 𝐴 )