This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ ℤ ≥ 3 → 1 < -1 mod M

Proof

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