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 ( 𝑀 ∈ ( ℤ≥ ‘ 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 eluz3nn ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → 𝑀 ∈ ℕ )
16 m1modnnsub1 ⊢ ( 𝑀 ∈ ℕ → ( - 1 mod 𝑀 ) = ( 𝑀 − 1 ) )
17 15 16 syl ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → ( - 1 mod 𝑀 ) = ( 𝑀 − 1 ) )
18 14 17 breqtrrd ⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 3 ) → 1 < ( - 1 mod 𝑀 ) )