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 ) ) ) |