Theorem jm2.25lem1

Description: Lemma for jm2.26 . (Contributed by Stefan O'Rear, 2-Oct-2014)

	Ref	Expression
Assertion	jm2.25lem1	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) → ( ( 𝐴 ∥ ( 𝐷 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐷 − - 𝐵 ) ) ↔ ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl1l	⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) ∧ ( 𝐴 ∥ ( 𝐷 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐷 − - 𝐵 ) ) ) → 𝐴 ∈ ℤ )
2		simpl2l	⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) ∧ ( 𝐴 ∥ ( 𝐷 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐷 − - 𝐵 ) ) ) → 𝐶 ∈ ℤ )
3		simpl2r	⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) ∧ ( 𝐴 ∥ ( 𝐷 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐷 − - 𝐵 ) ) ) → 𝐷 ∈ ℤ )
4		simpl1r	⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) ∧ ( 𝐴 ∥ ( 𝐷 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐷 − - 𝐵 ) ) ) → 𝐵 ∈ ℤ )
5		simpl3	⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) ∧ ( 𝐴 ∥ ( 𝐷 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐷 − - 𝐵 ) ) ) → ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) )
6		simpr	⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) ∧ ( 𝐴 ∥ ( 𝐷 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐷 − - 𝐵 ) ) ) → ( 𝐴 ∥ ( 𝐷 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐷 − - 𝐵 ) ) )
7		acongtr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) ∧ ( 𝐷 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ∧ ( 𝐴 ∥ ( 𝐷 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐷 − - 𝐵 ) ) ) ) → ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) )
8	1 2 3 4 5 6 7	syl222anc	⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) ∧ ( 𝐴 ∥ ( 𝐷 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐷 − - 𝐵 ) ) ) → ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) )
9		simpl1l	⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) ) → 𝐴 ∈ ℤ )
10		simpl2r	⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) ) → 𝐷 ∈ ℤ )
11		simpl2l	⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) ) → 𝐶 ∈ ℤ )
12		simpl1r	⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) ) → 𝐵 ∈ ℤ )
13		simpl3	⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) ) → ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) )
14		acongsym	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) → ( 𝐴 ∥ ( 𝐷 − 𝐶 ) ∨ 𝐴 ∥ ( 𝐷 − - 𝐶 ) ) )
15	9 11 10 13 14	syl31anc	⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) ) → ( 𝐴 ∥ ( 𝐷 − 𝐶 ) ∨ 𝐴 ∥ ( 𝐷 − - 𝐶 ) ) )
16		simpr	⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) ) → ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) )
17		acongtr	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( ( 𝐴 ∥ ( 𝐷 − 𝐶 ) ∨ 𝐴 ∥ ( 𝐷 − - 𝐶 ) ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) ) ) → ( 𝐴 ∥ ( 𝐷 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐷 − - 𝐵 ) ) )
18	9 10 11 12 15 16 17	syl222anc	⊢ ( ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) ) → ( 𝐴 ∥ ( 𝐷 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐷 − - 𝐵 ) ) )
19	8 18	impbida	⊢ ( ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) ∧ ( 𝐶 ∈ ℤ ∧ 𝐷 ∈ ℤ ) ∧ ( 𝐴 ∥ ( 𝐶 − 𝐷 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐷 ) ) ) → ( ( 𝐴 ∥ ( 𝐷 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐷 − - 𝐵 ) ) ↔ ( 𝐴 ∥ ( 𝐶 − 𝐵 ) ∨ 𝐴 ∥ ( 𝐶 − - 𝐵 ) ) ) )