Metamath Proof Explorer

Theorem minusmod5ne

Description: A nonnegative integer is not itself minus a positive integer less than 5 modulo 5. (Contributed by AV, 7-Sep-2025)

Ref Expression
Assertion minusmod5ne 
|- ( ( A e. ( 0 ..^ 5 ) /\ K e. ( 1 ..^ 5 ) ) -> ( ( A - K ) mod 5 ) =/= A )

Proof

Step Hyp Ref Expression
1 5nn 
 |-  5 e. NN
2 1 a1i 
 |-  ( ( A e. ( 0 ..^ 5 ) /\ K e. ( 1 ..^ 5 ) ) -> 5 e. NN )
3 elfzoelz 
 |-  ( A e. ( 0 ..^ 5 ) -> A e. ZZ )
4 3 adantr 
 |-  ( ( A e. ( 0 ..^ 5 ) /\ K e. ( 1 ..^ 5 ) ) -> A e. ZZ )
5 elfzoelz 
 |-  ( K e. ( 1 ..^ 5 ) -> K e. ZZ )
6 5 adantl 
 |-  ( ( A e. ( 0 ..^ 5 ) /\ K e. ( 1 ..^ 5 ) ) -> K e. ZZ )
7 4 6 zsubcld 
 |-  ( ( A e. ( 0 ..^ 5 ) /\ K e. ( 1 ..^ 5 ) ) -> ( A - K ) e. ZZ )
8 3 zcnd 
 |-  ( A e. ( 0 ..^ 5 ) -> A e. CC )
9 5 zcnd 
 |-  ( K e. ( 1 ..^ 5 ) -> K e. CC )
10 nncan 
 |-  ( ( A e. CC /\ K e. CC ) -> ( A - ( A - K ) ) = K )
11 8 9 10 syl2an 
 |-  ( ( A e. ( 0 ..^ 5 ) /\ K e. ( 1 ..^ 5 ) ) -> ( A - ( A - K ) ) = K )
12 elfzo1 
 |-  ( K e. ( 1 ..^ 5 ) <-> ( K e. NN /\ 5 e. NN /\ K < 5 ) )
13 nnge1 
 |-  ( K e. NN -> 1 <_ K )
14 13 anim1i 
 |-  ( ( K e. NN /\ K < 5 ) -> ( 1 <_ K /\ K < 5 ) )
15 14 3adant2 
 |-  ( ( K e. NN /\ 5 e. NN /\ K < 5 ) -> ( 1 <_ K /\ K < 5 ) )
16 12 15 sylbi 
 |-  ( K e. ( 1 ..^ 5 ) -> ( 1 <_ K /\ K < 5 ) )
17 16 adantl 
 |-  ( ( A e. ( 0 ..^ 5 ) /\ K e. ( 1 ..^ 5 ) ) -> ( 1 <_ K /\ K < 5 ) )
18 breq2 
 |-  ( ( A - ( A - K ) ) = K -> ( 1 <_ ( A - ( A - K ) ) <-> 1 <_ K ) )
19 breq1 
 |-  ( ( A - ( A - K ) ) = K -> ( ( A - ( A - K ) ) < 5 <-> K < 5 ) )
20 18 19 anbi12d 
 |-  ( ( A - ( A - K ) ) = K -> ( ( 1 <_ ( A - ( A - K ) ) /\ ( A - ( A - K ) ) < 5 ) <-> ( 1 <_ K /\ K < 5 ) ) )
21 17 20 syl5ibrcom 
 |-  ( ( A e. ( 0 ..^ 5 ) /\ K e. ( 1 ..^ 5 ) ) -> ( ( A - ( A - K ) ) = K -> ( 1 <_ ( A - ( A - K ) ) /\ ( A - ( A - K ) ) < 5 ) ) )
22 11 21 mpd 
 |-  ( ( A e. ( 0 ..^ 5 ) /\ K e. ( 1 ..^ 5 ) ) -> ( 1 <_ ( A - ( A - K ) ) /\ ( A - ( A - K ) ) < 5 ) )
23 difltmodne 
 |-  ( ( 5 e. NN /\ ( A e. ZZ /\ ( A - K ) e. ZZ ) /\ ( 1 <_ ( A - ( A - K ) ) /\ ( A - ( A - K ) ) < 5 ) ) -> ( A mod 5 ) =/= ( ( A - K ) mod 5 ) )
24 2 4 7 22 23 syl121anc 
 |-  ( ( A e. ( 0 ..^ 5 ) /\ K e. ( 1 ..^ 5 ) ) -> ( A mod 5 ) =/= ( ( A - K ) mod 5 ) )
25 24 necomd 
 |-  ( ( A e. ( 0 ..^ 5 ) /\ K e. ( 1 ..^ 5 ) ) -> ( ( A - K ) mod 5 ) =/= ( A mod 5 ) )
26 zmodidfzoimp 
 |-  ( A e. ( 0 ..^ 5 ) -> ( A mod 5 ) = A )
27 26 adantr 
 |-  ( ( A e. ( 0 ..^ 5 ) /\ K e. ( 1 ..^ 5 ) ) -> ( A mod 5 ) = A )
28 25 27 neeqtrd 
 |-  ( ( A e. ( 0 ..^ 5 ) /\ K e. ( 1 ..^ 5 ) ) -> ( ( A - K ) mod 5 ) =/= A )