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 ) )