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