Metamath Proof Explorer

Theorem m1modnep2mod

Description: A nonnegative integer minus 1 is not itself plus 2 modulo an integer greater than 3 and the nonnegative integer. (Contributed by AV, 6-Sep-2025)

Ref Expression
Assertion m1modnep2mod 
|- ( ( N e. ( ZZ>= ` 4 ) /\ A e. ZZ ) -> ( ( A - 1 ) mod N ) =/= ( ( A + 2 ) mod N ) )

Proof

Step Hyp Ref Expression
1 eluz4nn 
 |-  ( N e. ( ZZ>= ` 4 ) -> N e. NN )
2 1 adantr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ A e. ZZ ) -> N e. NN )
3 simpr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ A e. ZZ ) -> A e. ZZ )
4 2z 
 |-  2 e. ZZ
5 4 a1i 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ A e. ZZ ) -> 2 e. ZZ )
6 1zzd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ A e. ZZ ) -> 1 e. ZZ )
7 1le3 
 |-  1 <_ 3
8 2p1e3 
 |-  ( 2 + 1 ) = 3
9 7 8 breqtrri 
 |-  1 <_ ( 2 + 1 )
10 9 a1i 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ A e. ZZ ) -> 1 <_ ( 2 + 1 ) )
11 eluz2 
 |-  ( N e. ( ZZ>= ` 4 ) <-> ( 4 e. ZZ /\ N e. ZZ /\ 4 <_ N ) )
12 df-4 
 |-  4 = ( 3 + 1 )
13 12 breq1i 
 |-  ( 4 <_ N <-> ( 3 + 1 ) <_ N )
14 3z 
 |-  3 e. ZZ
15 14 a1i 
 |-  ( 4 e. ZZ -> 3 e. ZZ )
16 zltp1le 
 |-  ( ( 3 e. ZZ /\ N e. ZZ ) -> ( 3 < N <-> ( 3 + 1 ) <_ N ) )
17 15 16 sylan 
 |-  ( ( 4 e. ZZ /\ N e. ZZ ) -> ( 3 < N <-> ( 3 + 1 ) <_ N ) )
18 17 biimprd 
 |-  ( ( 4 e. ZZ /\ N e. ZZ ) -> ( ( 3 + 1 ) <_ N -> 3 < N ) )
19 13 18 biimtrid 
 |-  ( ( 4 e. ZZ /\ N e. ZZ ) -> ( 4 <_ N -> 3 < N ) )
20 19 3impia 
 |-  ( ( 4 e. ZZ /\ N e. ZZ /\ 4 <_ N ) -> 3 < N )
21 11 20 sylbi 
 |-  ( N e. ( ZZ>= ` 4 ) -> 3 < N )
22 8 21 eqbrtrid 
 |-  ( N e. ( ZZ>= ` 4 ) -> ( 2 + 1 ) < N )
23 22 adantr 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ A e. ZZ ) -> ( 2 + 1 ) < N )
24 submodneaddmod 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ 2 e. ZZ /\ 1 e. ZZ ) /\ ( 1 <_ ( 2 + 1 ) /\ ( 2 + 1 ) < N ) ) -> ( ( A + 2 ) mod N ) =/= ( ( A - 1 ) mod N ) )
25 2 3 5 6 10 23 24 syl132anc 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ A e. ZZ ) -> ( ( A + 2 ) mod N ) =/= ( ( A - 1 ) mod N ) )
26 25 necomd 
 |-  ( ( N e. ( ZZ>= ` 4 ) /\ A e. ZZ ) -> ( ( A - 1 ) mod N ) =/= ( ( A + 2 ) mod N ) )