Theorem m1modnnsub1

Description: Minus one modulo a positive integer is equal to the integer minus one. (Contributed by AV, 14-Jul-2021)

	Ref	Expression
Assertion	m1modnnsub1	⊢ ( 𝑀 ∈ ℕ → ( - 1 mod 𝑀 ) = ( 𝑀 − 1 ) )

Proof

Step	Hyp	Ref	Expression
1		1re	⊢ 1 ∈ ℝ
2		nnrp	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ+ )
3		negmod	⊢ ( ( 1 ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) → ( - 1 mod 𝑀 ) = ( ( 𝑀 − 1 ) mod 𝑀 ) )
4	1 2 3	sylancr	⊢ ( 𝑀 ∈ ℕ → ( - 1 mod 𝑀 ) = ( ( 𝑀 − 1 ) mod 𝑀 ) )
5		nnre	⊢ ( 𝑀 ∈ ℕ → 𝑀 ∈ ℝ )
6		peano2rem	⊢ ( 𝑀 ∈ ℝ → ( 𝑀 − 1 ) ∈ ℝ )
7	5 6	syl	⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 1 ) ∈ ℝ )
8		nnm1ge0	⊢ ( 𝑀 ∈ ℕ → 0 ≤ ( 𝑀 − 1 ) )
9	5	ltm1d	⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 1 ) < 𝑀 )
10		modid	⊢ ( ( ( ( 𝑀 − 1 ) ∈ ℝ ∧ 𝑀 ∈ ℝ+ ) ∧ ( 0 ≤ ( 𝑀 − 1 ) ∧ ( 𝑀 − 1 ) < 𝑀 ) ) → ( ( 𝑀 − 1 ) mod 𝑀 ) = ( 𝑀 − 1 ) )
11	7 2 8 9 10	syl22anc	⊢ ( 𝑀 ∈ ℕ → ( ( 𝑀 − 1 ) mod 𝑀 ) = ( 𝑀 − 1 ) )
12	4 11	eqtrd	⊢ ( 𝑀 ∈ ℕ → ( - 1 mod 𝑀 ) = ( 𝑀 − 1 ) )