Theorem fzdisj

Description: Condition for two finite intervals of integers to be disjoint. (Contributed by Jeff Madsen, 17-Jun-2010)

	Ref	Expression
Assertion	fzdisj	|- ( K < M -> ( ( J ... K ) i^i ( M ... N ) ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		elin	|- ( x e. ( ( J ... K ) i^i ( M ... N ) ) <-> ( x e. ( J ... K ) /\ x e. ( M ... N ) ) )
2		elfzel1	|- ( x e. ( M ... N ) -> M e. ZZ )
3	2	adantl	|- ( ( x e. ( J ... K ) /\ x e. ( M ... N ) ) -> M e. ZZ )
4	3	zred	|- ( ( x e. ( J ... K ) /\ x e. ( M ... N ) ) -> M e. RR )
5		elfzel2	|- ( x e. ( J ... K ) -> K e. ZZ )
6	5	adantr	|- ( ( x e. ( J ... K ) /\ x e. ( M ... N ) ) -> K e. ZZ )
7	6	zred	|- ( ( x e. ( J ... K ) /\ x e. ( M ... N ) ) -> K e. RR )
8		elfzelz	|- ( x e. ( M ... N ) -> x e. ZZ )
9	8	zred	|- ( x e. ( M ... N ) -> x e. RR )
10	9	adantl	|- ( ( x e. ( J ... K ) /\ x e. ( M ... N ) ) -> x e. RR )
11		elfzle1	|- ( x e. ( M ... N ) -> M <_ x )
12	11	adantl	|- ( ( x e. ( J ... K ) /\ x e. ( M ... N ) ) -> M <_ x )
13		elfzle2	|- ( x e. ( J ... K ) -> x <_ K )
14	13	adantr	|- ( ( x e. ( J ... K ) /\ x e. ( M ... N ) ) -> x <_ K )
15	4 10 7 12 14	letrd	|- ( ( x e. ( J ... K ) /\ x e. ( M ... N ) ) -> M <_ K )
16	4 7 15	lensymd	|- ( ( x e. ( J ... K ) /\ x e. ( M ... N ) ) -> -. K < M )
17	1 16	sylbi	|- ( x e. ( ( J ... K ) i^i ( M ... N ) ) -> -. K < M )
18	17	con2i	|- ( K < M -> -. x e. ( ( J ... K ) i^i ( M ... N ) ) )
19	18	eq0rdv	|- ( K < M -> ( ( J ... K ) i^i ( M ... N ) ) = (/) )