Theorem ltnsym

Description: 'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002)

	Ref	Expression
Assertion	ltnsym	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\to \neg B<A\right)$$

Proof

Step	Hyp	Ref	Expression
1		axlttri	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow \neg \left(A=B\vee B<A\right)\right)$$
2		pm2.46	$$⊢\neg \left(A=B\vee B<A\right)\to \neg B<A$$
3	1 2	biimtrdi	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\to \neg B<A\right)$$