# 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}\in {ℤ}_{\ge 3}\to 1<-1\mathrm{mod}{M}$

### Proof

Step Hyp Ref Expression
1 1p1e2 ${⊢}1+1=2$
2 2p1e3 ${⊢}2+1=3$
3 eluzle ${⊢}{M}\in {ℤ}_{\ge 3}\to 3\le {M}$
4 2 3 eqbrtrid ${⊢}{M}\in {ℤ}_{\ge 3}\to 2+1\le {M}$
5 2z ${⊢}2\in ℤ$
6 eluzelz ${⊢}{M}\in {ℤ}_{\ge 3}\to {M}\in ℤ$
7 zltp1le ${⊢}\left(2\in ℤ\wedge {M}\in ℤ\right)\to \left(2<{M}↔2+1\le {M}\right)$
8 5 6 7 sylancr ${⊢}{M}\in {ℤ}_{\ge 3}\to \left(2<{M}↔2+1\le {M}\right)$
9 4 8 mpbird ${⊢}{M}\in {ℤ}_{\ge 3}\to 2<{M}$
10 1 9 eqbrtrid ${⊢}{M}\in {ℤ}_{\ge 3}\to 1+1<{M}$
11 1red ${⊢}{M}\in {ℤ}_{\ge 3}\to 1\in ℝ$
12 eluzelre ${⊢}{M}\in {ℤ}_{\ge 3}\to {M}\in ℝ$
13 11 11 12 ltaddsub2d ${⊢}{M}\in {ℤ}_{\ge 3}\to \left(1+1<{M}↔1<{M}-1\right)$
14 10 13 mpbid ${⊢}{M}\in {ℤ}_{\ge 3}\to 1<{M}-1$
15 eluzge3nn ${⊢}{M}\in {ℤ}_{\ge 3}\to {M}\in ℕ$
16 m1modnnsub1 ${⊢}{M}\in ℕ\to -1\mathrm{mod}{M}={M}-1$
17 15 16 syl ${⊢}{M}\in {ℤ}_{\ge 3}\to -1\mathrm{mod}{M}={M}-1$
18 14 17 breqtrrd ${⊢}{M}\in {ℤ}_{\ge 3}\to 1<-1\mathrm{mod}{M}$