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

Metamath Proof Explorer

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 ⊢ M ∈ ℕ → -1 mod M = M − 1

Proof

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