Metamath Proof Explorer

Theorem congtr

Description: A wff of the form A || ( B - C ) is interpreted as a congruential equation. This is similar to ( B mod A ) = ( C mod A ) , but is defined such that behavior is regular for zero and negative values of A . To use this concept effectively, we need to show that congruential equations behave similarly to normal equations; first a transitivity law. Idea for the future: If there was a congruential equation symbol, it could incorporate type constraints, so that most of these would not need them. (Contributed by Stefan O'Rear, 1-Oct-2014)

Ref Expression
Assertion congtr 
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> A || ( B - D ) )

Proof

Step Hyp Ref Expression
1 simp1l 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> A e. ZZ )
2 simp1r 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> B e. ZZ )
3 simp2l 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> C e. ZZ )
4 2 3 zsubcld 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> ( B - C ) e. ZZ )
5 zsubcl 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> ( C - D ) e. ZZ )
6 5 3ad2ant2 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> ( C - D ) e. ZZ )
7 simp3 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> ( A || ( B - C ) /\ A || ( C - D ) ) )
8 dvds2add 
 |-  ( ( A e. ZZ /\ ( B - C ) e. ZZ /\ ( C - D ) e. ZZ ) -> ( ( A || ( B - C ) /\ A || ( C - D ) ) -> A || ( ( B - C ) + ( C - D ) ) ) )
9 8 imp 
 |-  ( ( ( A e. ZZ /\ ( B - C ) e. ZZ /\ ( C - D ) e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> A || ( ( B - C ) + ( C - D ) ) )
10 1 4 6 7 9 syl31anc 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> A || ( ( B - C ) + ( C - D ) ) )
11 zcn 
 |-  ( B e. ZZ -> B e. CC )
12 11 adantl 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> B e. CC )
13 12 3ad2ant1 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> B e. CC )
14 zcn 
 |-  ( C e. ZZ -> C e. CC )
15 14 adantr 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> C e. CC )
16 15 3ad2ant2 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> C e. CC )
17 zcn 
 |-  ( D e. ZZ -> D e. CC )
18 17 adantl 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> D e. CC )
19 18 3ad2ant2 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> D e. CC )
20 13 16 19 npncand 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> ( ( B - C ) + ( C - D ) ) = ( B - D ) )
21 10 20 breqtrd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> A || ( B - D ) )