Metamath Proof Explorer

Theorem minusmodnep2tmod

Description: A nonnegative integer minus a positive integer 1 or 2 is not itself plus 2 times the positive integer modulo 5. (Contributed by AV, 8-Sep-2025)

Ref Expression
Assertion minusmodnep2tmod 
|- ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> ( ( A - B ) mod 5 ) =/= ( ( A + ( 2 x. B ) ) mod 5 ) )

Proof

Step Hyp Ref Expression
1 elpri 
 |-  ( B e. { 1 , 2 } -> ( B = 1 \/ B = 2 ) )
2 5ndvds3 
 |-  -. 5 || 3
3 oveq2 
 |-  ( B = 1 -> ( 3 x. B ) = ( 3 x. 1 ) )
4 3t1e3 
 |-  ( 3 x. 1 ) = 3
5 3 4 eqtrdi 
 |-  ( B = 1 -> ( 3 x. B ) = 3 )
6 5 breq2d 
 |-  ( B = 1 -> ( 5 || ( 3 x. B ) <-> 5 || 3 ) )
7 2 6 mtbiri 
 |-  ( B = 1 -> -. 5 || ( 3 x. B ) )
8 5ndvds6 
 |-  -. 5 || 6
9 oveq2 
 |-  ( B = 2 -> ( 3 x. B ) = ( 3 x. 2 ) )
10 3t2e6 
 |-  ( 3 x. 2 ) = 6
11 9 10 eqtrdi 
 |-  ( B = 2 -> ( 3 x. B ) = 6 )
12 11 breq2d 
 |-  ( B = 2 -> ( 5 || ( 3 x. B ) <-> 5 || 6 ) )
13 8 12 mtbiri 
 |-  ( B = 2 -> -. 5 || ( 3 x. B ) )
14 7 13 jaoi 
 |-  ( ( B = 1 \/ B = 2 ) -> -. 5 || ( 3 x. B ) )
15 1 14 syl 
 |-  ( B e. { 1 , 2 } -> -. 5 || ( 3 x. B ) )
16 fzo13pr 
 |-  ( 1 ..^ 3 ) = { 1 , 2 }
17 15 16 eleq2s 
 |-  ( B e. ( 1 ..^ 3 ) -> -. 5 || ( 3 x. B ) )
18 17 adantl 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> -. 5 || ( 3 x. B ) )
19 5nn 
 |-  5 e. NN
20 19 a1i 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> 5 e. NN )
21 simpl 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> A e. ZZ )
22 2z 
 |-  2 e. ZZ
23 22 a1i 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> 2 e. ZZ )
24 elfzoelz 
 |-  ( B e. ( 1 ..^ 3 ) -> B e. ZZ )
25 24 adantl 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> B e. ZZ )
26 23 25 zmulcld 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> ( 2 x. B ) e. ZZ )
27 submodaddmod 
 |-  ( ( 5 e. NN /\ ( A e. ZZ /\ ( 2 x. B ) e. ZZ /\ B e. ZZ ) ) -> ( ( ( A + ( 2 x. B ) ) mod 5 ) = ( ( A - B ) mod 5 ) <-> ( ( A + ( ( 2 x. B ) + B ) ) mod 5 ) = ( A mod 5 ) ) )
28 20 21 26 25 27 syl13anc 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> ( ( ( A + ( 2 x. B ) ) mod 5 ) = ( ( A - B ) mod 5 ) <-> ( ( A + ( ( 2 x. B ) + B ) ) mod 5 ) = ( A mod 5 ) ) )
29 2cnd 
 |-  ( B e. ( 1 ..^ 3 ) -> 2 e. CC )
30 24 zcnd 
 |-  ( B e. ( 1 ..^ 3 ) -> B e. CC )
31 29 30 adddirp1d 
 |-  ( B e. ( 1 ..^ 3 ) -> ( ( 2 + 1 ) x. B ) = ( ( 2 x. B ) + B ) )
32 31 eqcomd 
 |-  ( B e. ( 1 ..^ 3 ) -> ( ( 2 x. B ) + B ) = ( ( 2 + 1 ) x. B ) )
33 32 adantl 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> ( ( 2 x. B ) + B ) = ( ( 2 + 1 ) x. B ) )
34 2p1e3 
 |-  ( 2 + 1 ) = 3
35 34 oveq1i 
 |-  ( ( 2 + 1 ) x. B ) = ( 3 x. B )
36 33 35 eqtrdi 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> ( ( 2 x. B ) + B ) = ( 3 x. B ) )
37 36 oveq2d 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> ( A + ( ( 2 x. B ) + B ) ) = ( A + ( 3 x. B ) ) )
38 37 oveq1d 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> ( ( A + ( ( 2 x. B ) + B ) ) mod 5 ) = ( ( A + ( 3 x. B ) ) mod 5 ) )
39 38 eqeq1d 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> ( ( ( A + ( ( 2 x. B ) + B ) ) mod 5 ) = ( A mod 5 ) <-> ( ( A + ( 3 x. B ) ) mod 5 ) = ( A mod 5 ) ) )
40 28 39 bitrd 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> ( ( ( A + ( 2 x. B ) ) mod 5 ) = ( ( A - B ) mod 5 ) <-> ( ( A + ( 3 x. B ) ) mod 5 ) = ( A mod 5 ) ) )
41 eqcom 
 |-  ( ( ( A - B ) mod 5 ) = ( ( A + ( 2 x. B ) ) mod 5 ) <-> ( ( A + ( 2 x. B ) ) mod 5 ) = ( ( A - B ) mod 5 ) )
42 41 a1i 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> ( ( ( A - B ) mod 5 ) = ( ( A + ( 2 x. B ) ) mod 5 ) <-> ( ( A + ( 2 x. B ) ) mod 5 ) = ( ( A - B ) mod 5 ) ) )
43 3z 
 |-  3 e. ZZ
44 43 a1i 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> 3 e. ZZ )
45 addmulmodb 
 |-  ( ( 5 e. NN /\ ( A e. ZZ /\ 3 e. ZZ /\ B e. ZZ ) ) -> ( 5 || ( 3 x. B ) <-> ( ( A + ( 3 x. B ) ) mod 5 ) = ( A mod 5 ) ) )
46 20 21 44 25 45 syl13anc 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> ( 5 || ( 3 x. B ) <-> ( ( A + ( 3 x. B ) ) mod 5 ) = ( A mod 5 ) ) )
47 40 42 46 3bitr4d 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> ( ( ( A - B ) mod 5 ) = ( ( A + ( 2 x. B ) ) mod 5 ) <-> 5 || ( 3 x. B ) ) )
48 18 47 mtbird 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> -. ( ( A - B ) mod 5 ) = ( ( A + ( 2 x. B ) ) mod 5 ) )
49 48 neqned 
 |-  ( ( A e. ZZ /\ B e. ( 1 ..^ 3 ) ) -> ( ( A - B ) mod 5 ) =/= ( ( A + ( 2 x. B ) ) mod 5 ) )