Metamath Proof Explorer

Theorem fzodisj

Description: Abutting half-open integer ranges are disjoint. (Contributed by Stefan O'Rear, 14-Aug-2015)

Ref Expression
Assertion fzodisj 
|- ( ( A ..^ B ) i^i ( B ..^ C ) ) = (/)

Proof

Step Hyp Ref Expression
1 disj1 
 |-  ( ( ( A ..^ B ) i^i ( B ..^ C ) ) = (/) <-> A. x ( x e. ( A ..^ B ) -> -. x e. ( B ..^ C ) ) )
2 elfzolt2 
 |-  ( x e. ( A ..^ B ) -> x < B )
3 elfzoelz 
 |-  ( x e. ( A ..^ B ) -> x e. ZZ )
4 3 zred 
 |-  ( x e. ( A ..^ B ) -> x e. RR )
5 elfzoel2 
 |-  ( x e. ( A ..^ B ) -> B e. ZZ )
6 5 zred 
 |-  ( x e. ( A ..^ B ) -> B e. RR )
7 4 6 ltnled 
 |-  ( x e. ( A ..^ B ) -> ( x < B <-> -. B <_ x ) )
8 2 7 mpbid 
 |-  ( x e. ( A ..^ B ) -> -. B <_ x )
9 elfzole1 
 |-  ( x e. ( B ..^ C ) -> B <_ x )
10 8 9 nsyl 
 |-  ( x e. ( A ..^ B ) -> -. x e. ( B ..^ C ) )
11 1 10 mpgbir 
 |-  ( ( A ..^ B ) i^i ( B ..^ C ) ) = (/)