Metamath Proof Explorer

Theorem jm2.25lem1

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

Ref Expression
Assertion jm2.25lem1 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D → A ∥ D − B ∨ A ∥ D − − B ↔ A ∥ C − B ∨ A ∥ C − − B

Proof

Step Hyp Ref Expression
1 simpl1l ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D ∧ A ∥ D − B ∨ A ∥ D − − B → A ∈ ℤ
2 simpl2l ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D ∧ A ∥ D − B ∨ A ∥ D − − B → C ∈ ℤ
3 simpl2r ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D ∧ A ∥ D − B ∨ A ∥ D − − B → D ∈ ℤ
4 simpl1r ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D ∧ A ∥ D − B ∨ A ∥ D − − B → B ∈ ℤ
5 simpl3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D ∧ A ∥ D − B ∨ A ∥ D − − B → A ∥ C − D ∨ A ∥ C − − D
6 simpr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D ∧ A ∥ D − B ∨ A ∥ D − − B → A ∥ D − B ∨ A ∥ D − − B
7 acongtr ⊢ A ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ B ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D ∧ A ∥ D − B ∨ A ∥ D − − B → A ∥ C − B ∨ A ∥ C − − B
8 1 2 3 4 5 6 7 syl222anc ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D ∧ A ∥ D − B ∨ A ∥ D − − B → A ∥ C − B ∨ A ∥ C − − B
9 simpl1l ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D ∧ A ∥ C − B ∨ A ∥ C − − B → A ∈ ℤ
10 simpl2r ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D ∧ A ∥ C − B ∨ A ∥ C − − B → D ∈ ℤ
11 simpl2l ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D ∧ A ∥ C − B ∨ A ∥ C − − B → C ∈ ℤ
12 simpl1r ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D ∧ A ∥ C − B ∨ A ∥ C − − B → B ∈ ℤ
13 simpl3 ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D ∧ A ∥ C − B ∨ A ∥ C − − B → A ∥ C − D ∨ A ∥ C − − D
14 acongsym ⊢ A ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D → A ∥ D − C ∨ A ∥ D − − C
15 9 11 10 13 14 syl31anc ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D ∧ A ∥ C − B ∨ A ∥ C − − B → A ∥ D − C ∨ A ∥ D − − C
16 simpr ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D ∧ A ∥ C − B ∨ A ∥ C − − B → A ∥ C − B ∨ A ∥ C − − B
17 acongtr ⊢ A ∈ ℤ ∧ D ∈ ℤ ∧ C ∈ ℤ ∧ B ∈ ℤ ∧ A ∥ D − C ∨ A ∥ D − − C ∧ A ∥ C − B ∨ A ∥ C − − B → A ∥ D − B ∨ A ∥ D − − B
18 9 10 11 12 15 16 17 syl222anc ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D ∧ A ∥ C − B ∨ A ∥ C − − B → A ∥ D − B ∨ A ∥ D − − B
19 8 18 impbida ⊢ A ∈ ℤ ∧ B ∈ ℤ ∧ C ∈ ℤ ∧ D ∈ ℤ ∧ A ∥ C − D ∨ A ∥ C − − D → A ∥ D − B ∨ A ∥ D − − B ↔ A ∥ C − B ∨ A ∥ C − − B