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

Metamath Proof Explorer

Theorem lttri5d

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

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

Proof

Step Hyp Ref Expression
1 lttri5d.a 
 |-  ( ph -> A e. RR )
2 lttri5d.b 
 |-  ( ph -> B e. RR )
3 lttri5d.aneb 
 |-  ( ph -> A =/= B )
4 lttri5d.nlt 
 |-  ( ph -> -. B < A )
5 1 rexrd 
 |-  ( ph -> A e. RR* )
6 2 rexrd 
 |-  ( ph -> B e. RR* )
7 5 6 3 4 xrlttri5d 
 |-  ( ph -> A < B )