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 ( 𝑀 ∈ ℕ → ( - 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 ) )