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	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → 1 < ( - 1 mod 𝑀 ) )

Proof

Step	Hyp	Ref	Expression
1		1p1e2	⊢ ( 1 + 1 ) = 2
2		2p1e3	⊢ ( 2 + 1 ) = 3
3		eluzle	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → 3 ≤ 𝑀 )
4	2 3	eqbrtrid	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → ( 2 + 1 ) ≤ 𝑀 )
5		2z	⊢ 2 ∈ ℤ
6		eluzelz	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → 𝑀 ∈ ℤ )
7		zltp1le	⊢ ( ( 2 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 2 < 𝑀 ↔ ( 2 + 1 ) ≤ 𝑀 ) )
8	5 6 7	sylancr	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → ( 2 < 𝑀 ↔ ( 2 + 1 ) ≤ 𝑀 ) )
9	4 8	mpbird	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → 2 < 𝑀 )
10	1 9	eqbrtrid	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → ( 1 + 1 ) < 𝑀 )
11		1red	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → 1 ∈ ℝ )
12		eluzelre	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → 𝑀 ∈ ℝ )
13	11 11 12	ltaddsub2d	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → ( ( 1 + 1 ) < 𝑀 ↔ 1 < ( 𝑀 − 1 ) ) )
14	10 13	mpbid	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → 1 < ( 𝑀 − 1 ) )
15		eluzge3nn	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → 𝑀 ∈ ℕ )
16		m1modnnsub1	⊢ ( 𝑀 ∈ ℕ → ( - 1 mod 𝑀 ) = ( 𝑀 − 1 ) )
17	15 16	syl	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → ( - 1 mod 𝑀 ) = ( 𝑀 − 1 ) )
18	14 17	breqtrrd	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → 1 < ( - 1 mod 𝑀 ) )