Theorem xrlttri5d

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

	Ref	Expression
Hypotheses	xrlttri5d.a	$$⊢\phi \to A\in {ℝ}^{*}$$
	xrlttri5d.b	$$⊢\phi \to B\in {ℝ}^{*}$$
	xrlttri5d.aneb	$$⊢\phi \to A\ne B$$
	xrlttri5d.nlt	$$⊢\phi \to \neg B<A$$
Assertion	xrlttri5d	$$⊢\phi \to A<B$$

Proof

Step	Hyp	Ref	Expression
1		xrlttri5d.a	$$⊢\phi \to A\in {ℝ}^{*}$$
2		xrlttri5d.b	$$⊢\phi \to B\in {ℝ}^{*}$$
3		xrlttri5d.aneb	$$⊢\phi \to A\ne B$$
4		xrlttri5d.nlt	$$⊢\phi \to \neg B<A$$
5	3	neneqd	$$⊢\phi \to \neg A=B$$
6		xrlttri3	$$⊢\left(A\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(A=B\leftrightarrow \left(\neg A<B\wedge \neg B<A\right)\right)$$
7	1 2 6	syl2anc	$$⊢\phi \to \left(A=B\leftrightarrow \left(\neg A<B\wedge \neg B<A\right)\right)$$
8	5 7	mtbid	$$⊢\phi \to \neg \left(\neg A<B\wedge \neg B<A\right)$$
9		oran	$$⊢\left(A<B\vee B<A\right)\leftrightarrow \neg \left(\neg A<B\wedge \neg B<A\right)$$
10	8 9	sylibr	$$⊢\phi \to \left(A<B\vee B<A\right)$$
11	10 4	jca	$$⊢\phi \to \left(\left(A<B\vee B<A\right)\wedge \neg B<A\right)$$
12		pm5.61	$$⊢\left(\left(A<B\vee B<A\right)\wedge \neg B<A\right)\leftrightarrow \left(A<B\wedge \neg B<A\right)$$
13	11 12	sylib	$$⊢\phi \to \left(A<B\wedge \neg B<A\right)$$
14	13	simpld	$$⊢\phi \to A<B$$