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

Proof

Step Hyp Ref Expression
1 1re ⊢1∈ℝ
2 nnrp ⊢M∈ℕ→M∈ℝ+
3 negmod ⊢1∈ℝ∧M∈ℝ+→-1modM=M−1modM
4 1 2 3 sylancr ⊢M∈ℕ→-1modM=M−1modM
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−1modM=M−1
11 7 2 8 9 10 syl22anc ⊢M∈ℕ→M−1modM=M−1
12 4 11 eqtrd ⊢M∈ℕ→-1modM=M−1