Metamath Proof Explorer

Theorem submodaddmod

Description: Subtraction and addition modulo a positive integer. (Contributed by AV, 7-Sep-2025)

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

Proof

Step Hyp Ref Expression
1 zcn 
 |-  ( A e. ZZ -> A e. CC )
2 1 3ad2ant1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> A e. CC )
3 2 adantl 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> A e. CC )
4 zcn 
 |-  ( B e. ZZ -> B e. CC )
5 4 3ad2ant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> B e. CC )
6 5 adantl 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> B e. CC )
7 zcn 
 |-  ( C e. ZZ -> C e. CC )
8 7 3ad2ant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> C e. CC )
9 8 adantl 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> C e. CC )
10 3 6 9 pnncand 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( A + B ) - ( A - C ) ) = ( B + C ) )
11 zaddcl 
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> ( B + C ) e. ZZ )
12 11 zcnd 
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> ( B + C ) e. CC )
13 12 3adant1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( B + C ) e. CC )
14 13 adantl 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( B + C ) e. CC )
15 3 14 pncan2d 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( A + ( B + C ) ) - A ) = ( B + C ) )
16 10 15 eqtr4d 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( A + B ) - ( A - C ) ) = ( ( A + ( B + C ) ) - A ) )
17 16 breq2d 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( N || ( ( A + B ) - ( A - C ) ) <-> N || ( ( A + ( B + C ) ) - A ) ) )
18 simpl 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> N e. NN )
19 zaddcl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( A + B ) e. ZZ )
20 19 3adant3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A + B ) e. ZZ )
21 20 adantl 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( A + B ) e. ZZ )
22 zsubcl 
 |-  ( ( A e. ZZ /\ C e. ZZ ) -> ( A - C ) e. ZZ )
23 22 3adant2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A - C ) e. ZZ )
24 23 adantl 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( A - C ) e. ZZ )
25 moddvds 
 |-  ( ( N e. NN /\ ( A + B ) e. ZZ /\ ( A - C ) e. ZZ ) -> ( ( ( A + B ) mod N ) = ( ( A - C ) mod N ) <-> N || ( ( A + B ) - ( A - C ) ) ) )
26 18 21 24 25 syl3anc 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( ( A + B ) mod N ) = ( ( A - C ) mod N ) <-> N || ( ( A + B ) - ( A - C ) ) ) )
27 simp1 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> A e. ZZ )
28 simp2 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> B e. ZZ )
29 simp3 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> C e. ZZ )
30 28 29 zaddcld 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( B + C ) e. ZZ )
31 27 30 zaddcld 
 |-  ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( A + ( B + C ) ) e. ZZ )
32 31 adantl 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( A + ( B + C ) ) e. ZZ )
33 simpr1 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> A e. ZZ )
34 moddvds 
 |-  ( ( N e. NN /\ ( A + ( B + C ) ) e. ZZ /\ A e. ZZ ) -> ( ( ( A + ( B + C ) ) mod N ) = ( A mod N ) <-> N || ( ( A + ( B + C ) ) - A ) ) )
35 18 32 33 34 syl3anc 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( ( A + ( B + C ) ) mod N ) = ( A mod N ) <-> N || ( ( A + ( B + C ) ) - A ) ) )
36 17 26 35 3bitr4d 
 |-  ( ( N e. NN /\ ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) ) -> ( ( ( A + B ) mod N ) = ( ( A - C ) mod N ) <-> ( ( A + ( B + C ) ) mod N ) = ( A mod N ) ) )