Metamath Proof Explorer

Theorem m1modne

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

Ref Expression
Assertion m1modne 
|- ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) -> ( ( A - 1 ) mod N ) =/= A )

Proof

Step Hyp Ref Expression
1 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
2 1 adantr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) -> N e. NN )
3 elfzoelz 
 |-  ( A e. ( 0 ..^ N ) -> A e. ZZ )
4 1zzd 
 |-  ( A e. ( 0 ..^ N ) -> 1 e. ZZ )
5 3 4 zsubcld 
 |-  ( A e. ( 0 ..^ N ) -> ( A - 1 ) e. ZZ )
6 3 5 jca 
 |-  ( A e. ( 0 ..^ N ) -> ( A e. ZZ /\ ( A - 1 ) e. ZZ ) )
7 6 adantl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) -> ( A e. ZZ /\ ( A - 1 ) e. ZZ ) )
8 3 zcnd 
 |-  ( A e. ( 0 ..^ N ) -> A e. CC )
9 8 adantl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) -> A e. CC )
10 1cnd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) -> 1 e. CC )
11 9 10 nncand 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) -> ( A - ( A - 1 ) ) = 1 )
12 1le1 
 |-  1 <_ 1
13 breq2 
 |-  ( ( A - ( A - 1 ) ) = 1 -> ( 1 <_ ( A - ( A - 1 ) ) <-> 1 <_ 1 ) )
14 13 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) /\ ( A - ( A - 1 ) ) = 1 ) -> ( 1 <_ ( A - ( A - 1 ) ) <-> 1 <_ 1 ) )
15 12 14 mpbiri 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) /\ ( A - ( A - 1 ) ) = 1 ) -> 1 <_ ( A - ( A - 1 ) ) )
16 eluz2gt1 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 < N )
17 16 adantr 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) -> 1 < N )
18 17 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) /\ ( A - ( A - 1 ) ) = 1 ) -> 1 < N )
19 breq1 
 |-  ( ( A - ( A - 1 ) ) = 1 -> ( ( A - ( A - 1 ) ) < N <-> 1 < N ) )
20 19 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) /\ ( A - ( A - 1 ) ) = 1 ) -> ( ( A - ( A - 1 ) ) < N <-> 1 < N ) )
21 18 20 mpbird 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) /\ ( A - ( A - 1 ) ) = 1 ) -> ( A - ( A - 1 ) ) < N )
22 15 21 jca 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) /\ ( A - ( A - 1 ) ) = 1 ) -> ( 1 <_ ( A - ( A - 1 ) ) /\ ( A - ( A - 1 ) ) < N ) )
23 11 22 mpdan 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) -> ( 1 <_ ( A - ( A - 1 ) ) /\ ( A - ( A - 1 ) ) < N ) )
24 difltmodne 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ ( A - 1 ) e. ZZ ) /\ ( 1 <_ ( A - ( A - 1 ) ) /\ ( A - ( A - 1 ) ) < N ) ) -> ( A mod N ) =/= ( ( A - 1 ) mod N ) )
25 2 7 23 24 syl3anc 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) -> ( A mod N ) =/= ( ( A - 1 ) mod N ) )
26 25 necomd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) -> ( ( A - 1 ) mod N ) =/= ( A mod N ) )
27 zmodidfzoimp 
 |-  ( A e. ( 0 ..^ N ) -> ( A mod N ) = A )
28 27 adantl 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) -> ( A mod N ) = A )
29 26 28 neeqtrd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ( 0 ..^ N ) ) -> ( ( A - 1 ) mod N ) =/= A )