Metamath Proof Explorer

Theorem m1modge3gt1

Description: Minus one modulo an integer greater than two is greater than one. (Contributed by AV, 14-Jul-2021)

Ref Expression
Assertion m1modge3gt1 
|- ( M e. ( ZZ>= ` 3 ) -> 1 < ( -u 1 mod M ) )

Proof

Step Hyp Ref Expression
1 1p1e2 
 |-  ( 1 + 1 ) = 2
2 2p1e3 
 |-  ( 2 + 1 ) = 3
3 eluzle 
 |-  ( M e. ( ZZ>= ` 3 ) -> 3 <_ M )
4 2 3 eqbrtrid 
 |-  ( M e. ( ZZ>= ` 3 ) -> ( 2 + 1 ) <_ M )
5 2z 
 |-  2 e. ZZ
6 eluzelz 
 |-  ( M e. ( ZZ>= ` 3 ) -> M e. ZZ )
7 zltp1le 
 |-  ( ( 2 e. ZZ /\ M e. ZZ ) -> ( 2 < M <-> ( 2 + 1 ) <_ M ) )
8 5 6 7 sylancr 
 |-  ( M e. ( ZZ>= ` 3 ) -> ( 2 < M <-> ( 2 + 1 ) <_ M ) )
9 4 8 mpbird 
 |-  ( M e. ( ZZ>= ` 3 ) -> 2 < M )
10 1 9 eqbrtrid 
 |-  ( M e. ( ZZ>= ` 3 ) -> ( 1 + 1 ) < M )
11 1red 
 |-  ( M e. ( ZZ>= ` 3 ) -> 1 e. RR )
12 eluzelre 
 |-  ( M e. ( ZZ>= ` 3 ) -> M e. RR )
13 11 11 12 ltaddsub2d 
 |-  ( M e. ( ZZ>= ` 3 ) -> ( ( 1 + 1 ) < M <-> 1 < ( M - 1 ) ) )
14 10 13 mpbid 
 |-  ( M e. ( ZZ>= ` 3 ) -> 1 < ( M - 1 ) )
15 eluzge3nn 
 |-  ( M e. ( ZZ>= ` 3 ) -> M e. NN )
16 m1modnnsub1 
 |-  ( M e. NN -> ( -u 1 mod M ) = ( M - 1 ) )
17 15 16 syl 
 |-  ( M e. ( ZZ>= ` 3 ) -> ( -u 1 mod M ) = ( M - 1 ) )
18 14 17 breqtrrd 
 |-  ( M e. ( ZZ>= ` 3 ) -> 1 < ( -u 1 mod M ) )