Metamath Proof Explorer

Theorem acongtr

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

Ref Expression
Assertion acongtr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ B − C ∨ A ∥ B − − C ∧ A ∥ C − D ∨ A ∥ C − − D → A ∥ B − D ∨ A ∥ B − − D

Proof

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