This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xrlttri5d

Description: Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses xrlttri5d.a 
|- ( ph -> A e. RR* )
xrlttri5d.b 
|- ( ph -> B e. RR* )
xrlttri5d.aneb 
|- ( ph -> A =/= B )
xrlttri5d.nlt 
|- ( ph -> -. B < A )
Assertion xrlttri5d 
|- ( ph -> A < B )

Proof

Step Hyp Ref Expression
1 xrlttri5d.a 
 |-  ( ph -> A e. RR* )
2 xrlttri5d.b 
 |-  ( ph -> B e. RR* )
3 xrlttri5d.aneb 
 |-  ( ph -> A =/= B )
4 xrlttri5d.nlt 
 |-  ( ph -> -. B < A )
5 3 neneqd 
 |-  ( ph -> -. A = B )
6 xrlttri3 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
7 1 2 6 syl2anc 
 |-  ( ph -> ( A = B <-> ( -. A < B /\ -. B < A ) ) )
8 5 7 mtbid 
 |-  ( ph -> -. ( -. A < B /\ -. B < A ) )
9 oran 
 |-  ( ( A < B \/ B < A ) <-> -. ( -. A < B /\ -. B < A ) )
10 8 9 sylibr 
 |-  ( ph -> ( A < B \/ B < A ) )
11 10 4 jca 
 |-  ( ph -> ( ( A < B \/ B < A ) /\ -. B < A ) )
12 pm5.61 
 |-  ( ( ( A < B \/ B < A ) /\ -. B < A ) <-> ( A < B /\ -. B < A ) )
13 11 12 sylib 
 |-  ( ph -> ( A < B /\ -. B < A ) )
14 13 simpld 
 |-  ( ph -> A < B )