This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) = (/) )