Metamath Proof Explorer

Theorem signslema

Description: Computational part of ~? signwlemn . (Contributed by Thierry Arnoux, 29-Sep-2018)

Ref Expression
Hypotheses signslema.1 
|- ( ph -> E e. NN0 )
signslema.2 
|- ( ph -> F e. NN0 )
signslema.3 
|- ( ph -> G e. NN0 )
signslema.4 
|- ( ph -> H e. NN0 )
signslema.5 
|- ( ph -> ( E < G /\ -. 2 || ( G - E ) ) )
signslema.6 
|- ( ph -> ( ( H - G ) - ( F - E ) ) e. { 0 , 2 } )
Assertion signslema 
|- ( ph -> ( F < H /\ -. 2 || ( H - F ) ) )

Proof

Step Hyp Ref Expression
1 signslema.1 
 |-  ( ph -> E e. NN0 )
2 signslema.2 
 |-  ( ph -> F e. NN0 )
3 signslema.3 
 |-  ( ph -> G e. NN0 )
4 signslema.4 
 |-  ( ph -> H e. NN0 )
5 signslema.5 
 |-  ( ph -> ( E < G /\ -. 2 || ( G - E ) ) )
6 signslema.6 
 |-  ( ph -> ( ( H - G ) - ( F - E ) ) e. { 0 , 2 } )
7 5 simpld 
 |-  ( ph -> E < G )
8 7 adantr 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 0 ) -> E < G )
9 4 nn0cnd 
 |-  ( ph -> H e. CC )
10 2 nn0cnd 
 |-  ( ph -> F e. CC )
11 9 10 subcld 
 |-  ( ph -> ( H - F ) e. CC )
12 3 nn0cnd 
 |-  ( ph -> G e. CC )
13 1 nn0cnd 
 |-  ( ph -> E e. CC )
14 12 13 subcld 
 |-  ( ph -> ( G - E ) e. CC )
15 11 14 subeq0ad 
 |-  ( ph -> ( ( ( H - F ) - ( G - E ) ) = 0 <-> ( H - F ) = ( G - E ) ) )
16 15 biimpa 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 0 ) -> ( H - F ) = ( G - E ) )
17 16 breq2d 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 0 ) -> ( 0 < ( H - F ) <-> 0 < ( G - E ) ) )
18 2 nn0red 
 |-  ( ph -> F e. RR )
19 4 nn0red 
 |-  ( ph -> H e. RR )
20 18 19 posdifd 
 |-  ( ph -> ( F < H <-> 0 < ( H - F ) ) )
21 20 adantr 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 0 ) -> ( F < H <-> 0 < ( H - F ) ) )
22 1 nn0red 
 |-  ( ph -> E e. RR )
23 3 nn0red 
 |-  ( ph -> G e. RR )
24 22 23 posdifd 
 |-  ( ph -> ( E < G <-> 0 < ( G - E ) ) )
25 24 adantr 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 0 ) -> ( E < G <-> 0 < ( G - E ) ) )
26 17 21 25 3bitr4rd 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 0 ) -> ( E < G <-> F < H ) )
27 8 26 mpbid 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 0 ) -> F < H )
28 0red 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 2 ) -> 0 e. RR )
29 23 22 resubcld 
 |-  ( ph -> ( G - E ) e. RR )
30 29 adantr 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 2 ) -> ( G - E ) e. RR )
31 19 18 resubcld 
 |-  ( ph -> ( H - F ) e. RR )
32 31 adantr 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 2 ) -> ( H - F ) e. RR )
33 7 adantr 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 2 ) -> E < G )
34 24 adantr 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 2 ) -> ( E < G <-> 0 < ( G - E ) ) )
35 33 34 mpbid 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 2 ) -> 0 < ( G - E ) )
36 2pos 
 |-  0 < 2
37 breq2 
 |-  ( ( ( H - F ) - ( G - E ) ) = 2 -> ( 0 < ( ( H - F ) - ( G - E ) ) <-> 0 < 2 ) )
38 36 37 mpbiri 
 |-  ( ( ( H - F ) - ( G - E ) ) = 2 -> 0 < ( ( H - F ) - ( G - E ) ) )
39 29 31 posdifd 
 |-  ( ph -> ( ( G - E ) < ( H - F ) <-> 0 < ( ( H - F ) - ( G - E ) ) ) )
40 39 biimpar 
 |-  ( ( ph /\ 0 < ( ( H - F ) - ( G - E ) ) ) -> ( G - E ) < ( H - F ) )
41 38 40 sylan2 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 2 ) -> ( G - E ) < ( H - F ) )
42 28 30 32 35 41 lttrd 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 2 ) -> 0 < ( H - F ) )
43 20 adantr 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 2 ) -> ( F < H <-> 0 < ( H - F ) ) )
44 42 43 mpbird 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 2 ) -> F < H )
45 9 12 10 13 sub4d 
 |-  ( ph -> ( ( H - G ) - ( F - E ) ) = ( ( H - F ) - ( G - E ) ) )
46 45 6 eqeltrrd 
 |-  ( ph -> ( ( H - F ) - ( G - E ) ) e. { 0 , 2 } )
47 ovex 
 |-  ( ( H - F ) - ( G - E ) ) e. _V
48 47 elpr 
 |-  ( ( ( H - F ) - ( G - E ) ) e. { 0 , 2 } <-> ( ( ( H - F ) - ( G - E ) ) = 0 \/ ( ( H - F ) - ( G - E ) ) = 2 ) )
49 46 48 sylib 
 |-  ( ph -> ( ( ( H - F ) - ( G - E ) ) = 0 \/ ( ( H - F ) - ( G - E ) ) = 2 ) )
50 27 44 49 mpjaodan 
 |-  ( ph -> F < H )
51 5 simprd 
 |-  ( ph -> -. 2 || ( G - E ) )
52 51 adantr 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 0 ) -> -. 2 || ( G - E ) )
53 16 breq2d 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 0 ) -> ( 2 || ( H - F ) <-> 2 || ( G - E ) ) )
54 52 53 mtbird 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 0 ) -> -. 2 || ( H - F ) )
55 2z 
 |-  2 e. ZZ
56 3 nn0zd 
 |-  ( ph -> G e. ZZ )
57 1 nn0zd 
 |-  ( ph -> E e. ZZ )
58 56 57 zsubcld 
 |-  ( ph -> ( G - E ) e. ZZ )
59 dvdsaddr 
 |-  ( ( 2 e. ZZ /\ ( G - E ) e. ZZ ) -> ( 2 || ( G - E ) <-> 2 || ( ( G - E ) + 2 ) ) )
60 55 58 59 sylancr 
 |-  ( ph -> ( 2 || ( G - E ) <-> 2 || ( ( G - E ) + 2 ) ) )
61 51 60 mtbid 
 |-  ( ph -> -. 2 || ( ( G - E ) + 2 ) )
62 61 adantr 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 2 ) -> -. 2 || ( ( G - E ) + 2 ) )
63 2cnd 
 |-  ( ph -> 2 e. CC )
64 11 14 63 subaddd 
 |-  ( ph -> ( ( ( H - F ) - ( G - E ) ) = 2 <-> ( ( G - E ) + 2 ) = ( H - F ) ) )
65 64 biimpa 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 2 ) -> ( ( G - E ) + 2 ) = ( H - F ) )
66 65 breq2d 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 2 ) -> ( 2 || ( ( G - E ) + 2 ) <-> 2 || ( H - F ) ) )
67 62 66 mtbid 
 |-  ( ( ph /\ ( ( H - F ) - ( G - E ) ) = 2 ) -> -. 2 || ( H - F ) )
68 54 67 49 mpjaodan 
 |-  ( ph -> -. 2 || ( H - F ) )
69 50 68 jca 
 |-  ( ph -> ( F < H /\ -. 2 || ( H - F ) ) )