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 )