# Metamath Proof Explorer

## Theorem acongtr

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

Ref Expression
Assertion acongtr ${⊢}\left(\left({A}\in ℤ\wedge {B}\in ℤ\right)\wedge \left({C}\in ℤ\wedge {D}\in ℤ\right)\wedge \left(\left({A}\parallel \left({B}-{C}\right)\vee {A}\parallel \left({B}-\left(-{C}\right)\right)\right)\wedge \left({A}\parallel \left({C}-{D}\right)\vee {A}\parallel \left({C}-\left(-{D}\right)\right)\right)\right)\right)\to \left({A}\parallel \left({B}-{D}\right)\vee {A}\parallel \left({B}-\left(-{D}\right)\right)\right)$

### Proof

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