Metamath Proof Explorer

Theorem ltord2

Description: Infer an ordering relation from a proof in only one direction. (Contributed by Mario Carneiro, 14-Jun-2014)

Ref Expression
Hypotheses ltord.1 
|- ( x = y -> A = B )
ltord.2 
|- ( x = C -> A = M )
ltord.3 
|- ( x = D -> A = N )
ltord.4 
|- S C_ RR
ltord.5 
|- ( ( ph /\ x e. S ) -> A e. RR )
ltord2.6 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x < y -> B < A ) )
Assertion ltord2 
|- ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C < D <-> N < M ) )

Proof

Step Hyp Ref Expression
1 ltord.1 
 |-  ( x = y -> A = B )
2 ltord.2 
 |-  ( x = C -> A = M )
3 ltord.3 
 |-  ( x = D -> A = N )
4 ltord.4 
 |-  S C_ RR
5 ltord.5 
 |-  ( ( ph /\ x e. S ) -> A e. RR )
6 ltord2.6 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x < y -> B < A ) )
7 1 negeqd 
 |-  ( x = y -> -u A = -u B )
8 2 negeqd 
 |-  ( x = C -> -u A = -u M )
9 3 negeqd 
 |-  ( x = D -> -u A = -u N )
10 5 renegcld 
 |-  ( ( ph /\ x e. S ) -> -u A e. RR )
11 5 ralrimiva 
 |-  ( ph -> A. x e. S A e. RR )
12 1 eleq1d 
 |-  ( x = y -> ( A e. RR <-> B e. RR ) )
13 12 rspccva 
 |-  ( ( A. x e. S A e. RR /\ y e. S ) -> B e. RR )
14 11 13 sylan 
 |-  ( ( ph /\ y e. S ) -> B e. RR )
15 14 adantrl 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> B e. RR )
16 5 adantrr 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> A e. RR )
17 ltneg 
 |-  ( ( B e. RR /\ A e. RR ) -> ( B < A <-> -u A < -u B ) )
18 15 16 17 syl2anc 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( B < A <-> -u A < -u B ) )
19 6 18 sylibd 
 |-  ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x < y -> -u A < -u B ) )
20 7 8 9 4 10 19 ltord1 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C < D <-> -u M < -u N ) )
21 3 eleq1d 
 |-  ( x = D -> ( A e. RR <-> N e. RR ) )
22 21 rspccva 
 |-  ( ( A. x e. S A e. RR /\ D e. S ) -> N e. RR )
23 11 22 sylan 
 |-  ( ( ph /\ D e. S ) -> N e. RR )
24 23 adantrl 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> N e. RR )
25 2 eleq1d 
 |-  ( x = C -> ( A e. RR <-> M e. RR ) )
26 25 rspccva 
 |-  ( ( A. x e. S A e. RR /\ C e. S ) -> M e. RR )
27 11 26 sylan 
 |-  ( ( ph /\ C e. S ) -> M e. RR )
28 27 adantrr 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> M e. RR )
29 ltneg 
 |-  ( ( N e. RR /\ M e. RR ) -> ( N < M <-> -u M < -u N ) )
30 24 28 29 syl2anc 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( N < M <-> -u M < -u N ) )
31 20 30 bitr4d 
 |-  ( ( ph /\ ( C e. S /\ D e. S ) ) -> ( C < D <-> N < M ) )