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 {\mathbb{Z}}_{\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 {\mathbb{Z}}_{\ge 3}\to 3\le M$$
4	2 3	eqbrtrid	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to 2+1\le M$$
5		2z	$$⊢2\in \mathbb{Z}$$
6		eluzelz	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to M\in \mathbb{Z}$$
7		zltp1le	$$⊢\left(2\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\to \left(2<M\leftrightarrow 2+1\le M\right)$$
8	5 6 7	sylancr	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to \left(2<M\leftrightarrow 2+1\le M\right)$$
9	4 8	mpbird	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to 2<M$$
10	1 9	eqbrtrid	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to 1+1<M$$
11		1red	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to 1\in ℝ$$
12		eluzelre	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to M\in ℝ$$
13	11 11 12	ltaddsub2d	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to \left(1+1<M\leftrightarrow 1<M-1\right)$$
14	10 13	mpbid	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to 1<M-1$$
15		eluz3nn	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to M\in \mathbb{N}$$
16		m1modnnsub1	$$⊢M\in \mathbb{N}\to -1\mathrm{mod}M=M-1$$
17	15 16	syl	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to -1\mathrm{mod}M=M-1$$
18	14 17	breqtrrd	$$⊢M\in {\mathbb{Z}}_{\ge 3}\to 1<-1\mathrm{mod}M$$