Metamath Proof Explorer

Theorem zplusmodne

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

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

Proof

Step Hyp Ref Expression
1 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
2 1 3ad2ant1 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ K e. ( 1 ..^ N ) ) -> N e. NN )
3 simp2 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ K e. ( 1 ..^ N ) ) -> A e. ZZ )
4 elfzoelz 
 |-  ( K e. ( 1 ..^ N ) -> K e. ZZ )
5 4 3ad2ant3 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ K e. ( 1 ..^ N ) ) -> K e. ZZ )
6 3 5 zaddcld 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ K e. ( 1 ..^ N ) ) -> ( A + K ) e. ZZ )
7 3 zcnd 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ K e. ( 1 ..^ N ) ) -> A e. CC )
8 4 zcnd 
 |-  ( K e. ( 1 ..^ N ) -> K e. CC )
9 8 3ad2ant3 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ K e. ( 1 ..^ N ) ) -> K e. CC )
10 7 9 pncan2d 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ K e. ( 1 ..^ N ) ) -> ( ( A + K ) - A ) = K )
11 elfzo1 
 |-  ( K e. ( 1 ..^ N ) <-> ( K e. NN /\ N e. NN /\ K < N ) )
12 nnge1 
 |-  ( K e. NN -> 1 <_ K )
13 12 anim1i 
 |-  ( ( K e. NN /\ K < N ) -> ( 1 <_ K /\ K < N ) )
14 13 3adant2 
 |-  ( ( K e. NN /\ N e. NN /\ K < N ) -> ( 1 <_ K /\ K < N ) )
15 11 14 sylbi 
 |-  ( K e. ( 1 ..^ N ) -> ( 1 <_ K /\ K < N ) )
16 15 3ad2ant3 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ K e. ( 1 ..^ N ) ) -> ( 1 <_ K /\ K < N ) )
17 16 adantr 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ K e. ( 1 ..^ N ) ) /\ ( ( A + K ) - A ) = K ) -> ( 1 <_ K /\ K < N ) )
18 breq2 
 |-  ( ( ( A + K ) - A ) = K -> ( 1 <_ ( ( A + K ) - A ) <-> 1 <_ K ) )
19 18 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ K e. ( 1 ..^ N ) ) /\ ( ( A + K ) - A ) = K ) -> ( 1 <_ ( ( A + K ) - A ) <-> 1 <_ K ) )
20 breq1 
 |-  ( ( ( A + K ) - A ) = K -> ( ( ( A + K ) - A ) < N <-> K < N ) )
21 20 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ K e. ( 1 ..^ N ) ) /\ ( ( A + K ) - A ) = K ) -> ( ( ( A + K ) - A ) < N <-> K < N ) )
22 19 21 anbi12d 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ K e. ( 1 ..^ N ) ) /\ ( ( A + K ) - A ) = K ) -> ( ( 1 <_ ( ( A + K ) - A ) /\ ( ( A + K ) - A ) < N ) <-> ( 1 <_ K /\ K < N ) ) )
23 17 22 mpbird 
 |-  ( ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ K e. ( 1 ..^ N ) ) /\ ( ( A + K ) - A ) = K ) -> ( 1 <_ ( ( A + K ) - A ) /\ ( ( A + K ) - A ) < N ) )
24 10 23 mpdan 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ K e. ( 1 ..^ N ) ) -> ( 1 <_ ( ( A + K ) - A ) /\ ( ( A + K ) - A ) < N ) )
25 difltmodne 
 |-  ( ( N e. NN /\ ( ( A + K ) e. ZZ /\ A e. ZZ ) /\ ( 1 <_ ( ( A + K ) - A ) /\ ( ( A + K ) - A ) < N ) ) -> ( ( A + K ) mod N ) =/= ( A mod N ) )
26 2 6 3 24 25 syl121anc 
 |-  ( ( N e. ( ZZ>= ` 2 ) /\ A e. ZZ /\ K e. ( 1 ..^ N ) ) -> ( ( A + K ) mod N ) =/= ( A mod N ) )