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 )