Metamath Proof Explorer

Theorem submodneaddmod

Description: An integer minus B is not itself plus C modulo an integer greater than the sum of B and C . (Contributed by AV, 6-Sep-2025)

Ref Expression
Assertion submodneaddmod 
|- ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( 1 <_ ( B + C ) /\ ( B + C ) < N ) ) -> ( ( A + B ) mod N ) =/= ( ( A - C ) mod N ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( 1 <_ ( B + C ) /\ ( B + C ) < N ) ) -> N e. NN )
2 zaddcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A + B ) e. ZZ )
3 2 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A + B ) e. ZZ )
4 zsubcl 
 |-  ( ( A e. ZZ /\ C e. ZZ ) -> ( A - C ) e. ZZ )
5 4 3adant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A - C ) e. ZZ )
6 3 5 jca 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( A + B ) e. ZZ /\ ( A - C ) e. ZZ ) )
7 6 3ad2ant2 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( 1 <_ ( B + C ) /\ ( B + C ) < N ) ) -> ( ( A + B ) e. ZZ /\ ( A - C ) e. ZZ ) )
8 zcn 
 |-  ( A e. ZZ -> A e. CC )
9 8 3ad2ant1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> A e. CC )
10 9 3ad2ant2 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( 1 <_ ( B + C ) /\ ( B + C ) < N ) ) -> A e. CC )
11 zcn 
 |-  ( B e. ZZ -> B e. CC )
12 11 3ad2ant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> B e. CC )
13 12 3ad2ant2 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( 1 <_ ( B + C ) /\ ( B + C ) < N ) ) -> B e. CC )
14 zcn 
 |-  ( C e. ZZ -> C e. CC )
15 14 3ad2ant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> C e. CC )
16 15 3ad2ant2 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( 1 <_ ( B + C ) /\ ( B + C ) < N ) ) -> C e. CC )
17 10 13 16 pnncand 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( 1 <_ ( B + C ) /\ ( B + C ) < N ) ) -> ( ( A + B ) - ( A - C ) ) = ( B + C ) )
18 simpl3l 
 |-  ( ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( 1 <_ ( B + C ) /\ ( B + C ) < N ) ) /\ ( ( A + B ) - ( A - C ) ) = ( B + C ) ) -> 1 <_ ( B + C ) )
19 breq2 
 |-  ( ( ( A + B ) - ( A - C ) ) = ( B + C ) -> ( 1 <_ ( ( A + B ) - ( A - C ) ) <-> 1 <_ ( B + C ) ) )
20 19 adantl 
 |-  ( ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( 1 <_ ( B + C ) /\ ( B + C ) < N ) ) /\ ( ( A + B ) - ( A - C ) ) = ( B + C ) ) -> ( 1 <_ ( ( A + B ) - ( A - C ) ) <-> 1 <_ ( B + C ) ) )
21 18 20 mpbird 
 |-  ( ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( 1 <_ ( B + C ) /\ ( B + C ) < N ) ) /\ ( ( A + B ) - ( A - C ) ) = ( B + C ) ) -> 1 <_ ( ( A + B ) - ( A - C ) ) )
22 simpl3r 
 |-  ( ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( 1 <_ ( B + C ) /\ ( B + C ) < N ) ) /\ ( ( A + B ) - ( A - C ) ) = ( B + C ) ) -> ( B + C ) < N )
23 breq1 
 |-  ( ( ( A + B ) - ( A - C ) ) = ( B + C ) -> ( ( ( A + B ) - ( A - C ) ) < N <-> ( B + C ) < N ) )
24 23 adantl 
 |-  ( ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( 1 <_ ( B + C ) /\ ( B + C ) < N ) ) /\ ( ( A + B ) - ( A - C ) ) = ( B + C ) ) -> ( ( ( A + B ) - ( A - C ) ) < N <-> ( B + C ) < N ) )
25 22 24 mpbird 
 |-  ( ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( 1 <_ ( B + C ) /\ ( B + C ) < N ) ) /\ ( ( A + B ) - ( A - C ) ) = ( B + C ) ) -> ( ( A + B ) - ( A - C ) ) < N )
26 21 25 jca 
 |-  ( ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( 1 <_ ( B + C ) /\ ( B + C ) < N ) ) /\ ( ( A + B ) - ( A - C ) ) = ( B + C ) ) -> ( 1 <_ ( ( A + B ) - ( A - C ) ) /\ ( ( A + B ) - ( A - C ) ) < N ) )
27 17 26 mpdan 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( 1 <_ ( B + C ) /\ ( B + C ) < N ) ) -> ( 1 <_ ( ( A + B ) - ( A - C ) ) /\ ( ( A + B ) - ( A - C ) ) < N ) )
28 difltmodne 
 |-  ( ( N e. NN /\ ( ( A + B ) e. ZZ /\ ( A - C ) e. ZZ ) /\ ( 1 <_ ( ( A + B ) - ( A - C ) ) /\ ( ( A + B ) - ( A - C ) ) < N ) ) -> ( ( A + B ) mod N ) =/= ( ( A - C ) mod N ) )
29 1 7 27 28 syl3anc 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( 1 <_ ( B + C ) /\ ( B + C ) < N ) ) -> ( ( A + B ) mod N ) =/= ( ( A - C ) mod N ) )