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 e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) -> ( ( A || ( D - B ) \/ A || ( D - -u B ) ) <-> ( A || ( C - B ) \/ A || ( C - -u B ) ) ) )

Proof

Step Hyp Ref Expression
1 simpl1l 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) /\ ( A || ( D - B ) \/ A || ( D - -u B ) ) ) -> A e. ZZ )
2 simpl2l 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) /\ ( A || ( D - B ) \/ A || ( D - -u B ) ) ) -> C e. ZZ )
3 simpl2r 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) /\ ( A || ( D - B ) \/ A || ( D - -u B ) ) ) -> D e. ZZ )
4 simpl1r 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) /\ ( A || ( D - B ) \/ A || ( D - -u B ) ) ) -> B e. ZZ )
5 simpl3 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) /\ ( A || ( D - B ) \/ A || ( D - -u B ) ) ) -> ( A || ( C - D ) \/ A || ( C - -u D ) ) )
6 simpr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) /\ ( A || ( D - B ) \/ A || ( D - -u B ) ) ) -> ( A || ( D - B ) \/ A || ( D - -u B ) ) )
7 acongtr 
 |-  ( ( ( A e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ B e. ZZ ) /\ ( ( A || ( C - D ) \/ A || ( C - -u D ) ) /\ ( A || ( D - B ) \/ A || ( D - -u B ) ) ) ) -> ( A || ( C - B ) \/ A || ( C - -u B ) ) )
8 1 2 3 4 5 6 7 syl222anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) /\ ( A || ( D - B ) \/ A || ( D - -u B ) ) ) -> ( A || ( C - B ) \/ A || ( C - -u B ) ) )
9 simpl1l 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) /\ ( A || ( C - B ) \/ A || ( C - -u B ) ) ) -> A e. ZZ )
10 simpl2r 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) /\ ( A || ( C - B ) \/ A || ( C - -u B ) ) ) -> D e. ZZ )
11 simpl2l 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) /\ ( A || ( C - B ) \/ A || ( C - -u B ) ) ) -> C e. ZZ )
12 simpl1r 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) /\ ( A || ( C - B ) \/ A || ( C - -u B ) ) ) -> B e. ZZ )
13 simpl3 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) /\ ( A || ( C - B ) \/ A || ( C - -u B ) ) ) -> ( A || ( C - D ) \/ A || ( C - -u D ) ) )
14 acongsym 
 |-  ( ( ( A e. ZZ /\ C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) -> ( A || ( D - C ) \/ A || ( D - -u C ) ) )
15 9 11 10 13 14 syl31anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) /\ ( A || ( C - B ) \/ A || ( C - -u B ) ) ) -> ( A || ( D - C ) \/ A || ( D - -u C ) ) )
16 simpr 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) /\ ( A || ( C - B ) \/ A || ( C - -u B ) ) ) -> ( A || ( C - B ) \/ A || ( C - -u B ) ) )
17 acongtr 
 |-  ( ( ( A e. ZZ /\ D e. ZZ ) /\ ( C e. ZZ /\ B e. ZZ ) /\ ( ( A || ( D - C ) \/ A || ( D - -u C ) ) /\ ( A || ( C - B ) \/ A || ( C - -u B ) ) ) ) -> ( A || ( D - B ) \/ A || ( D - -u B ) ) )
18 9 10 11 12 15 16 17 syl222anc 
 |-  ( ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) /\ ( A || ( C - B ) \/ A || ( C - -u B ) ) ) -> ( A || ( D - B ) \/ A || ( D - -u B ) ) )
19 8 18 impbida 
 |-  ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) -> ( ( A || ( D - B ) \/ A || ( D - -u B ) ) <-> ( A || ( C - B ) \/ A || ( C - -u B ) ) ) )