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 e. NN -> ( -u 1 mod M ) = ( M - 1 ) )

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 nnrp 
 |-  ( M e. NN -> M e. RR+ )
3 negmod 
 |-  ( ( 1 e. RR /\ M e. RR+ ) -> ( -u 1 mod M ) = ( ( M - 1 ) mod M ) )
4 1 2 3 sylancr 
 |-  ( M e. NN -> ( -u 1 mod M ) = ( ( M - 1 ) mod M ) )
5 nnre 
 |-  ( M e. NN -> M e. RR )
6 peano2rem 
 |-  ( M e. RR -> ( M - 1 ) e. RR )
7 5 6 syl 
 |-  ( M e. NN -> ( M - 1 ) e. RR )
8 nnm1ge0 
 |-  ( M e. NN -> 0 <_ ( M - 1 ) )
9 5 ltm1d 
 |-  ( M e. NN -> ( M - 1 ) < M )
10 modid 
 |-  ( ( ( ( M - 1 ) e. RR /\ M e. RR+ ) /\ ( 0 <_ ( M - 1 ) /\ ( M - 1 ) < M ) ) -> ( ( M - 1 ) mod M ) = ( M - 1 ) )
11 7 2 8 9 10 syl22anc 
 |-  ( M e. NN -> ( ( M - 1 ) mod M ) = ( M - 1 ) )
12 4 11 eqtrd 
 |-  ( M e. NN -> ( -u 1 mod M ) = ( M - 1 ) )