Metamath Proof Explorer

Theorem acongtr

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

Ref Expression
Assertion acongtr ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( ( 𝐴 ∥ ( 𝐵 − 𝐶 ) ∨ 𝐴 ∥ ( 𝐵 − - 𝐶 ) ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) ) → ( 𝐴 ∥ ( 𝐵 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐵 − - 𝐷 ) ) )

Proof

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