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}\in ℕ\to -1\mathrm{mod}{M}={M}-1$

Proof

Step Hyp Ref Expression
1 1re ${⊢}1\in ℝ$
2 nnrp ${⊢}{M}\in ℕ\to {M}\in {ℝ}^{+}$
3 negmod ${⊢}\left(1\in ℝ\wedge {M}\in {ℝ}^{+}\right)\to -1\mathrm{mod}{M}=\left({M}-1\right)\mathrm{mod}{M}$
4 1 2 3 sylancr ${⊢}{M}\in ℕ\to -1\mathrm{mod}{M}=\left({M}-1\right)\mathrm{mod}{M}$
5 nnre ${⊢}{M}\in ℕ\to {M}\in ℝ$
6 peano2rem ${⊢}{M}\in ℝ\to {M}-1\in ℝ$
7 5 6 syl ${⊢}{M}\in ℕ\to {M}-1\in ℝ$
8 nnm1ge0 ${⊢}{M}\in ℕ\to 0\le {M}-1$
9 5 ltm1d ${⊢}{M}\in ℕ\to {M}-1<{M}$
10 modid ${⊢}\left(\left({M}-1\in ℝ\wedge {M}\in {ℝ}^{+}\right)\wedge \left(0\le {M}-1\wedge {M}-1<{M}\right)\right)\to \left({M}-1\right)\mathrm{mod}{M}={M}-1$
11 7 2 8 9 10 syl22anc ${⊢}{M}\in ℕ\to \left({M}-1\right)\mathrm{mod}{M}={M}-1$
12 4 11 eqtrd ${⊢}{M}\in ℕ\to -1\mathrm{mod}{M}={M}-1$