Theorem llnnlt

Description: Two lattice lines cannot satisfy the less than relation. (Contributed by NM, 26-Jun-2012)

	Ref	Expression
Hypotheses	llnnlt.s	|- .< = ( lt ` K )
	llnnlt.n	|- N = ( LLines ` K )
Assertion	llnnlt	|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> -. X .< Y )

Proof

Step	Hyp	Ref	Expression
1		llnnlt.s	|- .< = ( lt ` K )
2		llnnlt.n	|- N = ( LLines ` K )
3	1	pltirr	|- ( ( K e. HL /\ X e. N ) -> -. X .< X )
4	3	3adant3	|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> -. X .< X )
5		breq2	|- ( X = Y -> ( X .< X <-> X .< Y ) )
6	5	notbid	|- ( X = Y -> ( -. X .< X <-> -. X .< Y ) )
7	4 6	syl5ibcom	|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( X = Y -> -. X .< Y ) )
8		eqid	|- ( le ` K ) = ( le ` K )
9	8 1	pltle	|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( X .< Y -> X ( le ` K ) Y ) )
10	8 2	llncmp	|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( X ( le ` K ) Y <-> X = Y ) )
11	9 10	sylibd	|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( X .< Y -> X = Y ) )
12	11	necon3ad	|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> ( X =/= Y -> -. X .< Y ) )
13	7 12	pm2.61dne	|- ( ( K e. HL /\ X e. N /\ Y e. N ) -> -. X .< Y )