Metamath Proof Explorer

Theorem acongtr

Description: Transitivity of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014)

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

Proof

Step Hyp Ref Expression
1 congtr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> A || ( B - D ) )
2 1 3expa 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> A || ( B - D ) )
3 2 orcd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> ( A || ( B - D ) \/ A || ( B - -u D ) ) )
4 3 ex 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( A || ( B - C ) /\ A || ( C - D ) ) -> ( A || ( B - D ) \/ A || ( B - -u D ) ) ) )
5 simpll 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - -u C ) /\ A || ( C - D ) ) ) -> ( A e. ZZ /\ B e. ZZ ) )
6 znegcl 
 |-  ( C e. ZZ -> -u C e. ZZ )
7 znegcl 
 |-  ( D e. ZZ -> -u D e. ZZ )
8 6 7 anim12i 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> ( -u C e. ZZ /\ -u D e. ZZ ) )
9 8 ad2antlr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - -u C ) /\ A || ( C - D ) ) ) -> ( -u C e. ZZ /\ -u D e. ZZ ) )
10 simplll 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ A || ( C - D ) ) -> A e. ZZ )
11 simplrl 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ A || ( C - D ) ) -> C e. ZZ )
12 simplrr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ A || ( C - D ) ) -> D e. ZZ )
13 simpr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ A || ( C - D ) ) -> A || ( C - D ) )
14 congsym 
 |-  ( ( ( A e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ A || ( C - D ) ) ) -> A || ( D - C ) )
15 10 11 12 13 14 syl22anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ A || ( C - D ) ) -> A || ( D - C ) )
16 15 ex 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( A || ( C - D ) -> A || ( D - C ) ) )
17 zcn 
 |-  ( C e. ZZ -> C e. CC )
18 17 adantr 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> C e. CC )
19 zcn 
 |-  ( D e. ZZ -> D e. CC )
20 19 adantl 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> D e. CC )
21 18 20 neg2subd 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> ( -u C - -u D ) = ( D - C ) )
22 21 adantl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( -u C - -u D ) = ( D - C ) )
23 22 eqcomd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( D - C ) = ( -u C - -u D ) )
24 23 breq2d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( A || ( D - C ) <-> A || ( -u C - -u D ) ) )
25 16 24 sylibd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( A || ( C - D ) -> A || ( -u C - -u D ) ) )
26 25 anim2d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( A || ( B - -u C ) /\ A || ( C - D ) ) -> ( A || ( B - -u C ) /\ A || ( -u C - -u D ) ) ) )
27 26 imp 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - -u C ) /\ A || ( C - D ) ) ) -> ( A || ( B - -u C ) /\ A || ( -u C - -u D ) ) )
28 congtr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( -u C e. ZZ /\ -u D e. ZZ ) /\ ( A || ( B - -u C ) /\ A || ( -u C - -u D ) ) ) -> A || ( B - -u D ) )
29 5 9 27 28 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - -u C ) /\ A || ( C - D ) ) ) -> A || ( B - -u D ) )
30 29 olcd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - -u C ) /\ A || ( C - D ) ) ) -> ( A || ( B - D ) \/ A || ( B - -u D ) ) )
31 30 ex 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( A || ( B - -u C ) /\ A || ( C - D ) ) -> ( A || ( B - D ) \/ A || ( B - -u D ) ) ) )
32 simpll 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - C ) /\ A || ( C - -u D ) ) ) -> ( A e. ZZ /\ B e. ZZ ) )
33 7 anim2i 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> ( C e. ZZ /\ -u D e. ZZ ) )
34 33 ad2antlr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - C ) /\ A || ( C - -u D ) ) ) -> ( C e. ZZ /\ -u D e. ZZ ) )
35 simpr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - C ) /\ A || ( C - -u D ) ) ) -> ( A || ( B - C ) /\ A || ( C - -u D ) ) )
36 congtr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ -u D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - -u D ) ) ) -> A || ( B - -u D ) )
37 32 34 35 36 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - C ) /\ A || ( C - -u D ) ) ) -> A || ( B - -u D ) )
38 37 olcd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - C ) /\ A || ( C - -u D ) ) ) -> ( A || ( B - D ) \/ A || ( B - -u D ) ) )
39 38 ex 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( A || ( B - C ) /\ A || ( C - -u D ) ) -> ( A || ( B - D ) \/ A || ( B - -u D ) ) ) )
40 simpll 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - -u C ) /\ A || ( C - -u D ) ) ) -> ( A e. ZZ /\ B e. ZZ ) )
41 6 anim1i 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> ( -u C e. ZZ /\ D e. ZZ ) )
42 41 ad2antlr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - -u C ) /\ A || ( C - -u D ) ) ) -> ( -u C e. ZZ /\ D e. ZZ ) )
43 simpl 
 |-  ( ( A e. ZZ /\ D e. ZZ ) -> A e. ZZ )
44 simpr 
 |-  ( ( B e. ZZ /\ C e. ZZ ) -> C e. ZZ )
45 43 44 anim12i 
 |-  ( ( ( A e. ZZ /\ D e. ZZ ) /\ ( B e. ZZ /\ C e. ZZ ) ) -> ( A e. ZZ /\ C e. ZZ ) )
46 45 an42s 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( A e. ZZ /\ C e. ZZ ) )
47 46 adantr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ A || ( C - -u D ) ) -> ( A e. ZZ /\ C e. ZZ ) )
48 7 adantl 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> -u D e. ZZ )
49 48 ad2antlr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ A || ( C - -u D ) ) -> -u D e. ZZ )
50 simpr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ A || ( C - -u D ) ) -> A || ( C - -u D ) )
51 congsym 
 |-  ( ( ( A e. ZZ /\ C e. ZZ ) /\ ( -u D e. ZZ /\ A || ( C - -u D ) ) ) -> A || ( -u D - C ) )
52 47 49 50 51 syl12anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ A || ( C - -u D ) ) -> A || ( -u D - C ) )
53 52 ex 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( A || ( C - -u D ) -> A || ( -u D - C ) ) )
54 18 negnegd 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> -u -u C = C )
55 54 oveq2d 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> ( -u D - -u -u C ) = ( -u D - C ) )
56 zcn 
 |-  ( -u C e. ZZ -> -u C e. CC )
57 56 adantr 
 |-  ( ( -u C e. ZZ /\ -u D e. ZZ ) -> -u C e. CC )
58 8 57 syl 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> -u C e. CC )
59 20 58 neg2subd 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> ( -u D - -u -u C ) = ( -u C - D ) )
60 55 59 eqtr3d 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> ( -u D - C ) = ( -u C - D ) )
61 60 adantl 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( -u D - C ) = ( -u C - D ) )
62 61 breq2d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( A || ( -u D - C ) <-> A || ( -u C - D ) ) )
63 53 62 sylibd 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( A || ( C - -u D ) -> A || ( -u C - D ) ) )
64 63 anim2d 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( A || ( B - -u C ) /\ A || ( C - -u D ) ) -> ( A || ( B - -u C ) /\ A || ( -u C - D ) ) ) )
65 64 imp 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - -u C ) /\ A || ( C - -u D ) ) ) -> ( A || ( B - -u C ) /\ A || ( -u C - D ) ) )
66 congtr 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( -u C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - -u C ) /\ A || ( -u C - D ) ) ) -> A || ( B - D ) )
67 40 42 65 66 syl3anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - -u C ) /\ A || ( C - -u D ) ) ) -> A || ( B - D ) )
68 67 orcd 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) /\ ( A || ( B - -u C ) /\ A || ( C - -u D ) ) ) -> ( A || ( B - D ) \/ A || ( B - -u D ) ) )
69 68 ex 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( A || ( B - -u C ) /\ A || ( C - -u D ) ) -> ( A || ( B - D ) \/ A || ( B - -u D ) ) ) )
70 4 31 39 69 ccased 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) ) -> ( ( ( A || ( B - C ) \/ A || ( B - -u C ) ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) -> ( A || ( B - D ) \/ A || ( B - -u D ) ) ) )
71 70 3impia 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( ( A || ( B - C ) \/ A || ( B - -u C ) ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) ) -> ( A || ( B - D ) \/ A || ( B - -u D ) ) )